mathlib3 documentation

ring_theory.artinian

Artinian rings and modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

is_artinian R M is the proposition that M is a Artinian R-module. It is a class, implemented as the predicate that the < relation on submodules is well founded.
is_artinian_ring 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]

structure is_artinian (R : Type u_1) (M : Type u_2) [semiring R] [add_comm_monoid M] [module R M] :

Prop

well_founded_submodule_lt : well_founded has_lt.lt

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

Instances of this typeclass

theorem is_artinian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] (f : M →ₗ[R] P) (h : function.injective ⇑f) [is_artinian R P] :

is_artinian R M

@[protected, instance]

def is_artinian_submodule' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (N : submodule R M) :

is_artinian R ↥N

theorem is_artinian_of_le {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] {s t : submodule R M} [ht : is_artinian R ↥t] (h : s ≤ t) :

is_artinian R ↥s

theorem is_artinian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] (f : M →ₗ[R] P) (hf : function.surjective ⇑f) [is_artinian R M] :

is_artinian R P

theorem is_artinian_of_linear_equiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] (f : M ≃ₗ[R] P) [is_artinian R M] :

is_artinian R P

theorem is_artinian_of_range_eq_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type u_4} [ring R] [add_comm_group M] [add_comm_group P] [add_comm_group N] [module R M] [module R P] [module R N] [is_artinian R M] [is_artinian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : function.injective ⇑f) (hg : function.surjective ⇑g) (h : linear_map.range f = linear_map.ker g) :

is_artinian R N

@[protected, instance]

def is_artinian_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [add_comm_group M] [add_comm_group P] [module R M] [module R P] [is_artinian R M] [is_artinian R P] :

is_artinian R (M × P)

@[protected, instance]

