Theorems · Theorem · category theory
CategoryTheory.Category.comp_id
∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {X Y : obj} (f : X ⟶ Y),
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = fIdentity morphisms are right identities for composition.
- Defined in
- Mathlib.CategoryTheory.Category.Basic
- Cited by
- 2,119 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,122
Results whose statement or proof uses this declaration.
- CategoryTheory.MonoidalCategory.whiskerLeft_compproof · cited by 82
- CategoryTheory.MonoidalCategory.comp_whiskerRightproof · cited by 76
- CategoryTheory.MonoidalCategory.tensorHom_idproof · cited by 67
- CategoryTheory.eqToHom_transproof · cited by 54
- CategoryTheory.Over.wproof · cited by 42
- CategoryTheory.Iso.comp_inv_eqproof · cited by 41
- CategoryTheory.Limits.IsZero.iff_id_eq_zeroproof · cited by 40
- CategoryTheory.MonoidalCategory.whiskerRight_idproof · cited by 38
- CategoryTheory.MonoidalCategory.tensor_whiskerLeftproof · cited by 37
- CategoryTheory.MonoidalCategory.whisker_exchangeproof · cited by 36
- AlgebraicGeometry.Scheme.Hom.app_eq_appLEproof · cited by 32
- CategoryTheory.MonoidalCategory.whisker_assocproof · cited by 31
Showing the 200 most cited of 2,122.