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.

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

• wellFounded_submodule_lt' : WellFounded fun x x_1 => x < x_1

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

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 => 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 { x // x ∈ N }

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 { x // x ∈ t }] (h : s ≤ t) : IsArtinian R { x // x ∈ 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)

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

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)

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

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)

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 => 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 R Subtype.val) : Set.Finite s

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)), Set.Nonempty a → ∃ M', M' ∈ a ∧ ∀ (I : Submodule R M), 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 : Set.Nonempty a) : ∃ M', M' ∈ a ∧ ∀ (I : Submodule R M), 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.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 : 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.exists_endomorphism_iterate_ker_sup_range_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : M →ₗ[R] M) : ∃ n, n ≠ 0 ∧ LinearMap.ker (f ^ n) ⊔ LinearMap.range (f ^ n) = ⊤

For any endomorphism of an Artinian module, there is some nontrivial iterate with disjoint kernel and range.

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, r ^ Nat.succ n • y = r ^ n • x

@[reducible]

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

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

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 { x // x ∈ 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)

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 instIsArtinianRingQuotientIdealToSemiringToCommSemiringInstHasQuotientIdealToSemiringToCommSemiringToRingCommRing (R : Type u_1) [CommRing R] [IsArtinianRing R] (I : Ideal R) : IsArtinianRing (R ⧸ I)

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 : Submodule.FG N) : IsArtinian R { x // x ∈ N }

theorem isArtinian_of_fg_of_artinian' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] (h : Submodule.FG ⊤) : IsArtinian R M

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 : Set.Finite A) : IsArtinian R { x // x ∈ 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} [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 { x // x ∈ RingHom.range f }

theorem IsArtinianRing.isNilpotent_jacobson_bot {R : Type u_1} [CommRing R] [IsArtinianRing R] : IsNilpotent (Ideal.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.instIsArtinianRingLocalizationToCommMonoidToRingInstCommRingLocalizationToCommMonoid {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.

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