Evaluation

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

Statistics

Metric	Count
Definitions evaluationAdjunctionLeft, evaluationAdjunctionRight, evaluationLeftAdjoint, evaluationRightAdjoint	4
Theorems epi_iff_epi_app', mono_iff_mono_app', evaluationAdjunctionLeft_counit_app, evaluationAdjunctionLeft_unit_app_app, evaluationAdjunctionRight_counit_app_app, evaluationAdjunctionRight_unit_app, evaluationIsLeftAdjoint, evaluationIsRightAdjoint, evaluationLeftAdjoint_map_app, evaluationLeftAdjoint_obj_map, evaluationLeftAdjoint_obj_obj, evaluationRightAdjoint_map_app, evaluationRightAdjoint_obj_map, evaluationRightAdjoint_obj_obj	14
Total	18

CategoryTheory

Definitions

Name	Category	Theorems
evaluationAdjunctionLeft 📖	CompOp	2 math math: evaluationAdjunctionLeft_unit_app_app, evaluationAdjunctionLeft_counit_app
evaluationAdjunctionRight 📖	CompOp	2 math math: evaluationAdjunctionRight_counit_app_app, evaluationAdjunctionRight_unit_app
evaluationLeftAdjoint 📖	CompOp	5 math math: evaluationLeftAdjoint_map_app, evaluationAdjunctionRight_counit_app_app, evaluationLeftAdjoint_obj_obj, evaluationAdjunctionRight_unit_app, evaluationLeftAdjoint_obj_map
evaluationRightAdjoint 📖	CompOp	5 math math: evaluationRightAdjoint_obj_map, evaluationAdjunctionLeft_unit_app_app, evaluationRightAdjoint_map_app, evaluationRightAdjoint_obj_obj, evaluationAdjunctionLeft_counit_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evaluationAdjunctionLeft_counit_app 📖	mathematical	Limits.HasProductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	NatTrans.app Functor.comp Functor Functor.category evaluationRightAdjoint Functor.obj evaluation Functor.id Adjunction.counit evaluationAdjunctionLeft Limits.Pi.π CategoryStruct.id	—	Category.id_comp
evaluationAdjunctionLeft_unit_app_app 📖	mathematical	Limits.HasProductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	NatTrans.app Functor.obj Functor Functor.category evaluationRightAdjoint evaluation Functor.id Functor.comp Adjunction.unit evaluationAdjunctionLeft Limits.Pi.lift Functor.map	—	Category.comp_id
evaluationAdjunctionRight_counit_app_app 📖	mathematical	Limits.HasCoproductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	NatTrans.app Functor.obj Functor Functor.category evaluationLeftAdjoint evaluation Functor.id Functor.comp Adjunction.counit evaluationAdjunctionRight Limits.Sigma.desc Functor.map	—	Category.id_comp
evaluationAdjunctionRight_unit_app 📖	mathematical	Limits.HasCoproductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	NatTrans.app Functor.id Functor.comp Functor Functor.category evaluationLeftAdjoint Functor.obj evaluation Adjunction.unit evaluationAdjunctionRight Limits.Sigma.ι CategoryStruct.id	—	Category.comp_id
evaluationIsLeftAdjoint 📖	mathematical	Limits.HasProductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Functor.IsLeftAdjoint Functor Functor.category Functor.obj evaluation	—	—
evaluationIsRightAdjoint 📖	mathematical	Limits.HasCoproductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Functor.IsRightAdjoint Functor Functor.category Functor.obj evaluation	—	—
evaluationLeftAdjoint_map_app 📖	mathematical	Limits.HasCoproductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	NatTrans.app Limits.sigmaObj Limits.Sigma.desc Limits.Sigma.ι CategoryStruct.comp Functor.map Functor Functor.category evaluationLeftAdjoint Functor.obj	—	—
evaluationLeftAdjoint_obj_map 📖	mathematical	Limits.HasCoproductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Functor.map Functor.obj Functor Functor.category evaluationLeftAdjoint Limits.Sigma.desc Limits.sigmaObj Limits.Sigma.ι CategoryStruct.comp	—	—
evaluationLeftAdjoint_obj_obj 📖	mathematical	Limits.HasCoproductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Functor.obj Functor Functor.category evaluationLeftAdjoint Limits.sigmaObj	—	—
evaluationRightAdjoint_map_app 📖	mathematical	Limits.HasProductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	NatTrans.app Limits.piObj Limits.Pi.lift Limits.Pi.π CategoryStruct.comp Functor.map Functor Functor.category evaluationRightAdjoint Functor.obj	—	—
evaluationRightAdjoint_obj_map 📖	mathematical	Limits.HasProductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Functor.map Functor.obj Functor Functor.category evaluationRightAdjoint Limits.Pi.lift Limits.piObj Limits.Pi.π CategoryStruct.comp	—	—
evaluationRightAdjoint_obj_obj 📖	mathematical	Limits.HasProductsOfShape Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	Functor.obj Functor Functor.category evaluationRightAdjoint Limits.piObj	—	—

CategoryTheory.NatTrans

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_epi_app' 📖	mathematical	CategoryTheory.Limits.HasProductsOfShape Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj app	—	CategoryTheory.Functor.map_epi CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint CategoryTheory.evaluationIsLeftAdjoint epi_of_epi_app
mono_iff_mono_app' 📖	mathematical	CategoryTheory.Limits.HasCoproductsOfShape Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj app	—	CategoryTheory.Functor.map_mono CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint CategoryTheory.evaluationIsRightAdjoint mono_of_mono_app

---

← Back to Index