Theorems · Theorem · category theory
CategoryTheory.Cat.whiskerRight_app
∀ {C D E : CategoryTheory.Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : ↑C),
(CategoryTheory.Bicategory.whiskerRight η H).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)- Defined in
- Mathlib.CategoryTheory.Category.Cat
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement · cited by 19,642
- CategoryTheory.CategoryStruct.compstatement · cited by 17,999
- CategoryTheory.Functor.mapstatement and proof · cited by 8,698
- CategoryTheory.NatTrans.appstatement and proof · cited by 7,406
- CategoryTheory.Catstatement and proof · cited by 884
- CategoryTheory.Bundled.αstatement and proof · cited by 736
- CategoryTheory.Cat.Hom.toFunctorstatement and proof · cited by 531
- CategoryTheory.Bicategory.whiskerRightstatement · cited by 531
- CategoryTheory.Cat.Hom₂.toNatTransstatement and proof · cited by 277
Cited by51
Results whose statement or proof uses this declaration.
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_inv_appproof · cited by 3
- CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_hom_appproof · cited by 1
- CategoryTheory.Pseudofunctor.StrongTrans.naturality_id_inv_appproof · cited by 1
- CategoryTheory.Pseudofunctor.map₂_associator_appproof · cited by 1
- CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_appproof · cited by 1
- CategoryTheory.Pseudofunctor.map₂_left_unitor_appproof · cited by 1
- CategoryTheory.Pseudofunctor.map₂_whisker_right_appproof · cited by 1
- CategoryTheory.LaxFunctor.mapComp_assoc_left_appproof · cited by 1
- CategoryTheory.LaxFunctor.mapComp_assoc_right_appproof · cited by 1
- CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_appproof · cited by 1
- CategoryTheory.LaxFunctor.mapComp_naturality_left_appproof · cited by 1