English
Let f be a ring homomorphism R → S. If every element of its kernel is nilpotent and e ∈ S is idempotent and lies in the image of f, then there exists an idempotent e′ in R with f(e′) = e.
Русский
Пусть f: R → S — гомоморфизм колец. Если каждый элемент ядра f является нильпотентным, и e ∈ S является идемпотентом и лежит в образе f, то существует идемпотент e′ ∈ R такой, что f(e′) = e.
LaTeX
$$$\\forall f : R \\to_* S, \\; (\\forall x \\in \\ker f, \\ IsNilpotent x) \\\\Rightarrow\\; \\forall e \\in \\operatorname{range} f, \\ IsIdempotentElem e \\;\\exists e' \\in R,\\ \\operatorname{IsIdempotentElem} e' \\wedge f(e') = e$$$
Lean4
/-- Idempotents lift along nil ideals. -/
theorem exists_isIdempotentElem_eq_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e : S)
(he : e ∈ f.range) (he' : IsIdempotentElem e) : ∃ e' : R, IsIdempotentElem e' ∧ f e' = e := by
simpa using exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h e he he' 0 .zero (by simp)
