Theorems · Definition · category theory

CategoryTheory.Idempotents.Karoubi.decompId_i

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.Idempotents.Karoubi C) → P ⟶ { X := P.X, p := CategoryTheory.CategoryStruct.id P.X, idem := ⋯ }

The split mono which appears in the factorisation decompId P.

Defined in

Mathlib.CategoryTheory.Idempotents.Karoubi

Cited by

12 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.Category