HepLean Documentation

Mathlib.RingTheory.Artinian

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

@[reducible, inline]

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

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)

Instances For

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 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] :

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] :

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)

Equations

⋯ = ⋯

instance isArtinian_range {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 ↥(LinearMap.range f)

Equations

⋯ = ⋯

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] :

theorem LinearEquiv.isArtinian_iff {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) (h : LinearMap.range f = LinearMap.ker g) :

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)

Equations

⋯ = ⋯

@[instance 100]

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

Equations

⋯ = ⋯

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

IsArtinian R ↥(M₁ ⊔ M₂)

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

theorem IsArtinian.finite_of_linearIndependent {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup 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} [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] :

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

Instances For

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

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

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] :

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 = Ideal.Quotient.field ↑I

Instances For

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

Instances For

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

Instances For

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