def is_artinian_of_finite {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [finite M] :

is_artinian R M

@[protected, instance]

def is_artinian_pi {R : Type u_1} {ι : Type u_2} [finite ι] {M : ι → Type u_3} [ring R] [Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [∀ (i : ι), is_artinian R (M i)] :

is_artinian R (Π (i : ι), M i)

@[protected, instance]

def is_artinian_pi' {R : Type u_1} {ι : Type u_2} {M : Type u_3} [ring R] [add_comm_group M] [module R M] [finite ι] [is_artinian R M] :

is_artinian R (ι → M)

A version of is_artinian_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 ℝ).

theorem is_artinian_iff_well_founded {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :

is_artinian R M ↔ well_founded has_lt.lt

theorem is_artinian.finite_of_linear_independent {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [nontrivial R] [is_artinian R M] {s : set M} (hs : linear_independent R coe) :

theorem set_has_minimal_iff_artinian {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] :

(∀ (a : set (submodule R M)), a.nonempty → (∃ (M' : submodule R M) (H : M' ∈ a), ∀ (I : submodule R M), I ∈ a → ¬I < M')) ↔ is_artinian R M

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

theorem is_artinian.set_has_minimal {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (a : set (submodule R M)) (ha : a.nonempty) :

∃ (M' : submodule R M) (H : 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] [add_comm_group M] [module R M] :

(∀ (f : ℕ →o (submodule R M)ᵒᵈ), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ⇑f n = ⇑f m) ↔ is_artinian R M

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

theorem is_artinian.monotone_stabilizes {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (f : ℕ →o (submodule R M)ᵒᵈ) :

∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ⇑f n = ⇑f m

theorem is_artinian.induction {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian 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 is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (f : M →ₗ[R] M) :

∃ (n : ℕ), n ≠ 0 ∧ linear_map.ker (f ^ n) ⊔ linear_map.range (f ^ n) = ⊤

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

theorem is_artinian.surjective_of_injective_endomorphism {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (f : M →ₗ[R] M) (s : function.injective ⇑f) :

function.surjective ⇑f

Any injective endomorphism of an Artinian module is surjective.

theorem is_artinian.bijective_of_injective_endomorphism {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (f : M →ₗ[R] M) (s : function.injective ⇑f) :

function.bijective ⇑f

Any injective endomorphism of an Artinian module is bijective.

theorem is_artinian.disjoint_partial_infs_eventually_top {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian R M] (f : ℕ → submodule R M) (h : ∀ (n : ℕ), disjoint (⇑(partial_sups (⇑order_dual.to_dual ∘ f)) n) (⇑order_dual.to_dual (f (n + 1)))) :

∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊤

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

theorem is_artinian.range_smul_pow_stabilizes {R : Type u_1} (M : Type u_2) [comm_ring R] [add_comm_group M] [module R M] [is_artinian R M] (r : R) :

∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → linear_map.range (r ^ n • linear_map.id) = linear_map.range (r ^ m • linear_map.id)

theorem is_artinian.exists_pow_succ_smul_dvd {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] [is_artinian R M] (r : R) (x : M) :

∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x

@[reducible]

def is_artinian_ring (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 is_left_artinian_ring but we omit the left_ for convenience in the commutative case. For a right Artinian ring, use is_artinian Rᵐᵒᵖ R.

Equations

is_artinian_ring R = is_artinian R R

theorem is_artinian_ring_iff {R : Type u_1} [ring R] :

is_artinian_ring R ↔ is_artinian R R

theorem ring.is_artinian_of_zero_eq_one {R : Type u_1} [ring R] (h01 : 0 = 1) :

is_artinian_ring R

theorem is_artinian_of_submodule_of_artinian (R : Type u_1) (M : Type u_2) [ring R] [add_comm_group M] [module R M] (N : submodule R M) (h : is_artinian R M) :

is_artinian R ↥N

theorem is_artinian_of_quotient_of_artinian (R : Type u_1) [ring R] (M : Type u_2) [add_comm_group M] [module R M] (N : submodule R M) (h : is_artinian R M) :

is_artinian R (M ⧸ N)

theorem is_artinian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [comm_ring R] [ring S] [add_comm_group M] [algebra R S] [module S M] [module R M] [is_scalar_tower R S M] (h : is_artinian R M) :

is_artinian S M

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

theorem is_artinian_of_fg_of_artinian {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] (N : submodule R M) [is_artinian_ring R] (hN : N.fg) :

is_artinian R ↥N

theorem is_artinian_of_fg_of_artinian' {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian_ring R] (h : ⊤.fg) :

is_artinian R M

theorem is_artinian_span_of_finite (R : Type u_1) {M : Type u_2} [ring R] [add_comm_group M] [module R M] [is_artinian_ring R] {A : set M} (hA : A.finite) :

is_artinian R ↥(submodule.span R A)

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

theorem function.surjective.is_artinian_ring {R : Type u_1} [ring R] {S : Type u_2} [ring S] {F : Type u_3} [ring_hom_class F R S] {f : F} (hf : function.surjective ⇑f) [H : is_artinian_ring R] :

is_artinian_ring S

@[protected, instance]

def is_artinian_ring_range {R : Type u_1} [ring R] {S : Type u_2} [ring S] (f : R →+* S) [is_artinian_ring R] :

is_artinian_ring ↥(f.range)

theorem is_artinian_ring.is_nilpotent_jacobson_bot {R : Type u_1} [comm_ring R] [is_artinian_ring R] :

is_nilpotent ⊥.jacobson

theorem is_artinian_ring.localization_surjective {R : Type u_1} [comm_ring R] [is_artinian_ring R] (S : submonoid R) (L : Type u_2) [comm_ring L] [algebra R L] [is_localization S L] :

function.surjective ⇑(algebra_map R L)

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

theorem is_artinian_ring.localization_artinian {R : Type u_1} [comm_ring R] [is_artinian_ring R] (S : submonoid R) (L : Type u_2) [comm_ring L] [algebra R L] [is_localization S L] :

is_artinian_ring L

@[protected, instance]

def is_artinian_ring.localization.is_artinian_ring {R : Type u_1} [comm_ring R] [is_artinian_ring R] (S : submonoid R) :

is_artinian_ring (localization S)

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