English
A system of complete orthogonal idempotents in S can be lifted to a system in R via a nilpotent kernel, matching under f.
Русский
Система полных ортогональных идемпотентов в S может быть поднята до системы в R через нильпотентное ядро, сохранение под f.
LaTeX
$$$\\forall f,\\; (\\forall x \\in \\ker f, IsNilpotent x) \\Rightarrow (\\exists e', CompleteOrthogonalIdempotents e' \\wedge f \\circ e' = e)$$$
Lean4
/-- A system of complete orthogonal idempotents lift along nil ideals. -/
theorem lift_of_isNilpotent_ker (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {e : I → S}
(he : CompleteOrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) :
∃ e' : I → R, CompleteOrthogonalIdempotents e' ∧ f ∘ e' = e :=
by
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker_aux f h ((equiv (Fintype.equivFin I).symm).mpr he) (fun _ ↦ he' _)
refine ⟨_, ((equiv (Fintype.equivFin I)).mpr h₁), by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩
