eq_of_isNilpotent_sub_of_isIdempotentElem

English

If h: ker f nilpotent and e forms a complete orthogonal idempotents structure in S, then there is a lift e′ in R preserving the structure.

Русский

Если ядро f нильпотентно и e образует полную ортогональную систему идемпотентов в S, то имеется подъем e′ в R, сохраняющий структуру.

LaTeX

$$$\\forall h,\\; OrthogonalIdempotents e \\to (CompleteOrthogonalIdempotents e) \\Rightarrow \\exists e' : I \\to R, CompleteOrthogonalIdempotents e' \\land f \\circ e' = e$$$

Lean4

theorem eq_of_isNilpotent_sub_of_isIdempotentElem {e₁ e₂ : R} (he₁ : IsIdempotentElem e₁) (he₂ : IsIdempotentElem e₂)
    (H : IsNilpotent (e₁ - e₂)) : e₁ = e₂ :=
  eq_of_isNilpotent_sub_of_isIdempotentElem_of_commute he₁ he₂ H (.all _ _)

Похожие утверждения