Artinian rings and modules

A module satisfying these equivalent conditions is said to be an Artinian R-module if every decreasing chain of submodules is eventually constant, or equivalently, if the relation < on submodules is well founded.

A ring is said to be left (or right) Artinian if it is Artinian as a left (or right) module over itself, or simply Artinian if it is both left and right Artinian.

Main definitions

Let R be a ring and let M and P be R-modules. Let N be an R-submodule of M.

• IsArtinian R M is the proposition that M is an Artinian R-module. It is a class, implemented as the predicate that the < relation on submodules is well founded.
• IsArtinianRing R is the proposition that R is a left Artinian ring.

Main results

• IsArtinianRing.localization_surjective: the canonical homomorphism from a commutative artinian ring to any localization of itself is surjective.

• IsArtinianRing.isNilpotent_jacobson_bot: the Jacobson radical of a commutative artinian ring is a nilpotent ideal. (TODO: generalize to noncommutative rings.)

• IsArtinianRing.primeSpectrum_finite, IsArtinianRing.isMaximal_of_isPrime: there are only finitely prime ideals in a commutative artinian ring, and each of them is maximal.

• IsArtinianRing.equivPi: a reduced commutative artinian ring R is isomorphic to a finite product of fields (and therefore is a semisimple ring and a decomposition monoid; moreover R[X] is also a decomposition monoid).

References

• [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
• [samuel]

Tags

Artinian, artinian, Artinian ring, Artinian module, artinian ring, artinian module

class IsArtinian (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : Prop

IsArtinian R M is the proposition that M is an Artinian R-module, implemented as the well-foundedness of submodule inclusion.

• wellFounded_submodule_lt' : WellFounded fun (x x_1 : Submodule R M) => x < x_1

theorem IsArtinian.wellFounded_submodule_lt' {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [self : IsArtinian R M] : WellFounded fun (x x_1 : Submodule R M) => x < x_1

theorem IsArtinian.wellFounded_submodule_lt (R : Type u_5) (M : Type u_6) [Semiring R] [AddCommMonoid M] [Module R M] [IsArtinian R M] : WellFounded fun (x x_1 : Submodule R M) => x < x_1

theorem isArtinian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (f : M →ₗ[R] P) (h : Function.Injective ⇑f) [IsArtinian R P] : IsArtinian R M

instance isArtinian_submodule' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (N : Submodule R M) : IsArtinian R ↥N

Equations

• ⋯ = ⋯

theorem isArtinian_of_le {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {t : Submodule R M} [IsArtinian R ↥t] (h : s ≤ t) : IsArtinian R ↥s

theorem isArtinian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (f : M →ₗ[R] P) (hf : Function.Surjective ⇑f) [IsArtinian R M] : IsArtinian R P

theorem isArtinian_of_linearEquiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (f : M ≃ₗ[R] P) [IsArtinian R M] : IsArtinian R P

theorem isArtinian_of_range_eq_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup N] [Module R M] [Module R P] [Module R N] [IsArtinian R M] [IsArtinian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) (h : LinearMap.range f = LinearMap.ker g) : IsArtinian R N

instance isArtinian_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsArtinian R M] [IsArtinian R P] : IsArtinian R (M × P)

Equations

• ⋯ = ⋯

@[instance 100]

instance isArtinian_of_finite {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Finite M] : IsArtinian R M

Equations

• ⋯ = ⋯

instance isArtinian_pi {R : Type u_5} {ι : Type u_6} [Finite ι] {M : ι → Type u_7} [Ring R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), IsArtinian R (M i)] : IsArtinian R ((i : ι) → M i)

Equations

• ⋯ = ⋯

instance isArtinian_pi' {R : Type u_5} {ι : Type u_6} {M : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [Finite ι] [IsArtinian R M] : IsArtinian R (ι → M)

A version of isArtinian_pi for non-dependent functions. We need this instance because sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to prove that ι → ℝ is finite dimensional over ℝ).

Equations

• ⋯ = ⋯

instance isArtinian_finsupp {R : Type u_5} {ι : Type u_6} {M : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [Finite ι] [IsArtinian R M] : IsArtinian R (ι →₀ M)

Equations

• ⋯ = ⋯

theorem isArtinian_iff_wellFounded {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : IsArtinian R M ↔ WellFounded fun (x x_1 : Submodule R M) => x < x_1

theorem IsArtinian.finite_of_linearIndependent {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [IsArtinian R M] {s : Set M} (hs : LinearIndependent (ι := { x : M // x ∈ s }) R Subtype.val) : s.Finite

theorem set_has_minimal_iff_artinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M

A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.

theorem IsArtinian.set_has_minimal {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (a : Set (Submodule R M)) (ha : a.Nonempty) : ∃ M' ∈ a, ∀ I ∈ a, ¬I < M'

theorem monotone_stabilizes_iff_artinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : (∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsArtinian R M

A module is Artinian iff every decreasing chain of submodules stabilizes.

theorem IsArtinian.monotone_stabilizes {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : ℕ →o (Submodule R M)ᵒᵈ) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

theorem IsArtinian.eventuallyConst_of_isArtinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : ℕ →o (Submodule R M)ᵒᵈ) : Filter.EventuallyConst (⇑f) Filter.atTop

theorem IsArtinian.induction {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] {P : Submodule R M → Prop} (hgt : ∀ (I : Submodule R M), (∀ J < I, P J) → P I) (I : Submodule R M) : P I

If ∀ I > J, P I implies P J, then P holds for all submodules.

theorem LinearMap.eventually_codisjoint_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : M →ₗ[R] M) : ∀ᶠ (n : ℕ) in Filter.atTop, Codisjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

For any endomorphism of an Artinian module, any sufficiently high iterate has codisjoint kernel and range.

theorem LinearMap.eventually_iInf_range_pow_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : Module.End R M) : ∀ᶠ (n : ℕ) in Filter.atTop, ⨅ (m : ℕ), LinearMap.range (f ^ m) = LinearMap.range (f ^ n)

theorem LinearMap.eventually_isCompl_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (f : M →ₗ[R] M) : ∀ᶠ (n : ℕ) in Filter.atTop, IsCompl (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

This is the Fitting decomposition of the module M with respect to the endomorphism f.

See also LinearMap.isCompl_iSup_ker_pow_iInf_range_pow for an alternative spelling.

theorem LinearMap.isCompl_iSup_ker_pow_iInf_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (f : M →ₗ[R] M) : IsCompl (⨆ (n : ℕ), LinearMap.ker (f ^ n)) (⨅ (n : ℕ), LinearMap.range (f ^ n))

This is the Fitting decomposition of the module M with respect to the endomorphism f.

See also LinearMap.eventually_isCompl_ker_pow_range_pow for an alternative spelling.

theorem IsArtinian.surjective_of_injective_endomorphism {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : M →ₗ[R] M) (s : Function.Injective ⇑f) : Function.Surjective ⇑f

Any injective endomorphism of an Artinian module is surjective.

theorem IsArtinian.bijective_of_injective_endomorphism {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : M →ₗ[R] M) (s : Function.Injective ⇑f) : Function.Bijective ⇑f

Any injective endomorphism of an Artinian module is bijective.

theorem IsArtinian.disjoint_partial_infs_eventually_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : ℕ → Submodule R M) (h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤

A sequence f of submodules of an artinian module, with the supremum f (n+1) and the infimum of f 0, ..., f n being ⊤, is eventually ⊤.

theorem IsArtinian.range_smul_pow_stabilizes {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsArtinian R M] (r : R) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)

theorem IsArtinian.exists_pow_succ_smul_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsArtinian R M] (r : R) (x : M) : ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x

@[reducible, inline]

abbrev IsArtinianRing (R : Type u_1) [Ring R] : Prop

A ring is Artinian if it is Artinian as a module over itself.

Strictly speaking, this should be called IsLeftArtinianRing but we omit the Left for convenience in the commutative case. For a right Artinian ring, use IsArtinian Rᵐᵒᵖ R.

Equations

• IsArtinianRing R = IsArtinian R R

theorem isArtinianRing_iff {R : Type u_1} [Ring R] : IsArtinianRing R ↔ IsArtinian R R

instance DivisionRing.instIsArtinianRing {K : Type u_1} [DivisionRing K] : IsArtinianRing K

Equations

• ⋯ = ⋯

theorem Ring.isArtinian_of_zero_eq_one {R : Type u_1} [Ring R] (h01 : 0 = 1) : IsArtinianRing R

theorem isArtinian_of_submodule_of_artinian (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) : IsArtinian R M → IsArtinian R ↥N

instance isArtinian_of_quotient_of_artinian (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] (N : Submodule R M) [IsArtinian R M] : IsArtinian R (M ⧸ N)

Equations

• ⋯ = ⋯

theorem isArtinian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [CommRing R] [Ring S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] (h : IsArtinian R M) : IsArtinian S M

If M / S / R is a scalar tower, and M / R is Artinian, then M / S is also Artinian.

instance instIsArtinianRingQuotientIdeal (R : Type u_1) [CommRing R] [IsArtinianRing R] (I : Ideal R) : IsArtinianRing (R ⧸ I)

Equations

• ⋯ = ⋯

theorem isArtinian_of_fg_of_artinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsArtinianRing R] (hN : N.FG) : IsArtinian R ↥N

instance isArtinian_of_fg_of_artinian' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] [Module.Finite R M] : IsArtinian R M

Equations

• ⋯ = ⋯

theorem IsArtinianRing.of_finite (R : Type u_1) (S : Type u_2) [CommRing R] [Ring S] [Algebra R S] [IsArtinianRing R] [Module.Finite R S] : IsArtinianRing S

theorem isArtinian_span_of_finite (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] {A : Set M} (hA : A.Finite) : IsArtinian R ↥(Submodule.span R A)

In a module over an artinian ring, the submodule generated by finitely many vectors is artinian.

theorem Function.Surjective.isArtinianRing {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective ⇑f) [H : IsArtinianRing R] : IsArtinianRing S

instance isArtinianRing_range {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (f : R →+* S) [IsArtinianRing R] : IsArtinianRing ↥f.range

Equations

• ⋯ = ⋯

theorem IsArtinianRing.isNilpotent_jacobson_bot {R : Type u_1} [CommRing R] [IsArtinianRing R] : IsNilpotent ⊥.jacobson

theorem IsArtinianRing.localization_surjective {R : Type u_1} [CommRing R] [IsArtinianRing R] (S : Submonoid R) (L : Type u_2) [CommRing L] [Algebra R L] [IsLocalization S L] : Function.Surjective ⇑(algebraMap R L)

Localizing an artinian ring can only reduce the amount of elements.

theorem IsArtinianRing.localization_artinian {R : Type u_1} [CommRing R] [IsArtinianRing R] (S : Submonoid R) (L : Type u_2) [CommRing L] [Algebra R L] [IsLocalization S L] : IsArtinianRing L

instance IsArtinianRing.instLocalization {R : Type u_1} [CommRing R] [IsArtinianRing R] (S : Submonoid R) : IsArtinianRing (Localization S)

IsArtinianRing.localization_artinian can't be made an instance, as it would make S + R into metavariables. However, this is safe.

Equations

• ⋯ = ⋯

instance IsArtinianRing.isMaximal_of_isPrime {R : Type u_1} [CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime] : p.IsMaximal

Equations

• ⋯ = ⋯

theorem IsArtinianRing.isPrime_iff_isMaximal {R : Type u_1} [CommRing R] [IsArtinianRing R] (p : Ideal R) : p.IsPrime ↔ p.IsMaximal

theorem IsArtinianRing.primeSpectrum_finite (R : Type u_1) [CommRing R] [IsArtinianRing R] : {I : Ideal R | I.IsPrime}.Finite

theorem IsArtinianRing.maximal_ideals_finite (R : Type u_1) [CommRing R] [IsArtinianRing R] : {I : Ideal R | I.IsMaximal}.Finite

Stacks Lemma 00J7

theorem IsArtinianRing.subtype_isMaximal_finite (R : Type u_1) [CommRing R] [IsArtinianRing R] : Finite ↑{I : Ideal R | I.IsMaximal}

noncomputable def IsArtinianRing.fieldOfSubtypeIsMaximal (R : Type u_1) [CommRing R] (I : ↑{I : Ideal R | I.IsMaximal}) : Field (R ⧸ ↑I)

A temporary field instance on the quotients by maximal ideals.

Equations

• IsArtinianRing.fieldOfSubtypeIsMaximal R I = let_fun this := ⋯; Ideal.Quotient.field ↑I

noncomputable def IsArtinianRing.quotNilradicalEquivPi (R : Type u_1) [CommRing R] [IsArtinianRing R] : R ⧸ nilradical R ≃+* ((I : ↑{I : Ideal R | I.IsMaximal}) → R ⧸ ↑I)

The quotient of a commutative artinian ring by its nilradical is isomorphic to a finite product of fields, namely the quotients by the maximal ideals.

Equations

• IsArtinianRing.quotNilradicalEquivPi R = (Ideal.quotEquivOfEq ⋯).trans (Ideal.quotientInfRingEquivPiQuotient Subtype.val ⋯)

noncomputable def IsArtinianRing.equivPi (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : R ≃+* ((I : ↑{I : Ideal R | I.IsMaximal}) → R ⧸ ↑I)

A reduced commutative artinian ring is isomorphic to a finite product of fields, namely the quotients by the maximal ideals.

Equations

• IsArtinianRing.equivPi R = (RingEquiv.quotientBot R).symm.trans ((Ideal.quotEquivOfEq ⋯).trans (IsArtinianRing.quotNilradicalEquivPi R))

instance IsArtinianRing.instDecompositionMonoidOfIsReduced (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : DecompositionMonoid R

Equations

• ⋯ = ⋯

instance IsArtinianRing.instDecompositionMonoidPolynomialOfIsReduced (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : DecompositionMonoid (Polynomial R)

Equations

• ⋯ = ⋯

theorem IsArtinianRing.isSemisimpleRing_of_isReduced (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : IsSemisimpleRing R