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.

References #

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

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] :
@[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) :
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) :
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] :
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] :
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) :
@[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] :
@[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.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.

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

Any injective endomorphism of an Artinian module is surjective.

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.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
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] [add_comm_group M] [module R M] (N : submodule R M) (h : is_artinian R M) :
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) :
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) :

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

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

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

@[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.