decomp_p — Mathlib

English

Naturality of the split mono decompId_i with respect to morphisms.

Русский

Естественная совместимость разделяющего моно decompId_i относительно морфизмов.

LaTeX

$$$f \circ decompId_i Q = decompId_i P \circ (\mathrm{Hom.mk}\ f.f)$$$

Lean4

theorem decomp_p (P : Karoubi C) : (toKaroubi C).map P.p = decompId_p P ≫ decompId_i P :=
  by
  ext
  simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]

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