Documentation Verification Report

Adjunction

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

Statistics

Metric	Count
Definitions `adjunction`, `sheafForget`	2
Theorems `adjunction_counit_app_hom`, `adjunction_counit_app_val`, `adjunction_unit_app_hom`, `adjunction_unit_app_val`, `instIsLeftAdjointComposeAndSheafify`, `instIsRightAdjointSheafComposeOfHasWeakSheafify`, `instPreservesSheafificationOfIsLeftAdjoint`, `preservesSheafification_of_adjunction`	8
Total	10

CategoryTheory

Definitions

Name	Category	Theorems
`sheafForget` 📖	CompOp	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`adjunction` 📖	CompOp	4 math math: `adjunction_unit_app_hom`, `adjunction_counit_app_val`, `adjunction_unit_app_val`, `adjunction_counit_app_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjunction_counit_app_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `CategoryTheory.sheafCompose` `composeAndSheafify` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `adjunction` `CategoryTheory.sheafifyLift` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.Adjunction.whiskerRight` `CategoryTheory.ObjectProperty.FullSubcategory.property`	—	`CategoryTheory.ObjectProperty.FullSubcategory.property` `CategoryTheory.Functor.congr_map` `CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app` `CategoryTheory.Functor.whiskerRight_id'` `CategoryTheory.Functor.map_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_counit_app_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `CategoryTheory.sheafCompose` `composeAndSheafify` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `adjunction` `CategoryTheory.sheafifyLift` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.Adjunction.whiskerRight` `CategoryTheory.ObjectProperty.FullSubcategory.property`	—	`adjunction_counit_app_hom`
`adjunction_unit_app_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `composeAndSheafify` `CategoryTheory.sheafCompose` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `adjunction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `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`
`adjunction_unit_app_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `composeAndSheafify` `CategoryTheory.sheafCompose` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.unit` `adjunction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.whiskeringRight` `CategoryTheory.sheafify` `CategoryTheory.Adjunction.whiskerRight` `CategoryTheory.Functor.whiskerRight` `CategoryTheory.toSheafify`	—	`adjunction_unit_app_hom`
`instIsLeftAdjointComposeAndSheafify` 📖	mathematical	—	`CategoryTheory.Functor.IsLeftAdjoint` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `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` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `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` `CategoryTheory.ObjectProperty.FullSubcategory.property` `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