decompId — Mathlib

English

The identity on P in Karoubi C splits as the inclusion followed by the projection associated to the idempotent P.p.

Русский

Тождество на объекте P в Караоби C раскладывается на включение и проекцию, соответствующие идемпотенту P.p.

LaTeX

$$𝟙 P = decompId_i P ≫ decompId_p P$$

Lean4

/-- The formal direct factor of `P.X` given by the idempotent `P.p` in the category `C`
is actually a direct factor in the category `Karoubi C`. -/
@[reassoc]
theorem decompId (P : Karoubi C) : 𝟙 P = decompId_i P ≫ decompId_p P :=
  by
  ext
  simp only [comp_f, id_f, P.idem, decompId_i, decompId_p]

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