Whiskering

📁 Source: Mathlib/CategoryTheory/Adjunction/Whiskering.lean

Statistics

Metric	Count
Definitions whiskerLeft, whiskerRight	2
Theorems whiskerLeft_counit_app_app, whiskerLeft_unit_app_app, whiskerRight_counit_app_app, whiskerRight_unit_app_app	4
Total	6

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
whiskerLeft 📖	CompOp	2 math math: whiskerLeft_unit_app_app, whiskerLeft_counit_app_app
whiskerRight 📖	CompOp	4 math math: CategoryTheory.Sheaf.adjunction_counit_app_val, CategoryTheory.Sheaf.adjunction_unit_app_val, whiskerRight_counit_app_app, whiskerRight_unit_app_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
whiskerLeft_counit_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft CategoryTheory.Functor.id counit whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
whiskerLeft_unit_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringLeft unit whiskerLeft CategoryTheory.Functor.map	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
whiskerRight_counit_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight CategoryTheory.Functor.id counit whiskerRight	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
whiskerRight_unit_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Functor.whiskeringRight unit whiskerRight	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp

---

← Back to Index