decompId_i — Mathlib

English

The split mono appearing in the factorisation of the identity on P is given by the morphism decompId_i P.

Русский

Разделяющая монома, встречающаяся в разложении тождества на P, задаётся морфизмом decompId_i P.

LaTeX

$$$\mathbb{1}_P = decompId_i P \circ decompId_p P$$$

Lean4

/-- The split mono which appears in the factorisation `decompId P`. -/
@[simps]
def decompId_i (P : Karoubi C) : P ⟶ P.X :=
  ⟨P.p, by rw [coe_p, comp_id, P.idem]⟩

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