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 #
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.
- [M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
Artinian, artinian, Artinian ring, Artinian module, artinian ring, artinian module
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.
f of submodules of a artinian module,
with the supremum
f (n+1) and the infinum of
f 0, ...,
f n being ⊤,
is eventually ⊤.
M / S / R is a scalar tower, and
M / R is Artinian, then
M / S is