Documentation Verification Report

GlobalSections

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

Statistics

Metric	Count
Definitions `HasGlobalSectionsFunctor`, `coneΓ`, `isLimitConeΓ`, `natTransΓRes`, `Γ`, `ΓHomEquiv`, `ΓNatIsoCoyoneda`, `ΓNatIsoLim`, `ΓNatIsoSectionsFunctor`, `ΓNatIsoSheafSections`, `ΓObjEquivHom`, `ΓObjEquivSections`, `ΓRes`, `constantSheafΓAdj`	14
Theorems `coneΓ_pt`, `coneΓ_π_app`, `natTransΓRes_app`, `ΓHomEquiv_naturality_left`, `ΓHomEquiv_naturality_left_symm`, `ΓHomEquiv_naturality_right`, `ΓHomEquiv_naturality_right_symm`, `ΓObjEquivHom_naturality`, `ΓObjEquivHom_naturality_symm`, `ΓObjEquivSections_naturality`, `ΓObjEquivSections_naturality_symm`, `ΓRes_map`, `ΓRes_map_assoc`, `ΓRes_naturality`, `hasGlobalSectionsFunctor_of_hasLimitsOfShape`, `hasGlobalSectionsFunctor_of_hasTerminal`, `instIsRightAdjointSheafΓ`	17
Total	31

CategoryTheory

Definitions

