Artinian rings

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

• IsArtinianRing R is the proposition that R is a left Artinian ring.

Main results

• IsArtinianRing.localization_surjective: the canonical homomorphism from a commutative artinian ring to any localization of itself is surjective.

• IsArtinianRing.isNilpotent_jacobson_bot: the Jacobson radical of a commutative artinian ring is a nilpotent ideal. (TODO: generalize to noncommutative rings.)

Implementation Details

The predicate IsArtinianRing is defined in Mathlib.RingTheory.Artinian.Ring instead, so that we can apply basic API on artinian modules to division rings without a heavy import.

References

• M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra
• [samuel]

Tags

Artinian, artinian, Artinian ring, artinian ring

theorem IsArtinianRing.isNilpotent_jacobson_bot {R : Type u_1} [CommRing R] [IsArtinianRing R] : IsNilpotent ⊥.jacobson

Stacks Tag 00J8

theorem IsArtinianRing.localization_surjective {R : Type u_1} [CommRing R] [IsArtinianRing R] (S : Submonoid R) (L : Type u_2) [CommSemiring L] [Algebra R L] [IsLocalization S L] : Function.Surjective ⇑(algebraMap R L)

Localizing an artinian ring can only reduce the amount of elements.

theorem IsArtinianRing.localization_artinian {R : Type u_1} [CommRing R] [IsArtinianRing R] (S : Submonoid R) (L : Type u_2) [CommSemiring L] [Algebra R L] [IsLocalization S L] : IsArtinianRing L

instance IsArtinianRing.instLocalization {R : Type u_1} [CommRing R] [IsArtinianRing R] (S : Submonoid R) : IsArtinianRing (Localization S)

IsArtinianRing.localization_artinian can't be made an instance, as it would make S + R into metavariables. However, this is safe.