Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi._auxLemma.1
theorem Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi._auxLemma.1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
{f g : P ⟶ Q}, (f = g) = (f.f = g.f)
This theorem states that for any two morphisms `f` and `g` in the category of Karoubi idempotents of a category `C`, the equality of `f` and `g` is equivalent to the equality of their underlying morphisms `f.f` and `g.f`. This means we can identify morphisms in the Karoubi idempotents category by their underlying morphisms in `C`.
More concisely: In the category of Karoubi idempotents of a category $C$, two morphisms $f$ and $g$ are equal if and only if their underlying morphisms $f.f$ and $g.g$ in $C$ are equal.
|
CategoryTheory.Idempotents.KaroubiKaroubi.idem_f
theorem CategoryTheory.Idempotents.KaroubiKaroubi.idem_f :
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
(P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)),
CategoryTheory.CategoryStruct.comp P.p.f P.p.f = P.p.f
This theorem is a statement in category theory. It states that for any category `C` and any idempotent `P` in the category of idempotents of `C`, the composition of the morphism `P.p.f` with itself (written `P.p.f ≫ P.p.f` in category theory) is equal to `P.p.f`. In other words, the morphism `P.p.f` is idempotent in its category.
More concisely: For any idempotent `P` in a category `C`, the morphism `P.p.f` is idempotent, i.e., `P.p.f ≫ P.p.f = P.p.f`.
|