Documentation Verification Report

ConstantSheaf

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

Statistics

Metric	Count
Definitions `IsConstant`, `constantCommuteCompose`, `constantPresheafAdj`, `constantSheaf`, `constantSheafAdj`, `equivCommuteConstant`, `equivCommuteConstant'`	7
Theorems `mem_essImage`, `instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant`, `isConstant_congr`, `isConstant_iff_forget`, `isConstant_iff_isIso_counit_app`, `isConstant_iff_isIso_counit_app'`, `isConstant_iff_mem_essImage`, `isConstant_iff_of_equivalence`, `isConstant_of_forget`, `isConstant_of_isIso_counit_app`, `isConstant_of_iso`, `mem_essImage_of_isConstant`, `constantCommuteCompose_hom_app_hom`, `constantCommuteCompose_hom_app_val`, `constantPresheafAdj_counit_app_app`, `constantPresheafAdj_unit_app`, `constantSheafAdj_counit_app`, `constantSheafAdj_counit_w`, `instIsConstantObjSheafSheafCompose`	19
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
`constantCommuteCompose` 📖	CompOp	3 math math: `constantCommuteCompose_hom_app_val`, `constantSheafAdj_counit_w`, `constantCommuteCompose_hom_app_hom`
`constantPresheafAdj` 📖	CompOp	3 math math: `constantPresheafAdj_counit_app_app`, `constantSheafAdj_counit_app`, `constantPresheafAdj_unit_app`
`constantSheaf` 📖	CompOp	18 math math: `CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf`, `constantCommuteCompose_hom_app_val`, `Sheaf.mem_essImage_of_isConstant`, `Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant`, `LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf`, `Sheaf.ΓObjEquivHom_naturality_symm`, `CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf`, `Sheaf.ΓObjEquivHom_naturality`, `LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf`, `CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf`, `LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf`, `constantSheafAdj_counit_w`, `constantCommuteCompose_hom_app_hom`, `LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf`, `constantSheafAdj_counit_app`, `CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf`, `Sheaf.isConstant_iff_isIso_counit_app`, `Sheaf.IsConstant.mem_essImage`
`constantSheafAdj` 📖	CompOp	4 math math: `Sheaf.instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant`, `constantSheafAdj_counit_w`, `constantSheafAdj_counit_app`, `Sheaf.isConstant_iff_isIso_counit_app`
`equivCommuteConstant` 📖	CompOp	—
`equivCommuteConstant'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`constantCommuteCompose_hom_app_hom` 📖	mathematical	—	`InducedCategory.Hom.hom` `ObjectProperty.FullSubcategory` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `ObjectProperty.FullSubcategory.obj` `Functor.obj` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor.comp` `constantSheaf` `sheafCompose` `NatTrans.app` `Iso.hom` `constantCommuteCompose` `CategoryStruct.comp` `Category.toCategoryStruct` `sheafify` `Functor.const` `Iso.inv` `sheafifyComposeIso` `sheafifyMap` `Functor.constComp`	—	—
`constantCommuteCompose_hom_app_val` 📖	mathematical	—	`InducedCategory.Hom.hom` `ObjectProperty.FullSubcategory` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `ObjectProperty.FullSubcategory.obj` `Functor.obj` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor.comp` `constantSheaf` `sheafCompose` `NatTrans.app` `Iso.hom` `constantCommuteCompose` `CategoryStruct.comp` `Category.toCategoryStruct` `sheafify` `Functor.const` `Iso.inv` `sheafifyComposeIso` `sheafifyMap` `Functor.constComp`	—	`constantCommuteCompose_hom_app_hom`
`constantPresheafAdj_counit_app_app` 📖	mathematical	—	`NatTrans.app` `Opposite` `Category.opposite` `Functor.obj` `Functor` `Functor.category` `Functor.comp` `evaluation` `Opposite.op` `Functor.const` `Functor.id` `Adjunction.counit` `constantPresheafAdj` `Functor.map` `Quiver.Hom.op` `CategoryStruct.toQuiver` `Category.toCategoryStruct` `Opposite.unop` `Limits.IsTerminal.from`	—	—
`constantPresheafAdj_unit_app` 📖	mathematical	—	`NatTrans.app` `Functor.comp` `Functor` `Opposite` `Category.opposite` `Functor.category` `Functor.const` `Functor.obj` `evaluation` `Opposite.op` `Functor.id` `Adjunction.unit` `constantPresheafAdj` `CategoryStruct.id` `Category.toCategoryStruct`	—	—
`constantSheafAdj_counit_app` 📖	mathematical	—	`NatTrans.app` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `Functor.comp` `sheafToPresheaf` `Functor.obj` `evaluation` `Opposite.op` `Functor.const` `presheafToSheaf` `Functor.id` `Adjunction.counit` `constantSheaf` `sheafSections` `constantSheafAdj` `CategoryStruct.comp` `Category.toCategoryStruct` `ObjectProperty.FullSubcategory.obj` `Functor.map` `constantPresheafAdj` `sheafificationAdjunction`	—	`Category.comp_id` `Category.id_comp`
`constantSheafAdj_counit_w` 📖	mathematical	—	`CategoryStruct.comp` `Sheaf` `Category.toCategoryStruct` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `Functor.obj` `Functor.comp` `constantSheaf` `sheafCompose` `ObjectProperty.FullSubcategory.obj` `Opposite.op` `Functor.id` `NatTrans.app` `Iso.hom` `constantCommuteCompose` `sheafSections` `Adjunction.counit` `constantSheafAdj` `Functor.map`	—	`Sheaf.hom_ext` `constantCommuteCompose_hom_app_hom` `Category.assoc` `Iso.inv_comp_eq` `sheafify_hom_ext` `ObjectProperty.FullSubcategory.property` `NatTrans.ext'` `constantSheafAdj_counit_app` `sheafificationAdjunction_counit_app_val` `sheafifyMap_sheafifyLift` `sheafifyLift.congr_simp` `Category.comp_id` `toSheafify_sheafifyLift` `Category.id_comp` `sheafComposeIso_hom_fac_assoc`
`instIsConstantObjSheafSheafCompose` 📖	mathematical	—	`Sheaf.IsConstant` `Functor.obj` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `sheafCompose`	—	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`IsConstant` 📖	CompData	12 math math: `CondensedMod.isDiscrete_tfae`, `isConstant_of_isIso_counit_app`, `isConstant_iff_forget`, `isConstant_congr`, `isConstant_iff_isIso_counit_app'`, `CondensedSet.isDiscrete_tfae`, `isConstant_iff_mem_essImage`, `isConstant_iff_of_equivalence`, `isConstant_of_forget`, `CategoryTheory.instIsConstantObjSheafSheafCompose`, `isConstant_iff_isIso_counit_app`, `isConstant_of_iso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.sheafSections` `Opposite.op` `CategoryTheory.constantSheaf` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `CategoryTheory.constantSheafAdj`	—	`CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage` `mem_essImage_of_isConstant`
`isConstant_congr` 📖	mathematical	—	`IsConstant`	—	`CategoryTheory.Functor.essImage.ofIso` `mem_essImage_of_isConstant`
`isConstant_iff_forget` 📖	mathematical	—	`IsConstant` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.sheafCompose`	—	`CategoryTheory.instIsConstantObjSheafSheafCompose` `isConstant_of_forget`
`isConstant_iff_isIso_counit_app` 📖	mathematical	—	`IsConstant` `CategoryTheory.IsIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.sheafSections` `Opposite.op` `CategoryTheory.constantSheaf` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit` `CategoryTheory.constantSheafAdj`	—	`instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant`
`isConstant_iff_isIso_counit_app'` 📖	mathematical	—	`IsConstant` `CategoryTheory.IsIso` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.comp` `CategoryTheory.sheafSections` `Opposite.op` `CategoryTheory.Functor.id` `CategoryTheory.NatTrans.app` `CategoryTheory.Adjunction.counit`	—	`isConstant_iff_mem_essImage` `CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage`
`isConstant_iff_mem_essImage` 📖	mathematical	—	`IsConstant` `CategoryTheory.Functor.essImage` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf`	—	`CategoryTheory.Functor.essImage_eq_of_natIso`
`isConstant_iff_of_equivalence` 📖	mathematical	`CategoryTheory.Limits.HasLimitsOfShape` `CategoryTheory.StructuredArrow` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.op` `CategoryTheory.instCategoryStructuredArrow`	`IsConstant` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Equivalence.inverse` `CategoryTheory.Functor.IsDenseSubsite.sheafEquiv` `CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous`	—	`CategoryTheory.Functor.IsDenseSubsite.instIsEquivalenceSheafSheafPushforwardContinuous`
`isConstant_of_forget` 📖	mathematical	—	`IsConstant`	—	`CategoryTheory.constantSheafAdj_counit_w` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.NatIso.hom_app_isIso` `instIsIsoAppCounitConstantSheafAdjOfFaithfulOfFullConstantSheafOfIsConstant` `isConstant_iff_isIso_counit_app` `CategoryTheory.isIso_of_reflects_iso`
`isConstant_of_isIso_counit_app` 📖	mathematical	—	`IsConstant`	—	—
`isConstant_of_iso` 📖	mathematical	—	`IsConstant`	—	—
`mem_essImage_of_isConstant` 📖	mathematical	—	`CategoryTheory.Functor.essImage` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.constantSheaf`	—	`IsConstant.mem_essImage`

CategoryTheory.Sheaf.IsConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_essImage` 📖	mathematical	—	`CategoryTheory.Functor.essImage` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.constantSheaf`	—	—

---

← Back to Index