# mathlibdocumentation

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

• 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] [ M] :
Prop
• well_founded_submodule_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] [ M] [ P] (f : M →ₗ[R] P) (h : function.injective f) [ P] :
M
@[protected, instance]
def is_artinian_submodule' {R : Type u_1} {M : Type u_2} [ring R] [ M] [ M] (N : M) :
N
theorem is_artinian_of_le {R : Type u_1} {M : Type u_2} [ring R] [ M] {s t : M} [ht : t] (h : s t) :
s
theorem is_artinian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [ring R] [ M] [ P] (f : M →ₗ[R] P) (hf : function.surjective f) [ M] :
P
theorem is_artinian_of_linear_equiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [ M] [ P] (f : M ≃ₗ[R] P) [ M] :
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] [ M] [ P] [ N] [ M] [ P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : function.injective f) (hg : function.surjective g) (h : = ) :
N
@[protected, instance]
def is_artinian_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [ring R] [ M] [ P] [ M] [ P] :
(M × P)
@[protected, instance]
def is_artinian_of_finite {R : Type u_1} {M : Type u_2} [ring R] [ M] [finite M] :
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 : ι), (M i)] [∀ (i : ι), (M i)] :
(Π (i : ι), M i)
@[protected, instance]
def is_artinian_pi' {R : Type u_1} {ι : Type u_2} {M : Type u_3} [ring R] [ M] [finite ι] [ M] :
(ι → 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] [ M] :
theorem is_artinian.finite_of_linear_independent {R : Type u_1} {M : Type u_2} [ring R] [ M] [nontrivial R] [ M] {s : set M} (hs : coe) :
theorem set_has_minimal_iff_artinian {R : Type u_1} {M : Type u_2} [ring R] [ M] :
(∀ (a : set M)), a.nonempty(∃ (M' : M) (H : M' a), ∀ (I : M), I aI M'I = M')) 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] [ M] [ M] (a : set M)) (ha : a.nonempty) :
∃ (M' : M) (H : M' a), ∀ (I : M), I aI M'I = M'
theorem monotone_stabilizes_iff_artinian {R : Type u_1} {M : Type u_2} [ring R] [ M] :
(∀ (f : →o M)ᵒᵈ), ∃ (n : ), ∀ (m : ), n mf n = f m) 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] [ M] [ M] (f : →o M)ᵒᵈ) :
∃ (n : ), ∀ (m : ), n mf n = f m
theorem is_artinian.induction {R : Type u_1} {M : Type u_2} [ring R] [ M] [ M] {P : M → Prop} (hgt : ∀ (I : M), (∀ (J : M), J < IP J)P I) (I : 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] [ M] [ 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] [ M] [ M] (f : M →ₗ[R] M) (s : function.injective 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] [ M] [ M] (f : M →ₗ[R] M) (s : function.injective 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] [ M] [ M] (f : M) (h : ∀ (n : ), disjoint ( n) (order_dual.to_dual (f (n + 1)))) :
∃ (n : ), ∀ (m : ), n mf 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] [ M] [ M] (r : R) :
∃ (n : ), ∀ (m : ), n mlinear_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] [ M] [ 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
theorem is_artinian_ring_iff {R : Type u_1} [ring R] :
theorem ring.is_artinian_of_zero_eq_one {R : Type u_1} [ring R] (h01 : 0 = 1) :
theorem is_artinian_of_submodule_of_artinian (R : Type u_1) (M : Type u_2) [ring R] [ M] (N : M) (h : M) :
N
theorem is_artinian_of_quotient_of_artinian (R : Type u_1) [ring R] (M : Type u_2) [ M] (N : M) (h : M) :
(M N)
theorem is_artinian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [comm_ring R] [ring S] [ S] [ M] [ M] [ M] (h : M) :
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] [ M] (N : M) (hN : N.fg) :
N
theorem is_artinian_of_fg_of_artinian' {R : Type u_1} {M : Type u_2} [ring R] [ M] (h : .fg) :
M
theorem is_artinian_span_of_finite (R : Type u_1) {M : Type u_2} [ring R] [ M] {A : set M} (hA : A.finite) :
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} [ S] {f : F} (hf : function.surjective f) [H : is_artinian_ring R] :
@[protected, instance]
def is_artinian_ring_range {R : Type u_1} [ring R] {S : Type u_2} [ring S] (f : R →+* S)  :
theorem is_artinian_ring.localization_surjective {R : Type u_1} [comm_ring R] (S : submonoid R) (L : Type u_2) [comm_ring L] [ L] [ 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] (S : submonoid R) (L : Type u_2) [comm_ring L] [ L] [ L] :
@[protected, instance]

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