Adjunction

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

Statistics

Metric	Count
Definitions adjunction, sheafForget	2
Theorems adjunction_counit_app_val, adjunction_unit_app_val, instIsLeftAdjointComposeAndSheafify, instIsRightAdjointSheafComposeOfHasWeakSheafify, instPreservesSheafificationOfIsLeftAdjoint, preservesSheafification_of_adjunction	6
Total	8

CategoryTheory

Definitions

Name	Category	Theorems
sheafForget 📖	CompOp	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	2 math math: adjunction_counit_app_val, adjunction_unit_app_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjunction_counit_app_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.Functor.comp CategoryTheory.sheafCompose composeAndSheafify CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit adjunction CategoryTheory.sheafifyLift CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.whiskeringRight val CategoryTheory.Adjunction.whiskerRight cond	—	cond CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app CategoryTheory.Functor.whiskerRight_id' CategoryTheory.Adjunction.comp_counit_app CategoryTheory.Category.id_comp CategoryTheory.sheafificationAdjunction_counit_app_val CategoryTheory.sheafifyMap_sheafifyLift CategoryTheory.sheafifyLift.congr_simp CategoryTheory.Category.comp_id
adjunction_unit_app_val 📖	mathematical	—	Hom.val CategoryTheory.Functor.obj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.Functor.id CategoryTheory.Functor.comp composeAndSheafify CategoryTheory.sheafCompose CategoryTheory.NatTrans.app CategoryTheory.Adjunction.unit adjunction CategoryTheory.CategoryStruct.comp CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category val CategoryTheory.Functor.whiskeringRight CategoryTheory.sheafify CategoryTheory.Adjunction.whiskerRight CategoryTheory.Functor.whiskerRight CategoryTheory.toSheafify	—	CategoryTheory.Adjunction.map_restrictFullyFaithful_unit_app CategoryTheory.Adjunction.comp_unit_app CategoryTheory.Functor.map_id CategoryTheory.Functor.whiskerRight_id' CategoryTheory.Category.comp_id
instIsLeftAdjointComposeAndSheafify 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint CategoryTheory.Sheaf instCategorySheaf composeAndSheafify	—	CategoryTheory.Adjunction.isLeftAdjoint CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint
instIsRightAdjointSheafComposeOfHasWeakSheafify 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.Sheaf instCategorySheaf CategoryTheory.sheafCompose CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index	—	CategoryTheory.Adjunction.isRightAdjoint CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint
instPreservesSheafificationOfIsLeftAdjoint 📖	mathematical	—	CategoryTheory.GrothendieckTopology.PreservesSheafification	—	preservesSheafification_of_adjunction
preservesSheafification_of_adjunction 📖	mathematical	—	CategoryTheory.GrothendieckTopology.PreservesSheafification	—	CategoryTheory.Adjunction.isRightAdjoint CategoryTheory.MorphismProperty.inverseImage_iff Equiv.comp_bijective cond CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.NatTrans.ext' CategoryTheory.NatTrans.comp_app CategoryTheory.Adjunction.homEquiv_naturality_left Equiv.bijective

---

← Back to Index