English
For a finite index set I, if a family e : I → R consists of orthogonal idempotents and each e i lies in the image of f, then there exists a lifted family e′ : I → R with orthogonal idempotents such that f ∘ e′ = e.
Русский
Для конечного индекcного множества I, если семейство e: I → R состоит из ортогональных идемпотентов и каждый e i лежит в образе f, то существует подъемное семейство e′ : I → R с ортогональными идемпотентами и равенством f(e′(i)) = e(i).
LaTeX
$$$\\forall I \\; [\\text{Finite} I],\\; (h : \\forall x \\in \\ker f,\\ IsNilpotent x) \\; \\forall e : I \\to S,\\; OrthogonalIdempotents e \\to (\\forall i, e(i) \\in \\operatorname{range} f) \\Rightarrow \\exists e' : I \\to R,\\; OrthogonalIdempotents e' \\wedge f \\circ e' = e$$$
Lean4
/-- A family of orthogonal idempotents lift along nil ideals. -/
theorem lift_of_isNilpotent_ker [Finite I] (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {e : I → S}
(he : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) : ∃ e' : I → R, OrthogonalIdempotents e' ∧ f ∘ e' = e :=
by
cases nonempty_fintype I
obtain ⟨e', h₁, h₂⟩ :=
lift_of_isNilpotent_ker_aux f h (he.embedding (Fintype.equivFin I).symm.toEmbedding) (fun _ ↦ he' _)
refine ⟨_, h₁.embedding (Fintype.equivFin I).toEmbedding, by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)⟩
