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.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).

• IsArtinian.isSemisimpleModule_iff_jacobson: an Artinian module is semisimple iff its Jacobson radical is zero.

• instIsSemiprimaryRingOfIsArtinianRing: an Artinian ring R is semiprimary, in particular the Jacobson radical of R is a nilpotent ideal (IsArtinianRing.isNilpotent_jacobson_bot).

References

• [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
• [P. Samuel, Algebraic Theory of Numbers][samuel1967]

Tags

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

@[reducible, inline]

abbrev 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.

Equations

• IsArtinian R M = WellFoundedLT (Submodule R M)

theorem isArtinian_iff (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] : IsArtinian R M ↔ WellFounded fun (x1 x2 : Submodule R M) => x1 < x2

theorem LinearMap.isArtinian_iff_of_bijective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_5} {P : Type u_6} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective ⇑l) : IsArtinian R M ↔ IsArtinian S P

theorem isArtinian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid 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} [Semiring R] [AddCommMonoid M] [Module R M] [IsArtinian R M] (N : Submodule R M) : IsArtinian R ↥N

theorem isArtinian_of_le {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {s 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} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M →ₗ[R] P) (hf : Function.Surjective ⇑f) [IsArtinian R M] : IsArtinian R P

theorem isArtinian_of_surjective_algebraMap {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_5} [CommSemiring S] [Algebra S R] [Module S M] [IsArtinian R M] [IsScalarTower S R M] (H : Function.Surjective ⇑(algebraMap S R)) : IsArtinian S M

If M is an Artinian R module, and S is an R-algebra with a surjective algebra map, then M is an Artinian S module.

instance isArtinian_range {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M →ₗ[R] P) [IsArtinian R M] : IsArtinian R ↥(LinearMap.range f)

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

theorem LinearEquiv.isArtinian_iff {R : Type u_1} {M : Type u_2} {P : Type u_3} [Semiring R] [AddCommMonoid M] [AddCommMonoid P] [Module R M] [Module R P] (f : M ≃ₗ[R] P) : IsArtinian R M ↔ IsArtinian R P

@[instance 100]

instance isArtinian_of_finite {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite M] : IsArtinian R M

theorem IsArtinian.finite_of_linearIndependent {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] [h : IsArtinian R M] {s : Set M} (hs : LinearIndependent R Subtype.val) : s.Finite

theorem set_has_minimal_iff_artinian {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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 IsArtinian.surjective_of_injective_endomorphism {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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} [Semiring R] [AddCommMonoid 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 LinearMap.eventually_iInf_range_pow_eq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [IsArtinian R M] (f : Module.End R M) : ∀ᶠ (n : ℕ) in Filter.atTop, ⨅ (m : ℕ), range (f ^ m) = range (f ^ n)

instance isArtinian_of_quotient_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 (M ⧸ N)

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) (h : LinearMap.range f = LinearMap.ker g) : IsArtinian R N

theorem isArtinian_iff_submodule_quotient {R : Type u_1} {P : Type u_3} [Ring R] [AddCommGroup P] [Module R P] (S : Submodule R P) : IsArtinian R P ↔ IsArtinian R ↥S ∧ IsArtinian R (P ⧸ S)

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)

instance isArtinian_sup {R : Type u_1} {P : Type u_3} [Ring R] [AddCommGroup P] [Module R P] (M₁ M₂ : Submodule R P) [IsArtinian R ↥M₁] [IsArtinian R ↥M₂] : IsArtinian R ↥(M₁ ⊔ M₂)

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

instance isArtinian_pi' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {ι : Type u_5} [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 ℝ).

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

instance isArtinian_iSup {R : Type u_1} {P : Type u_3} [Ring R] [AddCommGroup P] [Module R P] {ι : Type u_5} [Finite ι] {M : ι → Submodule R P} [∀ (i : ι), IsArtinian R ↥(M i)] : IsArtinian R ↥(⨆ (i : ι), M i)

