mathlib documentation

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.

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 : f.range = g.ker) :
@[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)
@[instance]
theorem is_artinian_of_fintype {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [fintype M] :
@[protected, instance]
def is_artinian_pi {R : Type u_1} {ι : Type u_2} [fintype ι] {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] [fintype ι] [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] :
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 aI M'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 aI M'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 mf 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 mf 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 < IP 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] [I : is_artinian R M] (f : M →ₗ[R] M) :
∃ (n : ), n 0 (f ^ n).ker (f ^ n).range =

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

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

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] [I : 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 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 ⊤.

@[class]
structure 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.

Instances of this typeclass
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] [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 is_artinian_ring_of_surjective (R : Type u_1) [ring R] (S : Type u_2) [ring S] (f : R →+* S) (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] :
theorem is_artinian_ring_of_ring_equiv (R : Type u_1) [ring R] {S : Type u_2} [ring S] (f : R ≃+* S) [is_artinian_ring R] :