Idempotents and locality in Henselian rings

A commutative ring that is Henselian along an ideal J lifts idempotents from S ⧸ J: an idempotent is a root of X² - X, and every root of X² - X modulo J is simple, since (2a - 1)² = 4(a² - a) + 1. Consequently, when S ⧸ J is Artinian, the idempotents of S control whether S is local. An Artinian ring with only the trivial idempotents is local, and a ring whose quotient by an ideal in its Jacobson radical is local is itself local.

The typical example is a finite algebra over a complete Noetherian local ring, Henselian along the extension of the maximal ideal: such an algebra with no nontrivial idempotents is local. This is the mechanism behind the locality of endomorphism rings of indecomposable modules over complete local rings.

Main results

• TauCeti.IsArtinianRing.isLocalRing_of_forall_isIdempotentElem: a nontrivial commutative Artinian ring whose only idempotents are 0 and 1 is local.
• TauCeti.HenselianRing.exists_isIdempotentElem_sub_mem: idempotents lift modulo an ideal along which the ring is Henselian.
• TauCeti.HenselianRing.isLocalRing_of_forall_isIdempotentElem: a nontrivial commutative ring, Henselian along an ideal with Artinian quotient, whose only idempotents are 0 and 1, is local.

References

• C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, §6.
• T. Y. Lam, A First Course in Noncommutative Rings, §21 and §23.

theorem TauCeti.IsArtinianRing.isLocalRing_of_forall_isIdempotentElem {S : Type u_1} [CommRing S] [IsArtinianRing S] [Nontrivial S] (h : ∀ (e : S), IsIdempotentElem e → e = 0 ∨ e = 1) : IsLocalRing S

A connected Artinian ring is local. A nontrivial commutative Artinian ring whose only idempotents are 0 and 1 is local.

theorem TauCeti.HenselianRing.exists_isIdempotentElem_sub_mem {S : Type u_1} [CommRing S] (J : Ideal S) [HenselianRing S J] {a : S} (ha : a * a - a ∈ J) : ∃ (e : S), IsIdempotentElem e ∧ e - a ∈ J

Idempotents lift along a Henselian pair. If S is Henselian along J and a is idempotent modulo J, then some idempotent of S is congruent to a modulo J.

theorem TauCeti.HenselianRing.isLocalRing_of_forall_isIdempotentElem {S : Type u_1} [CommRing S] [Nontrivial S] (J : Ideal S) [HenselianRing S J] [IsArtinianRing (S ⧸ J)] (h : ∀ (e : S), IsIdempotentElem e → e = 0 ∨ e = 1) : IsLocalRing S

Locality from the idempotents. A nontrivial commutative ring that is Henselian along an ideal J with S ⧸ J Artinian, and whose only idempotents are 0 and 1, is local.