Name	Category	Theorems
`HasGlobalSectionsFunctor` 📖	MathDef	2 math math: `hasGlobalSectionsFunctor_of_hasLimitsOfShape`, `hasGlobalSectionsFunctor_of_hasTerminal`
`constantSheafΓAdj` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasGlobalSectionsFunctor_of_hasLimitsOfShape` 📖	mathematical	—	`HasGlobalSectionsFunctor`	—	—
`hasGlobalSectionsFunctor_of_hasTerminal` 📖	mathematical	—	`HasGlobalSectionsFunctor`	—	—
`instIsRightAdjointSheafΓ` 📖	mathematical	—	`Functor.IsRightAdjoint` `Sheaf` `Sheaf.instCategorySheaf` `Sheaf.Γ`	—	`Adjunction.instIsRightAdjointRightAdjoint`

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`coneΓ` 📖	CompOp	2 math math: `coneΓ_pt`, `coneΓ_π_app`
`isLimitConeΓ` 📖	CompOp	—
`natTransΓRes` 📖	CompOp	1 math math: `natTransΓRes_app`
`Γ` 📖	CompOp	14 math math: `ΓHomEquiv_naturality_left_symm`, `ΓHomEquiv_naturality_left`, `natTransΓRes_app`, `CategoryTheory.instIsRightAdjointSheafΓ`, `ΓObjEquivSections_naturality_symm`, `ΓRes_map_assoc`, `ΓObjEquivHom_naturality_symm`, `coneΓ_pt`, `ΓHomEquiv_naturality_right_symm`, `ΓObjEquivHom_naturality`, `ΓRes_map`, `ΓHomEquiv_naturality_right`, `ΓObjEquivSections_naturality`, `ΓRes_naturality`
`ΓHomEquiv` 📖	CompOp	4 math math: `ΓHomEquiv_naturality_left_symm`, `ΓHomEquiv_naturality_left`, `ΓHomEquiv_naturality_right_symm`, `ΓHomEquiv_naturality_right`
`ΓNatIsoCoyoneda` 📖	CompOp	—
`ΓNatIsoLim` 📖	CompOp	—
`ΓNatIsoSectionsFunctor` 📖	CompOp	—
`ΓNatIsoSheafSections` 📖	CompOp	—
`ΓObjEquivHom` 📖	CompOp	2 math math: `ΓObjEquivHom_naturality_symm`, `ΓObjEquivHom_naturality`
`ΓObjEquivSections` 📖	CompOp	2 math math: `ΓObjEquivSections_naturality_symm`, `ΓObjEquivSections_naturality`
`ΓRes` 📖	CompOp	5 math math: `natTransΓRes_app`, `ΓRes_map_assoc`, `coneΓ_π_app`, `ΓRes_map`, `ΓRes_naturality`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coneΓ_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `Opposite` `CategoryTheory.Category.opposite` `val` `coneΓ` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ`	—	—
`coneΓ_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `val` `coneΓ` `CategoryTheory.Limits.Cone.π` `ΓRes`	—	—
`natTransΓRes_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.sheafSections` `natTransΓRes` `ΓRes`	—	—
`ΓHomEquiv_naturality_left` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `val` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `EquivLike.toFunLike` `Equiv.instEquivLike` `ΓHomEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Adjunction.homEquiv_naturality_left_symm` `CategoryTheory.Adjunction.homEquiv_naturality_left`
`ΓHomEquiv_naturality_left_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `val` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ΓHomEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Adjunction.homEquiv_naturality_left_symm` `CategoryTheory.Adjunction.homEquiv_naturality_left`
`ΓHomEquiv_naturality_right` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.const` `val` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `EquivLike.toFunLike` `Equiv.instEquivLike` `ΓHomEquiv` `CategoryTheory.CategoryStruct.comp` `Hom.val` `CategoryTheory.Functor.map`	—	`CategoryTheory.Adjunction.homEquiv_naturality_right_symm` `CategoryTheory.Adjunction.homEquiv_naturality_right`
`ΓHomEquiv_naturality_right_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `val` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ΓHomEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map` `Hom.val`	—	`CategoryTheory.Adjunction.homEquiv_naturality_right_symm` `CategoryTheory.Adjunction.homEquiv_naturality_right`
`ΓObjEquivHom_naturality` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.types` `instCategorySheaf` `Γ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.constantSheaf` `EquivLike.toFunLike` `Equiv.instEquivLike` `ΓObjEquivHom` `CategoryTheory.Functor.map` `CategoryTheory.CategoryStruct.comp`	—	`CategoryTheory.Adjunction.homEquiv_naturality_right_symm`
`ΓObjEquivHom_naturality_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.Sheaf` `CategoryTheory.types` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategorySheaf` `CategoryTheory.Functor.obj` `CategoryTheory.constantSheaf` `Γ` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ΓObjEquivHom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Functor.map`	—	`CategoryTheory.Adjunction.homEquiv_naturality_right`
`ΓObjEquivSections_naturality` 📖	mathematical	—	`DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `CategoryTheory.types` `instCategorySheaf` `Γ` `Set.Elem` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite` `val` `EquivLike.toFunLike` `Equiv.instEquivLike` `ΓObjEquivSections` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.sectionsFunctor` `Hom.val`	—	`ΓHomEquiv_naturality_right_symm` `CategoryTheory.Functor.sectionsEquivHom_naturality_symm`
`ΓObjEquivSections_naturality_symm` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Set.Elem` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite` `val` `CategoryTheory.types` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `ΓObjEquivSections` `CategoryTheory.Functor.map` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.sectionsFunctor` `Hom.val`	—	`ΓHomEquiv_naturality_right`
`ΓRes_map` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `Opposite` `CategoryTheory.Category.opposite` `val` `ΓRes` `CategoryTheory.Functor.map`	—	`CategoryTheory.Limits.Cone.w`
`ΓRes_map_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `Opposite` `CategoryTheory.Category.opposite` `val` `ΓRes` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ΓRes_map`
`ΓRes_naturality` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Sheaf` `instCategorySheaf` `Γ` `Opposite` `CategoryTheory.Category.opposite` `val` `CategoryTheory.Functor.map` `ΓRes` `CategoryTheory.NatTrans.app` `Hom.val`	—	`CategoryTheory.congr_app` `ΓHomEquiv_naturality_left_symm` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `ΓHomEquiv_naturality_right_symm`

---

← Back to Index