Documentation Verification Report

Sheaf

📁 Source: Mathlib/CategoryTheory/Generator/Sheaf.lean

Statistics

Metric	Count
Definitions `freeYoneda`, `freeYonedaHomEquiv`	2
Theorems `hasSeparator`, `isSeparating`, `isSeparator`	3
Total	5

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`freeYoneda` 📖	CompOp	2 math math: `isSeparating`, `isSeparator`
`freeYonedaHomEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSeparator` 📖	mathematical	`CategoryTheory.Limits.HasCoproducts`	`CategoryTheory.HasSeparator` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShape` `isSeparator` `CategoryTheory.isSeparator_separator`
`isSeparating` 📖	mathematical	`CategoryTheory.Limits.HasCoproducts` `CategoryTheory.ObjectProperty.IsSeparating` `CategoryTheory.ObjectProperty.ofObj` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.ObjectProperty.IsSeparating` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.ofObj` `CategoryTheory.Category.toCategoryStruct` `freeYoneda`	—	`CategoryTheory.Functor.map_injective` `CategoryTheory.ObjectProperty.faithful_ι` `CategoryTheory.Presheaf.isSeparating` `Equiv.injective` `CategoryTheory.ObjectProperty.ofObj_apply`
`isSeparator` 📖	mathematical	`CategoryTheory.Limits.HasCoproducts` `CategoryTheory.ObjectProperty.IsSeparating` `CategoryTheory.ObjectProperty.ofObj` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.IsSeparator` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.Limits.sigmaObj` `freeYoneda`	—	`CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct` `isSeparating`

---

← Back to Index