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 #
R be a ring and let
N be an
is_artinian R Mis the proposition that
Mis a Artinian
R-module. It is a class, implemented as the predicate that the
<relation on submodules is well founded.
is_artinian_ring Ris the proposition that
Ris a left Artinian ring.
- [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
Artinian, artinian, Artinian ring, Artinian module, artinian ring, artinian module
- well_founded_submodule_lt : well_founded has_lt.lt
is_artinian R M is the proposition that
M is an Artinian
implemented as the well-foundedness of submodule inclusion.
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
ι → ℝ is finite dimensional over
A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.
∀ 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.
f of submodules of a artinian module,
with the supremum
f (n+1) and the infinum of
f 0, ...,
f n being ⊤,
is eventually ⊤.
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
convenience in the commutative case. For a right Artinian ring, use
is_artinian Rᵐᵒᵖ R.
- is_artinian_ring R = is_artinian R R
M / S / R is a scalar tower, and
M / R is Artinian, then
M / S is
In a module over a artinian ring, the submodule generated by finitely many vectors is artinian.
Localizing an artinian ring can only reduce the amount of elements.
is_artinian_ring.localization_artinian can't be made an instance, as it would make
into metavariables. However, this is safe.