English
If ker f is nilpotent and each e i satisfies idempotence and centrality, and f ∘ e is a complete orthogonal idempotents, then e itself is a complete orthogonal idempotents system.
Русский
Если ker f нильпотентно и каждый e i удовлетворяет идемпотентности и централизации, а f ∘ e образует полную ортогональную цепочку идемпотентов, тогда e образует такую же структуру.
LaTeX
$$$\\forall h : (∀ x \\in \\ker f, IsNilpotent x) \\; \\forall e, OrthogonalIdempotents e \\to (CompleteOrthogonalIdempotents (f \\circ e)) \\Rightarrow CompleteOrthogonalIdempotents e$$$
Lean4
theorem of_ker_isNilpotent_of_isMulCentral (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (he : ∀ i, IsIdempotentElem (e i))
(he' : ∀ i, IsMulCentral (e i)) (he'' : CompleteOrthogonalIdempotents (f ∘ e)) : CompleteOrthogonalIdempotents e :=
by
obtain ⟨e', h₁, h₂⟩ := lift_of_isNilpotent_ker f h he'' (fun _ ↦ ⟨_, rfl⟩)
obtain rfl : e = e' := by
ext i
refine eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute (he _) (h₁.idem _) (h _ ?_) ((he' i).comm _)
simpa [RingHom.mem_ker, sub_eq_zero] using congr_fun h₂.symm i
exact h₁
