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
.
is_artinian R M
is the proposition thatM
is a ArtinianR
-module. It is a class, implemented as the predicate that the<
relation on submodules is well founded.is_artinian_ring R
is the proposition thatR
is a left Artinian ring.
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
- 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.
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 ℝ
).
A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.
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.
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 ⊤.
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
- is_artinian_ring R = is_artinian R R
If M / S / R
is a scalar tower, and M / R
is Artinian, then M / S
is
also Artinian.
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 S
+ R
into metavariables. However, this is safe.