Idempotents modulo an ideal in the Jacobson radical

In any ring, an idempotent e in the Jacobson radical is zero: 1 - e has a left inverse and (1 - e) e = 0. Consequently, in a commutative ring, idempotents are determined by their residues modulo any ideal I contained in the Jacobson radical. If e and e' are idempotents with e - e' in I, then e (1 - e') and (1 - e) e' are idempotents in the Jacobson radical, hence zero, and e - e' = e (1 - e') - (1 - e) e' = 0.

This is the uniqueness half of lifting idempotents along a Henselian pair, and it needs no Henselian hypothesis. The second step needs commutativity: for example, in the upper triangular 2 × 2 matrices over a field, E₁₁ and E₁₁ + E₁₂ are distinct idempotents whose difference lies in the Jacobson radical.

Main results

• IsIdempotentElem.eq_zero_of_mem_jacobson_bot: an idempotent in the Jacobson radical Ideal.jacobson ⊥ of a not necessarily commutative ring is zero.
• Ideal.Quotient.isIdempotentElem_mk_iff: a is idempotent modulo I if and only if a * a - a ∈ I.
• IsIdempotentElem.eq_of_sub_mem_of_le_jacobson_bot: idempotents congruent modulo an ideal in the Jacobson radical are equal.
• Ideal.injOn_quotient_mk_isIdempotentElem: modulo an ideal in the Jacobson radical, the quotient map is injective on idempotents.
• IsIdempotentElem.exists_smul_eq_mul_of_mul_sub_smul_mem: in a module-finite S-algebra T, an idempotent e with e T ⊆ S e + JT, for J in the Jacobson radical of S, has e T = S e.

References

• Stacks Project, Lemma 15.11.6, the uniqueness of lifts in condition (3).
• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit a39c3781b9850b9f3d5cbc9920322a3b8e365ef2 (Apache-2.0), lean/Pcf/Stacks/Purity/HenselianIdempotents.lean: eq_zero_of_mem_jacobson_bot and eq_of_sub_mem_of_le_jacobson_bot are its Pcf.Stacks.isIdempotentElem_eq_zero_of_mem_jacobson and Pcf.Stacks.eq_of_isIdempotentElem_of_sub_mem_of_le_jacobson, and injOn_quotient_mk_isIdempotentElem restates as Set.InjOn the injectivity step of its Pcf.Stacks.bijective_idempotentQuotientMap_of_henselian.

theorem IsIdempotentElem.eq_zero_of_mem_jacobson_bot {R : Type u_1} [Ring R] {e : R} (he : IsIdempotentElem e) (hJ : e ∈ ⊥.jacobson) : e = 0

An idempotent in the Jacobson radical Ideal.jacobson ⊥ of a (not necessarily commutative) ring is zero.

theorem Ideal.Quotient.isIdempotentElem_mk_iff {R : Type u_1} [Ring R] {I : Ideal R} [I.IsTwoSided] {a : R} : IsIdempotentElem ((mk I) a) ↔ a * a - a ∈ I

An element is idempotent modulo a two-sided ideal I if and only if a * a - a ∈ I.

theorem IsIdempotentElem.eq_of_sub_mem_of_le_jacobson_bot {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) {e e' : R} (he : IsIdempotentElem e) (he' : IsIdempotentElem e') (h : e - e' ∈ I) : e = e'

Idempotent lifts are unique modulo the Jacobson radical. Idempotents that are congruent modulo an ideal contained in the Jacobson radical are equal.

theorem Ideal.injOn_quotient_mk_isIdempotentElem {R : Type u_1} [CommRing R] {I : Ideal R} (hI : I ≤ ⊥.jacobson) : Set.InjOn ⇑(Quotient.mk I) {e : R | IsIdempotentElem e}

Modulo an ideal in the Jacobson radical, the quotient map is injective on idempotents.

theorem IsIdempotentElem.exists_smul_eq_mul_of_mul_sub_smul_mem {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra S T] [Module.Finite S T] {J : Ideal S} (hJ : J ≤ ⊥.jacobson) {e : T} (he : IsIdempotentElem e) (h : ∀ (x : T), ∃ (s : S), e * x - s • e ∈ Ideal.map (algebraMap S T) J) (x : T) : ∃ (s : S), s • e = e * x

Nakayama's lemma for an idempotent. Let T be a module-finite S-algebra and J an ideal of S in the Jacobson radical. If an idempotent e of T satisfies e T ⊆ S e + JT, then e T = S e.