theorem IsArtinian.isSemisimpleModule_iff_jacobson (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] : IsSemisimpleModule R M ↔ Module.jacobson R M = ⊥

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 : Module.End R M) : ∀ᶠ (n : ℕ) in Filter.atTop, Codisjoint (ker (f ^ n)) (range (f ^ n))

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

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 : Module.End R M) : ∀ᶠ (n : ℕ) in Filter.atTop, IsCompl (ker (f ^ n)) (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 : ℕ), ker (f ^ n)) (⨅ (n : ℕ), 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.range_smul_pow_stabilizes {R : Type u_1} (M : Type u_2) [CommSemiring R] [AddCommMonoid 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} [CommSemiring R] [AddCommMonoid M] [Module R M] [IsArtinian R M] (r : R) (x : M) : ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x

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

theorem isArtinian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [SMul 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.

@[reducible, inline]

abbrev IsArtinianRing (R : Type u_1) [Semiring 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.

For equivalent definitions, see Mathlib/RingTheory/Artinian/Ring.lean.

Stacks Tag 00J5

Equations

• IsArtinianRing R = IsArtinian R R

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

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

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

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

instance instIsArtinianRingQuotientIdeal (R : Type u_1) [Ring R] [IsArtinianRing R] (I : Ideal R) [I.IsTwoSided] : IsArtinianRing (R ⧸ I)

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

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

theorem IsArtinianRing.of_finite (R : Type u_1) (S : Type u_2) [Ring R] [Ring S] [Module R S] [IsScalarTower R S 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} [Semiring R] {S : Type u_2} [Semiring S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Surjective ⇑f) [H : IsArtinianRing R] : IsArtinianRing S

instance isArtinianRing_rangeS {R : Type u_1} [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) [IsArtinianRing R] : IsArtinianRing ↥f.rangeS

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

theorem RingEquiv.isArtinianRing {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R ≃+* S) [IsArtinianRing R] : IsArtinianRing S

instance instIsArtinianRingProd {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [IsArtinianRing R] [IsArtinianRing S] : IsArtinianRing (R × S)

instance instIsArtinianRingForallOfFinite {ι : Type u_2} [Finite ι] {R : ι → Type u_1} [(i : ι) → Semiring (R i)] [∀ (i : ι), IsArtinianRing (R i)] : IsArtinianRing ((i : ι) → R i)

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

Stacks Tag 00J7

instance IsArtinianRing.instFiniteMaximalSpectrum (R : Type u_1) [CommSemiring R] [IsArtinianRing R] : Finite (MaximalSpectrum R)

theorem IsArtinianRing.isField_of_isDomain (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsDomain R] : IsField R

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

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

def IsArtinianRing.primeSpectrumEquivMaximalSpectrum {R : Type u_1} [CommRing R] [IsArtinianRing R] : PrimeSpectrum R ≃ MaximalSpectrum R

The prime spectrum is in bijection with the maximal spectrum.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal {R : Type u_1} [CommRing R] [IsArtinianRing R] (I : PrimeSpectrum R) : (primeSpectrumEquivMaximalSpectrum I).asIdeal = I.asIdeal

@[simp]

theorem IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal {R : Type u_1} [CommRing R] [IsArtinianRing R] (I : MaximalSpectrum R) : (primeSpectrumEquivMaximalSpectrum.symm I).asIdeal = I.asIdeal

theorem IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal {R : Type u_1} [CommRing R] [IsArtinianRing R] : MaximalSpectrum.asIdeal ∘ ⇑primeSpectrumEquivMaximalSpectrum = PrimeSpectrum.asIdeal

theorem IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal {R : Type u_1} [CommRing R] [IsArtinianRing R] : PrimeSpectrum.asIdeal ∘ ⇑primeSpectrumEquivMaximalSpectrum.symm = MaximalSpectrum.asIdeal

theorem IsArtinianRing.primeSpectrum_asIdeal_range_eq {R : Type u_1} [CommRing R] [IsArtinianRing R] : Set.range PrimeSpectrum.asIdeal = Set.range MaximalSpectrum.asIdeal

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

instance IsArtinianRing.instFinitePrimeSpectrum (R : Type u_1) [CommRing R] [IsArtinianRing R] : Finite (PrimeSpectrum R)

noncomputable def IsArtinianRing.fieldOfSubtypeIsMaximal (R : Type u_1) [CommRing R] (I : MaximalSpectrum R) : Field (R ⧸ I.asIdeal)

A temporary field instance on the quotients by maximal ideals.

Equations

• IsArtinianRing.fieldOfSubtypeIsMaximal R I = Ideal.Quotient.field I.asIdeal

noncomputable def IsArtinianRing.quotNilradicalEquivPi (R : Type u_1) [CommRing R] [IsArtinianRing R] : R ⧸ nilradical R ≃+* ((I : MaximalSpectrum R) → R ⧸ I.asIdeal)

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 MaximalSpectrum.asIdeal ⋯)

noncomputable def IsArtinianRing.equivPi (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] : R ≃+* ((I : MaximalSpectrum R) → R ⧸ I.asIdeal)

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))

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

theorem IsArtinianRing.isSemisimpleRing_iff_jacobson {R : Type u_1} [Ring R] [IsArtinianRing R] : IsSemisimpleRing R ↔ Ring.jacobson R = ⊥

instance IsArtinianRing.instIsSemiprimaryRing {R : Type u_1} [Ring R] [IsArtinianRing R] : IsSemiprimaryRing R