idem_of_id_sub_idem — Mathlib

English

In a preadditive category, if p is idempotent, then 1 - p is also idempotent.

Русский

В преддобавительной категории, если p идемпотентен, то 1 - p также идемпотентен.

LaTeX

$$$ (\\mathbf{1}_X - p) \\circ (\\mathbf{1}_X - p) = (\\mathbf{1}_X - p) $$$

Lean4

/-- In a preadditive category, when `p : X ⟶ X` is idempotent,
then `𝟙 X - p` is also idempotent. -/
theorem idem_of_id_sub_idem [Preadditive C] {X : C} (p : X ⟶ X) (hp : p ≫ p = p) : (𝟙 _ - p) ≫ (𝟙 _ - p) = 𝟙 _ - p := by
  simp only [comp_sub, sub_comp, id_comp, comp_id, hp, sub_self, sub_zero]

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