finite_of_linearIndependent
theorem finite_of_linearIndependent :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] [inst_4 : Nontrivial R] {s : Set M},
LinearIndependent (ι := { x // x ∈ s }) R Subtype.val → s.Finite
This theorem, termed as `finite_of_linearIndependent`, states that for any ring `R`, any additive commutative group `M`, and any `R`-module `M`, if the ring `R` is Noetherian and non-trivial, then for any set `s` of `M`, if the family of vectors obtained from the elements of `s` (represented as subtypes) are linearly independent over `R`, then the set `s` is finite.
In less formal terms, this means that in a Noetherian, non-trivial ring, any set of vectors that are linearly independent must be finite. This theorem is also an alias of `LinearIndependent.set_finite_of_isNoetherian`.
More concisely: In a Noetherian, non-trivial ring, every linearly independent set of elements is finite.
|
IsNoetherian.noetherian
theorem IsNoetherian.noetherian :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[self : IsNoetherian R M] (s : Submodule R M), s.FG
The theorem `IsNoetherian.noetherian` states that for any semiring `R` and additive commutative monoid `M` that forms a `R`-module, if `M` is a Noetherian `R`-module (denoted by `IsNoetherian R M`), then all submodules of `M` (represented by `s`) are finitely generated (denoted by `s.FG`). The notion of a Noetherian `R`-module is implemented here as the predicate that all `R`-submodules of `M` are finitely generated.
More concisely: In a commutative semiring `R` and an additive commutative monoid `M` that forms an `R`-module, if `M` is Noetherian then all its submodules are finitely generated.
|
isNoetherianRing_iff
theorem isNoetherianRing_iff : ∀ {R : Type u_1} [inst : Semiring R], IsNoetherianRing R ↔ IsNoetherian R R
This theorem establishes the equivalence between a ring being a Noetherian ring and the ring being Noetherian over itself. In other words, for any type `R` with the structure of a semiring, `R` is a Noetherian ring if and only if `R` is Noetherian as a module over itself. A ring is Noetherian if all its ideals are finitely generated, which means there are only finitely many elements required to generate any ideal in the ring.
More concisely: A ring is Noetherian if and only if it is Noetherian as a module over itself. (That is, a ring is Noetherian if and only if all its ideals are finitely generated ideals.)
|
isNoetherianRing_of_ringEquiv
theorem isNoetherianRing_of_ringEquiv :
∀ (R : Type u_1) [inst : Ring R] {S : Type u_2} [inst_1 : Ring S],
R ≃+* S → ∀ [inst : IsNoetherianRing R], IsNoetherianRing S
The theorem `isNoetherianRing_of_ringEquiv` states that for any two types `R` and `S` that have a ring structure, if `R` is a Noetherian ring and there exists a ring isomorphism between `R` and `S`, then `S` is also a Noetherian ring. In other words, the property of being a Noetherian ring is preserved under a ring isomorphism. In mathematical terms, if $R$ is a Noetherian ring and there exists an isomorphism of rings between $R$ and $S$, then $S$ is also a Noetherian ring.
More concisely: If `R` is a Noetherian ring and there exists a ring isomorphism between `R` and `S`, then `S` is also a Noetherian ring. (Mathematically: If $R$ is a Noetherian ring and there exists a ring isomorphism between $R$ and $S$, then $S$ is also a Noetherian ring.)
|
isNoetherian_of_range_eq_ker
theorem isNoetherian_of_range_eq_ker :
∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P]
[inst_6 : Module R P] [inst_7 : IsNoetherian R M] [inst_8 : IsNoetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P),
LinearMap.range f = LinearMap.ker g → IsNoetherian R N
The theorem `isNoetherian_of_range_eq_ker` states that for any ring `R` and modules `M`, `N`, and `P` over `R`, if `M` and `P` are Noetherian modules and we have two linear maps `f` from `M` to `N` and `g` from `N` to `P` such that the range of `f` is equal to the kernel of `g` (thus forming an exact sequence), then `N` is also a Noetherian module. In other words, if the first and last modules in an exact sequence are Noetherian, then the middle module is also Noetherian.
More concisely: If `M` and `P` are Noetherian modules and there is an exact sequence `M → N → P`, then `N` is also Noetherian.
|
isNoetherian_of_linearEquiv
theorem isNoetherian_of_linearEquiv :
∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid P] [inst_3 : Module R M] [inst_4 : Module R P],
(M ≃ₗ[R] P) → ∀ [inst_5 : IsNoetherian R M], IsNoetherian R P
The theorem `isNoetherian_of_linearEquiv` states that for any semiring `R` and additively commutative monoids `M` and `P` that are also `R`-modules, if `M` is linearly equivalent to `P` (denoted as `M ≃ₗ[R] P`), then if `M` is a Noetherian `R`-module, `P` is also a Noetherian `R`-module. In simpler terms, this theorem says that the property of being a Noetherian module is preserved under linear equivalence.
More concisely: If `M` and `P` are additively commutative `R`-modules that are linearly equivalent and `M` is Noetherian, then `P` is also Noetherian.
|
isNoetherianRing_iff_ideal_fg
theorem isNoetherianRing_iff_ideal_fg :
∀ (R : Type u_1) [inst : Semiring R], IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG
The theorem `isNoetherianRing_iff_ideal_fg` states that a semiring `R` is a Noetherian ring if and only if all its ideals are finitely generated. In other words, a semiring is defined as Noetherian when every ideal (an additive submonoid where multiplication with any element from the ring results in another element within the ideal) is generated by a finite set of elements. The correspondence implies that no matter which ideal you choose within a Noetherian ring, you will always be able to find a finite set of generating elements.
More concisely: A semiring is Noetherian if and only if every ideal is finitely generated.
|
IsNoetherian.injective_of_surjective_endomorphism
theorem IsNoetherian.injective_of_surjective_endomorphism :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
This theorem states that for any Noetherian module 'M' over a ring 'R', if there is a surjective endomorphism 'f' (a linear map from 'M' to 'M'), then this endomorphism is also injective. In other words, in the context of Noetherian modules, surjective linear transformations are also injective. This theorem links the behavior of the function to the properties of the ring and the module. A Noetherian module is a type of mathematical structure that has a property related to the finite generation of its submodules.
More concisely: In a Noetherian module over a ring, any surjective endomorphism is injective.
|
isNoetherian_of_fg_of_noetherian
theorem isNoetherian_of_fg_of_noetherian :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
[I : IsNoetherianRing R], N.FG → IsNoetherian R ↥N
The theorem `isNoetherian_of_fg_of_noetherian` states that for any ring `R` and an additive commutative group `M` that is a module over `R`, if `R` is a Noetherian ring (i.e., all its ideals are finitely generated), then for any submodule `N` of `M` that is finitely generated, `N` is also a Noetherian module over `R`. In other words, if a ring is Noetherian and a submodule of a module over this ring is finitely generated, then this submodule is also Noetherian as a module over the ring.
More concisely: If `R` is a Noetherian ring and `M` is an `R`-module with `N` a finitely generated submodule of `M`, then `N` is a Noetherian `R`-module.
|
isNoetherian_of_tower
theorem isNoetherian_of_tower :
∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
[inst_3 : SMul R S] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : IsScalarTower R S M],
IsNoetherian R M → IsNoetherian S M
This theorem states that if we have a scalar tower `M / S / R`, where `M`, `S`, and `R` are types, and if `M / R` is Noetherian (a property of rings and modules that loosely means they cannot be broken down into infinitely many smaller non-trivial submodules), then `M / S` is also Noetherian. This holds under the conditions that `R` is a semiring, `S` is a semiring, `M` is an additive commutative monoid, `R` can be multiplied by `S`, `M` is a module over `S`, `M` is a module over `R`, and `R`, `S`, and `M` form a scalar tower.
More concisely: If `M / S` is a scalar tower over semirings `R`, `S`, where `M` is an additive commutative monoid that is a module over both `R` and `S`, and `M / R` is Noetherian, then `M / S` is also Noetherian.
|
isNoetherianRing_of_surjective
theorem isNoetherianRing_of_surjective :
∀ (R : Type u_1) [inst : Ring R] (S : Type u_2) [inst_1 : Ring S] (f : R →+* S),
Function.Surjective ⇑f → ∀ [H : IsNoetherianRing R], IsNoetherianRing S
This theorem states that if we have two rings, `R` and `S`, and a ring homomorphism `f` from `R` to `S` that is surjective (meaning that for every element in `S`, there is some element in `R` such that the function `f` maps it to `S`), then if `R` is a Noetherian ring (i.e., a ring in which all ideals are finitely generated), `S` is also a Noetherian ring. To put it in simpler terms, surjective ring homomorphisms preserve the property of being a Noetherian ring.
More concisely: If `f` is a surjective ring homomorphism from the Noetherian ring `R` to the ring `S`, then `S` is also a Noetherian ring.
|
IsNoetherian.disjoint_partialSups_eventually_bot
theorem IsNoetherian.disjoint_partialSups_eventually_bot :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] (f : ℕ → Submodule R M),
(∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))) → ∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
This theorem states that in the context of a noetherian module, if we have a sequence of submodules, denoted by `f`, where the `n+1`-th submodule is disjoint from the supremum of the first `n` submodules, then the sequence `f` eventually becomes zero. In other words, there exists a certain `n` beyond which all submodules in the sequence are the zero submodule.
Here, disjointness of two submodules means that their infimum is the bottom element. Being a noetherian module means that every submodule is finitely generated.
More concisely: In a noetherian module, if a sequence of submodules has the property that the `(n+1)`-th submodule is disjoint from the sum of the first `n` submodules for all `n`, then the sequence is eventually the zero sequence.
|
isNoetherian_submodule
theorem isNoetherian_submodule :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{N : Submodule R M}, IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG
The theorem `isNoetherian_submodule` states that for any semiring `R`, any additive commutative monoid `M`, and any module `M` over `R`, and for any submodule `N` of `M`, `N` is Noetherian if and only if all submodules `s` of `N` are finitely generated. Here, "Noetherian" means that every ascending chain of submodules in `N` stabilizes (i.e., for every chain, there exists some point after which all further elements are the same), and "finitely generated" means that the submodule can be expressed as the span of a finite subset of `M`.
More concisely: A submodule of an `R`-module `M` is Noetherian if and only if every submodule of it is finitely generated.
|
isNoetherian_span_of_finite
theorem isNoetherian_span_of_finite :
∀ (R : Type u_1) {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherianRing R] {A : Set M}, A.Finite → IsNoetherian R ↥(Submodule.span R A)
The theorem `isNoetherian_span_of_finite` states that in a module over a Noetherian ring, if a set of vectors is finite, then the submodule generated by this set is also Noetherian. Here, a Noetherian module is one in which every submodule is finitely generated and a Noetherian ring is a ring which is Noetherian as a module over itself, meaning all its ideals are finitely generated. The submodule generated by a set is defined as the smallest submodule that contains the set.
More concisely: In a Noetherian ring, every finite subset generates a Noetherian submodule.
|
isNoetherian_iff_wellFounded
theorem isNoetherian_iff_wellFounded :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
This theorem states that for any given Type `R` and `M` where `R` is a semiring, `M` is an additive commutative monoid and `M` is also a module over `R`, the type `M` is Noetherian if and only if the relation "greater than" (`>`) on the elements of `M` is well-founded. In terms of mathematics, a module `M` over a ring `R` is said to be Noetherian if every non-empty set of submodules of `M` has a maximal element, and a relation is well-founded if there are no infinite decreasing chains. This theorem connects these two concepts, showing that they are equivalent in this context.
More concisely: A module over a semiring is Noetherian if and only if the "greater than" relation on its elements is well-founded.
|
set_has_maximal_iff_noetherian
theorem set_has_maximal_iff_noetherian :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M
The theorem `set_has_maximal_iff_noetherian` states that a module is Noetherian if and only if, for every nonempty set of submodules, there exists a submodule in that set such that there is no other submodule in the set which is larger than it. Here, 'larger' refers to the ordering in the lattice structure of submodules, where one submodule is larger than another if it contains the other. The theorem is stated for any semiring `R` and any `R`-module `M`, where `R` is a semiring, `M` is an additive commutative monoid and `M` is a module over `R`.
More concisely: A module over a semiring is Noetherian if and only if every nonempty set of its submodules has a maximal element with respect to the submodule lattice.
|
IsNoetherian.bijective_of_surjective_endomorphism
theorem IsNoetherian.bijective_of_surjective_endomorphism :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] (f : M →ₗ[R] M), Function.Surjective ⇑f → Function.Bijective ⇑f
The theorem `IsNoetherian.bijective_of_surjective_endomorphism` states that for any Noetherian module `M` over a ring `R`, if a function `f` from `M` to itself (an endomorphism of `M`) is surjective (i.e., for every element `m` in `M`, there exists an element `n` in `M` such that `f(n) = m`), then `f` is also bijective (i.e., `f` is both injective and surjective). In other words, in a Noetherian module, any surjective endomorphism is also an injective, thus is bijective.
More concisely: In a Noetherian module, every surjective endomorphism is bijective.
|
IsNoetherian.induction
theorem IsNoetherian.induction :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] {P : Submodule R M → Prop},
(∀ (I : Submodule R M), (∀ J > I, P J) → P I) → ∀ (I : Submodule R M), P I
This theorem is a form of mathematical induction for submodules in the context of Noetherian modules. Specifically, given a semiring 'R', an additive commutative monoid 'M', and a module 'M' over 'R', if the module 'M' is Noetherian then the property 'P' holds for all submodules 'I' if whenever 'P' holds for all submodules 'J' larger than 'I', then 'P' also holds for 'I'.
More concisely: If 'M' is a Noetherian module over a semiring 'R' and 'P' is a property that holds for all submodules 'I' of 'M' if it holds for all larger submodules, then 'P' holds for every submodule of 'M'.
|
isNoetherian_def
theorem isNoetherian_def :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
IsNoetherian R M ↔ ∀ (s : Submodule R M), s.FG
This theorem states that for any given types `R` and `M`, with `R` being a semiring, `M` an additive commutative monoid, and `M` also a `R`-module, a `R`-module `M` is Noetherian if and only if all of its submodules `s` are finitely generated. In mathematical terms, this theorem captures the definition of a Noetherian module in the context of ring theory and module theory: a module is said to be Noetherian when every submodule of it can be generated by a finite set.
More concisely: A module over a semiring is Noetherian if and only if all its submodules are finitely generated.
|
monotone_stabilizes_iff_noetherian
theorem monotone_stabilizes_iff_noetherian :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
(∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M
This theorem states that a module is Noetherian if and only if every increasing chain of its submodules eventually stabilizes. In more detail, given a semiring `R` and an additive commutative monoid `M` with a module structure over `R`, for any strictly increasing function `f` that maps each natural number to a submodule of `M`, there exists a certain natural number `n` such that for all numbers `m` greater than or equal to `n`, the `m`-th submodule in the chain is the same as the `n`-th one. The theorem shows this condition is equivalent to the module `M` being Noetherian.
More concisely: A module over a semiring is Noetherian if and only if every increasing chain of its submodules is eventually constant.
|
LinearIndependent.finite_of_isNoetherian
theorem LinearIndependent.finite_of_isNoetherian :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] [inst_4 : Nontrivial R] {ι : Type u_4} {v : ι → M},
LinearIndependent R v → Finite ι
This theorem states that if we have a family of vectors `v` in a module `M` over a ring `R` that is linearly independent, and if the module `M` is Noetherian and the ring `R` is non-trivial, then the indexing set `ι` of the family of vectors `v` must be finite. In other words, a linearly independent family of vectors in a Noetherian module over a non-trivial ring can only be finite in size.
More concisely: A linearly independent family of vectors in a Noetherian module over a non-trivial ring must be finite.
|
LinearMap.eventually_disjoint_ker_pow_range_pow
theorem LinearMap.eventually_disjoint_ker_pow_range_pow :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsNoetherian R M] (f : M →ₗ[R] M),
∀ᶠ (n : ℕ) in Filter.atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))
The theorem `LinearMap.eventually_disjoint_ker_pow_range_pow` states the following: For a given endomorphism of a Noetherian module (represented by the linear map `f` from `M` to `M` over the ring `R`), there exists a positive integer `n` such that for all `n' ≥ n`, the kernel of `f^n'` and the range of `f^n'` are disjoint. Here, "disjoint" means that their intersection is the zero or bottom element of the lattice, and "sufficiently large" refers to numbers that are greater than or equal to `n` (represented by the filter `Filter.atTop`). The underlying module is assumed to be Noetherian, meaning that every submodule satisfies the ascending chain condition.
More concisely: For any endomorphism of a Noetherian module, there exists a positive integer such that the kernel and range raised to that power are disjoint.
|