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.

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} [Ring R] [IsArtinianRing R] : IsNilpotent ⊥.jacobson

Stacks Tag 00J8

theorem IsArtinianRing.jacobson_eq_radical {R : Type u_1} [CommRing R] [IsArtinianRing R] (I : Ideal R) : I.jacobson = I.radical

theorem IsArtinianRing.isNilpotent_nilradical {R : Type u_1} [CommRing R] [IsArtinianRing R] : IsNilpotent (nilradical R)

theorem IsArtinianRing.isField_of_isReduced_of_isLocalRing (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] [IsLocalRing R] : IsField R

Commutative artinian reduced local ring is a field.

theorem IsArtinianRing.isUnit_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] [IsArtinianRing R] {a : R} (ha : a ∈ nonZeroDivisors R) : IsUnit a

If an element of an artinian ring is not a zero divisor then it is a unit.

theorem IsArtinianRing.isUnit_iff_mem_nonZeroDivisors {R : Type u_1} [CommRing R] [IsArtinianRing R] {a : R} : IsUnit a ↔ a ∈ nonZeroDivisors R

In an artinian ring, an element is a unit iff it is a non-zero-divisor. See also isUnit_iff_mem_nonZeroDivisors_of_finite.

theorem IsArtinianRing.isUnit_submonoid_eq {R : Type u_1} [CommRing R] [IsArtinianRing R] : IsUnit.submonoid R = nonZeroDivisors R

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.