Lifting idempotents in adically complete algebras

Let R be a commutative ring, I an ideal of R, and S an R-algebra, possibly noncommutative, that is I-adically complete as an R-module. Then idempotents lift along any ring homomorphism f : S →+* T whose kernel is I • S: every idempotent of T in the range of f is the image of an idempotent of S.

Mathlib lifts idempotents along a ring homomorphism whose kernel is nil (exists_isIdempotentElem_eq_of_ker_isNilpotent), which covers a quotient by a nilpotent ideal. The kernel I • S is not nil in general, for instance p • ℤ_p[G] in the group algebra of a finite group over ℤ_p, and completeness replaces nilpotence. For commutative S the statement also follows from Hensel's lemma (TauCeti.HenselianRing.exists_isIdempotentElem_sub_mem); the point here is that S may be noncommutative, such as a matrix algebra or the endomorphism ring of a module.

The proof is Newton's iteration for the polynomial X ^ 2 - X. If a = x ^ 2 - x, then x' = x + a * (1 - 2 * x) satisfies x' ^ 2 - x' = a ^ 2 * (4 * a - 3), so the defect a is squared at each step while x' - x is a multiple of a. Starting from any lift of the idempotent, the iterates form an I-adic Cauchy sequence, and its limit is an idempotent lift. Every element involved is a polynomial in a single element of S, so noncommutativity of S plays no role.

Main results

• TauCeti.IsAdicComplete.exists_isIdempotentElem_eq: idempotents lift along a ring homomorphism with kernel I • S out of an I-adically complete R-algebra S.

References

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

theorem TauCeti.IsAdicComplete.exists_isIdempotentElem_eq {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] (I : Ideal R) [IsAdicComplete I S] {T : Type u_3} [Ring T] (f : S →+* T) (hf : ∀ (x : S), f x = 0 ↔ x ∈ I • ⊤) {e : T} (he : e ∈ f.range) (he' : IsIdempotentElem e) : ∃ (e' : S), IsIdempotentElem e' ∧ f e' = e

Idempotents lift modulo I • S in an I-adically complete algebra. Let S be an R-algebra, possibly noncommutative, which is I-adically complete as an R-module, and let f : S →+* T be a ring homomorphism whose kernel is I • S. Every idempotent of T in the range of f is the image of an idempotent of S.

This is the complete analogue of exists_isIdempotentElem_eq_of_ker_isNilpotent, which asks the kernel to be nil instead.