English
In the complete orthogonal idempotents setting, given h with nilpotent kernel and e : Fin n → R forming complete orthogonal idempotents in S, there exists e′ : Fin n → R lifting e with f ∘ e′ = e.
Русский
В рамках полной ортогональной Idempotents, при условии, что ядро нильпотентно и e : Fin n → R образует полные ортогональные идемпотенты в S, найдется подьём e′ : Fin n → R такой, что f ∘ e′ = e.
LaTeX
$$$\\forall n,\\; \\forall e : \\mathrm{Fin} \\ n \\to S,\\; OrthogonalIdempotents e \\to (\\forall i, e(i) \\in \\operatorname{range} f) \\Rightarrow \\exists e' : \\mathrm{Fin} \\ n \\to R,\\; OrthogonalIdempotents e' \\wedge f \\circ e' = e$$$
Lean4
theorem lift_of_isNilpotent_ker_aux (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) {n} {e : Fin n → S}
(he : CompleteOrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) :
∃ e' : Fin n → R, CompleteOrthogonalIdempotents e' ∧ f ∘ e' = e :=
by
cases subsingleton_or_nontrivial R
· choose e' he' using he'
exact ⟨e', .of_subsingleton, funext he'⟩
cases subsingleton_or_nontrivial S
· obtain ⟨n, hn⟩ := h 1 (Subsingleton.elim _ _)
simp at hn
rcases n with - | n
· simpa using he.complete
obtain ⟨e', h₁, h₂⟩ := OrthogonalIdempotents.lift_of_isNilpotent_ker f h he.1 he'
refine
⟨_, (equiv (finSuccEquiv n)).mpr (CompleteOrthogonalIdempotents.option (h₁.embedding (Fin.succEmb _))),
funext fun i ↦ ?_⟩
have (i : _) : f (e' i) = e i := congr_fun h₂ i
cases i using Fin.cases with
| zero => simp [this, Fin.sum_univ_succ, ← he.complete]
| succ i => simp [this]
