IsArtinian.induction
theorem IsArtinian.induction :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsArtinian 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, named `IsArtinian.induction`, states that if for any submodule `I` and `J` of a module `M` over a ring `R`, where `M` is an Artinian module, whenever `J` is strictly smaller than `I`, if property `P` holds for `J`, then `P` also holds for `I`, then we can conclude that property `P` holds for all submodules of `M`. This theorem is a form of mathematical induction applied to the context of submodules within an Artinian module.
More concisely: If `M` is an Artinian module and `P` is a property such that for any submodules `I` and `J` of `M` with `J` a proper subset of `I`, `P(J)` implies `P(I)`, then `P` holds for all submodules of `M`.
|
IsArtinian.monotone_stabilizes
theorem IsArtinian.monotone_stabilizes :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsArtinian R M] (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
This theorem states that for any given ordered homomorphism `f` from the natural numbers `ℕ` to the ordered dual of the set of submodules of a module `M` over a ring `R`, there exists a natural number `n` such that for all natural numbers `m` such that `n` is less than or equal to `m`, `f(n)` is equal to `f(m)`. The types `R` and `M` are universally quantified, as are the property of `R` being a ring, `M` being an `AddCommGroup`, and `M` being a module over `R`. The theorem also assumes that the module `M` is Artinian.
More concisely: For any Artinian module M over a ring R and ordered homomorphism f from the natural numbers to the ordered dual of submodules of M, there exists a natural number n such that for all m ≥ n, f(n) = f(m).
|
IsArtinian.bijective_of_injective_endomorphism
theorem IsArtinian.bijective_of_injective_endomorphism :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsArtinian R M] (f : M →ₗ[R] M), Function.Injective ⇑f → Function.Bijective ⇑f
The theorem `IsArtinian.bijective_of_injective_endomorphism` states that for any Artinian module `M` over a ring `R`, if there exists an endomorphism `f` of `M` that is injective (that is, if `f(x) = f(y)` implies `x = y`), then this endomorphism `f` is also bijective. In other words, `f` is both injective and surjective (for every element `b` in `M`, there is an element `a` in `M` such that `f(a) = b`). This theorem is a key result in the theory of Artinian modules, which are a special type of module in algebra that satisfy a descending chain condition.
More concisely: In an Artinian module over a ring, an injective endomorphism is bijective.
|
IsArtinian.surjective_of_injective_endomorphism
theorem IsArtinian.surjective_of_injective_endomorphism :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsArtinian R M] (f : M →ₗ[R] M), Function.Injective ⇑f → Function.Surjective ⇑f
The theorem `IsArtinian.surjective_of_injective_endomorphism` states that for any Artinian module `M` over a ring `R`, if we have an endomorphism `f` (a linear transformation from `M` to itself) which is injective (meaning that different inputs produce different outputs), then `f` is also surjective. In other words, every element of `M` is the image of some other element of `M` under the transformation `f`. This is an important property in the theory of Artinian modules and rings in abstract algebra.
More concisely: For any Artinian module M over a ring R, an injective endomorphism f of M is surjective.
|
IsArtinian.disjoint_partial_infs_eventually_top
theorem IsArtinian.disjoint_partial_infs_eventually_top :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsArtinian R M] (f : ℕ → Submodule R M),
(∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))) →
∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
The theorem `IsArtinian.disjoint_partial_infs_eventually_top` states that for an Artinian module, given a sequence `f` of its submodules such that for every natural number `n`, the supremum of `f (n + 1)` and the infimum of `f 0`, ..., `f n` are disjoint and equal to the top element, there exists a certain natural number such that all the submodules beyond that number in the sequence are equal to the top element. In other words, the sequence of submodules eventually becomes the top element.
More concisely: For an Artinian module and a sequence of its submodules with disjoint and equal supremum and infimum for every two consecutive indices, there exists a natural number such that all subsequent submodules in the sequence are the top element.
|
IsArtinian.wellFounded_submodule_lt
theorem IsArtinian.wellFounded_submodule_lt :
∀ (R : Type u_5) (M : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : IsArtinian R M], WellFounded fun x x_1 => x < x_1
This theorem states that for any semiring `R` and any additive commutative monoid `M` that also has a module structure over `R`, if `M` is Artinian (i.e., it satisfies the descending chain condition), then the relation "is a proper submodule of" (`x < x_1`) on the set of all submodules of `M` is a well-founded relation. A well-founded relation is one where there are no infinite descending chains, which aligns with the Artinian property.
More concisely: In a semiring `R` and an additive commutative `R`-module `M` that satisfies the descending chain condition, the relation "is a proper submodule of" on the set of submodules of `M` is well-founded.
|
LinearMap.isCompl_iSup_ker_pow_iInf_range_pow
theorem LinearMap.isCompl_iSup_ker_pow_iInf_range_pow :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : IsArtinian R M] [inst_4 : IsNoetherian R M] (f : M →ₗ[R] M),
IsCompl (⨆ n, LinearMap.ker (f ^ n)) (⨅ n, LinearMap.range (f ^ n))
This theorem states the Fitting decomposition of a module `M` with respect to an endomorphism `f`. In the context of a ring `R`, for a module `M` that is both Artinian and Noetherian, the theorem asserts that the suprema over all `n` of the kernel of `f` to the power `n` is complementary to the infima over all `n` of the range of `f` to the power `n`. This is a property of linear maps in the mathematical fields of ring and module theory.
More concisely: For an Artinian and Noetherian module `M` over a ring `R` and an endomorphism `f` of `M`, the supremum of the kernels of `f` raised to the power `n` equals the complement of the infimum of the images of `f` raised to the power `n`.
|
isArtinian_of_linearEquiv
theorem isArtinian_of_linearEquiv :
∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup P]
[inst_3 : Module R M] [inst_4 : Module R P], (M ≃ₗ[R] P) → ∀ [inst_5 : IsArtinian R M], IsArtinian R P
This theorem states that for any types `R`, `M`, and `P`, where `R` is a ring, `M` and `P` are additive commutative groups, `M` is a `R`-module, and `P` is also a `R`-module. Given that `M` is isomorphic to `P` under a linear equivalence, if `M` is an Artinian `R`-module, then `P` is also an Artinian `R`-module. In other words, the Artinian property of a module is preserved under a linear equivalence.
More concisely: If `M` and `P` are isomorphic additive commutative groups that are `R`-modules, and `M` is an Artinian `R`-module, then `P` is also an Artinian `R`-module.
|
isArtinian_span_of_finite
theorem isArtinian_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 : IsArtinianRing R] {A : Set M}, A.Finite → IsArtinian R ↥(Submodule.span R A)
The theorem "isArtinian_span_of_finite" states that for any Artinian ring `R` and a module `M` over `R`, if `A` is a finite set of vectors in `M`, then the submodule generated by `A` (denoted by `Submodule.span R A`) is an Artinian module over `R`. In other words, if we have an Artinian ring and a finite set of vectors, the submodule that these vectors span is also Artinian. This is a property about the "smallness" of submodules in the context of Artinian rings and modules.
More concisely: If `R` is an Artinian ring and `A` is a finite subset of an `R`-module `M`, then `Submodule.span R A` is an Artinian `R`-module.
|
set_has_minimal_iff_artinian
theorem set_has_minimal_iff_artinian :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M
The theorem `set_has_minimal_iff_artinian` states that: For any types `R` and `M`, where `R` is a ring, `M` is an additive commutative group and `M` is a module over `R`, a module is Artinian if and only if every nonempty set of `R`-submodules of `M` has a minimal `R`-submodule among them. In other words, we cannot find a `R`-submodule in the set that is strictly smaller than the minimal `R`-submodule. The condition of being "Artinian" for a module is equivalent to this property.
More concisely: A module over a ring is Artinian if and only if every nonempty collection of its submodules has a minimal element.
|
isArtinian_of_tower
theorem isArtinian_of_tower :
∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
[inst_3 : Algebra R S] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : IsScalarTower R S M],
IsArtinian R M → IsArtinian S M
This theorem states that if you have a scalar tower of types `M`, `S`, and `R`, where `M` over `R` is an Artinian ring, then `M` over `S` is also an Artinian ring. This is under the condition that `R` is a commutative ring, `S` is a ring, `M` is an additive commutative group, `S` is an `R`-algebra, `M` is an `S`-module, `M` is an `R`-module, and `M` is a scalar tower over `S` and `R`. In simpler terms, the theorem shows that the Artinian property propagates downwards in a scalar tower.
More concisely: If `M` is an Artinian `R`-module and `S` is a subring of `R`, then `M` is an Artinian `S`-module when `M` is an `S`-algebra and a scalar tower over `S` and `R`.
|
IsArtinianRing.localization_surjective
theorem IsArtinianRing.localization_surjective :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsArtinianRing R] (S : Submonoid R) (L : Type u_2)
[inst_2 : CommRing L] [inst_3 : Algebra R L] [inst_4 : IsLocalization S L],
Function.Surjective ⇑(algebraMap R L)
This theorem, `IsArtinianRing.localization_surjective`, states that for any Artinian ring `R`, any submonoid `S` of `R`, and any type `L` with a commutative ring structure and an algebra structure over `R` such that `L` is a localization of `R` at `S`, the algebra homomorphism from `R` to `L` given by the `Algebra` structure is surjective. In other words, every element in `L` is an image under this map of some element in `R`. This suggests that localising an Artinian ring cannot increase the amount of elements.
More concisely: For any Artinian ring `R`, any submonoid `S` of `R`, and any commutative `R`-algebra `L` obtained by localizing `R` at `S`, the algebra homomorphism from `R` to `L` is surjective.
|
monotone_stabilizes_iff_artinian
theorem monotone_stabilizes_iff_artinian :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
(∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsArtinian R M
The theorem states that a module is Artinian if and only if every decreasing chain of its submodules eventually stabilizes. In other words, given any strictly decreasing sequence of submodules (ordered by inclusion), there exists a certain point after which all submodules in the sequence are the same. This equivalence holds for any module over a ring, where the module and the ring are arbitrary types and the module has the structure of an additive commutative group and a module over the ring.
More concisely: A module over any ring is Artinian if and only if every decreasing sequence of its submodules has a stabilizing point.
|
IsArtinianRing.maximal_ideals_finite
theorem IsArtinianRing.maximal_ideals_finite :
∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsArtinianRing R], {I | I.IsMaximal}.Finite
This theorem, referenced as Stacks Lemma 00J7, states that for any given commutative ring `R` that is also an Artinian ring, the set of its maximal ideals is finite. In more mathematical terms, for a given ring `R`, if `R` satisfies the conditions of being both a commutative ring and an Artinian ring, then there exists a finite number of maximal ideals in `R`.
More concisely: In any commutative Artinian ring, the set of maximal ideals is finite.
|
LinearMap.eventually_isCompl_ker_pow_range_pow
theorem LinearMap.eventually_isCompl_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 : IsArtinian R M] [inst_4 : IsNoetherian R M] (f : M →ₗ[R] M),
∀ᶠ (n : ℕ) in Filter.atTop, IsCompl (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))
This theorem states that for any ring `R` and additive commutative group `M` that is both an Artinian and a Noetherian `R`-module, and for any linear map `f` from `M` to `M`, there eventually exists a natural number `n` such that the kernel of `f` to the power of `n` is complement to the range of `f` to the power of `n`. Here, "eventually" is in the sense of the filter `Filter.atTop`, which represents the limit `n → ∞`. This result is known as the Fitting decomposition of the module `M` with respect to the endomorphism `f`.
More concisely: For any Artinian and Noetherian `R`-module `M` and endomorphism `f`: There exists a natural number `n` such that `f^n(M)` and `(ker(f))^n` are complementary subspaces.
|
LinearMap.eventually_codisjoint_ker_pow_range_pow
theorem LinearMap.eventually_codisjoint_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 : IsArtinian R M] (f : M →ₗ[R] M),
∀ᶠ (n : ℕ) in Filter.atTop, Codisjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))
This theorem states that for any endomorphism (a function from a set to itself) of an Artinian module (a type of algebraic structure that satisfies a certain finiteness condition), there exists a point beyond which the kernel and range of the function's iterates are codisjoint. In other words, if you iterate the function enough times, then the kernel and range of the function become codisjoint. Here, being codisjoint for two elements in a lattice means that their supremum (or least upper bound) is the top element of the lattice. The kernel of a linear map refers to the set of elements that are mapped to zero, and the range refers to the set of resulting outputs after the map is applied. The `Filter.atTop` refers to the limit towards positive infinity.
More concisely: For any Artinian module endomorphism, the kernels and ranges of its iterates become codisjoint as the iteration count approaches infinity.
|
isArtinian_iff_wellFounded
theorem isArtinian_iff_wellFounded :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
IsArtinian R M ↔ WellFounded fun x x_1 => x < x_1
The theorem `isArtinian_iff_wellFounded` states that for any ring `R` and additively commutative group `M` which is also a module over `R`, the property of `M` being Artinian (meaning that every descending chain of submodules of `M` stabilizes) is equivalent to the property that the relation "less than" on the elements of `M` is well-founded (meaning that there's no infinite descending chain of elements).
More concisely: A module over a ring is Artinian if and only if the relation "less than" on its elements is well-founded.
|