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 an Artinian ring if it is Artinian as a module over itself.

(Note that we do not assume yet that our rings are commutative, so perhaps this should be called "left Artinian". To avoid cumbersome names once we specialize to the commutative case, we don't make this explicit in the declaration names.)

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.

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

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 : f.range = g.ker) :

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)

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

is_artinian R 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] :

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' → 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' → 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 order_dual (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 order_dual (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] [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) :

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

@[class]

structure is_artinian_ring (R : Type u_1) [ring R] :

Prop

to_is_artinian : is_artinian R R

A ring is Artinian if it is Artinian as a module over itself.

Instances

is_artinian_ring_range

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 is_artinian_ring_of_surjective (R : Type u_1) [comm_ring R] (S : Type u_2) [comm_ring S] (f : R →+* S) (hf : function.surjective ⇑f) [H : is_artinian_ring R] :

is_artinian_ring S

@[protected, instance]

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

is_artinian_ring ↥(f.range)

theorem is_artinian_ring_of_ring_equiv (R : Type u_1) [comm_ring R] {S : Type u_2} [comm_ring S] (f : R ≃+* S) [is_artinian_ring R] :

is_artinian_ring S

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

is_nilpotent ⊥.jacobson