English
Given a ring hom f and a finite index n with e : Fin n → S forming orthogonal idempotents in S, if every element of ker f is nilpotent and each e i lies in the image of f, then there exists e′ : Fin n → R with e′ forming orthogonal idempotents and f ∘ e′ = e.
Русский
Пусть дан гомоморфизм кольца f и конечный индекс n; множество e : Fin n → S образует ортогональные идемпотентные элементы. Если ядро f нильпотентно и каждый e i лежит в образе f, то существует e′ : Fin n → R, образующий ортогональные идемпотенты, такой что f ∘ e′ = e.
LaTeX
$$$\\forall f : R \\to_* S, \\; (\\forall x \\in \\ker f, \\ IsNilpotent x) \\; \\forall n : \\mathbb{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 : OrthogonalIdempotents e) (he' : ∀ i, e i ∈ f.range) :
∃ e' : Fin n → R, OrthogonalIdempotents e' ∧ f ∘ e' = e := by
induction n with
| zero => refine ⟨0, ⟨finZeroElim, finZeroElim⟩, funext finZeroElim⟩
| succ n IH =>
obtain ⟨e', h₁, h₂⟩ := IH (he.embedding (Fin.succEmb n)) (fun i ↦ he' _)
have h₂' (i) : f (e' i) = e i.succ := congr_fun h₂ i
obtain ⟨e₀, h₃, h₄, h₅, h₆⟩ :=
exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent f h _ (he' 0) (he.idem 0) _ h₁.isIdempotentElem_sum
(by simp [Finset.mul_sum, h₂', he.mul_eq, eq_comm]) (by simp [Finset.sum_mul, h₂', he.mul_eq])
refine ⟨_, (h₁.option _ h₃ h₅ h₆).embedding (finSuccEquiv n).toEmbedding, funext fun i ↦ ?_⟩
obtain ⟨_ | i, rfl⟩ := (finSuccEquiv n).symm.surjective i <;> simp [*]
