Documentation Verification Report

CoversTop

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

Statistics

Metric	Count
Definitions `CoversTop`, `cover`, `FamilyOfElementsOnObjects`, `IsCompatible`, `section_`, `familyOfElements`	6
Theorems `ext`, `sections_ext`, `coversTop_iff_of_isTerminal`, `existsUnique_section`, `familyOfElements_apply`, `familyOfElements_isCompatible`, `section_apply`	7
Total	13

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`CoversTop` 📖	MathDef	3 math math: `SheafOfModules.QuasicoherentData.coversTop`, `coversTop_iff_of_isTerminal`, `SheafOfModules.LocalGeneratorsData.coversTop`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coversTop_iff_of_isTerminal` 📖	mathematical	—	`CoversTop` `CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve` `CategoryTheory.Sieve.ofObjects`	—	`superset_covering` `pullback_stable`

CategoryTheory.GrothendieckTopology.CoversTop

Definitions

Name	Category	Theorems
`cover` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`CategoryTheory.GrothendieckTopology.CoversTop` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `CategoryTheory.Functor.obj` `Opposite.op` `CategoryTheory.NatTrans.app` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.π`	—	—	`CategoryTheory.Limits.IsLimit.hom_ext` `CategoryTheory.Presheaf.IsSheaf.hom_ext` `CategoryTheory.Sheaf.cond` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.Cone.w` `CategoryTheory.eq_whisker`
`sections_ext` 📖	—	`CategoryTheory.GrothendieckTopology.CoversTop` `Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Sheaf.val` `CategoryTheory.types` `Opposite.op`	—	—	`CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheaf.isSeparated` `CategoryTheory.isSheaf_iff_isSheaf_of_type` `CategoryTheory.Sheaf.cond` `CategoryTheory.Functor.sections_property`

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
`FamilyOfElementsOnObjects` 📖	CompOp	—

CategoryTheory.Presheaf.FamilyOfElementsOnObjects

Definitions

Name	Category	Theorems
`IsCompatible` 📖	MathDef	—
`familyOfElements` 📖	CompOp	2 math math: `IsCompatible.familyOfElements_apply`, `IsCompatible.familyOfElements_isCompatible`

CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible

Definitions

Name	Category	Theorems
`section_` 📖	CompOp	1 math math: `section_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`existsUnique_section` 📖	mathematical	`CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible` `CategoryTheory.GrothendieckTopology.CoversTop` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.types`	`ExistsUnique` `Set.Elem` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite`	—	`CategoryTheory.isSheaf_iff_isSheaf_of_type` `existsUnique_of_exists_of_unique` `familyOfElements_isCompatible` `CategoryTheory.Presieve.IsSheafFor.valid_glue` `CategoryTheory.Functor.map_id` `familyOfElements_apply` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheaf.isSeparated` `CategoryTheory.op_comp` `CategoryTheory.Functor.map_comp` `CategoryTheory.FunctorToTypes.map_id_apply` `CategoryTheory.GrothendieckTopology.CoversTop.sections_ext`
`familyOfElements_apply` 📖	mathematical	`CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible`	`CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.types` `Opposite.op` `Quiver.Hom.op`	—	—
`familyOfElements_isCompatible` 📖	mathematical	`CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible`	`CategoryTheory.Presieve.FamilyOfElements.Compatible` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.ofObjects` `CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements`	—	`familyOfElements_apply` `CategoryTheory.FunctorToTypes.map_comp_apply`
`section_apply` 📖	mathematical	`CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible` `CategoryTheory.GrothendieckTopology.CoversTop` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.types`	`Set` `Set.instMembership` `CategoryTheory.Functor.sections` `Opposite` `CategoryTheory.Category.opposite` `section_` `Opposite.op`	—	`existsUnique_section`

---

← Back to Index