Theorems · Theorem · category theory
CategoryTheory.Category.id_comp
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = fIdentity morphisms are left identities for composition.
- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Cited by
- 1,998 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 9 definitions · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.CategoryStruct.idstatement · cited by 6,235
Cited by2,000
Results whose statement or proof uses this declaration.
- CategoryTheory.Iso.inv_hom_id_assocproof · cited by 275
- CategoryTheory.Iso.hom_inv_id_assocproof · cited by 187
- CategoryTheory.Iso.inv_hom_id_app_assocproof · cited by 57
- CategoryTheory.MonoidalCategory.id_tensorHomproof · cited by 57
- CategoryTheory.Limits.Cone.wproof · cited by 40
- CategoryTheory.Iso.hom_inv_id_app_assocproof · cited by 40
- CategoryTheory.Limits.IsZero.iff_id_eq_zeroproof · cited by 40
- CategoryTheory.IsIso.inv_hom_id_assocproof · cited by 37
- CategoryTheory.MonoidalCategory.whisker_exchangeproof · cited by 36
- CategoryTheory.Functor.extproof · cited by 31
- CategoryTheory.IsIso.hom_inv_id_assocproof · cited by 29
- CategoryTheory.Iso.refl_transproof · cited by 27
Showing the 200 most cited of 2,000.