Documentation Verification Report

Presheaf

📁 Source: Mathlib/CategoryTheory/Sites/Point/Presheaf.lean

Statistics

Metric	Count
Definitions `pointBot`, `pointBotFunctor`, `pointBotPresheafFiberIso`, `pointsBot`	4
Theorems `instHasEnoughPointsBot`, `instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId`, `instSmallPointBotPointsBotOfSmall`, `isConservative_pointsBot`, `pointBotFunctor_map_hom`, `pointBotFunctor_obj`, `pointBotPresheafFiberIso_inv`, `pointBot_fiber`	8
Total	12

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`pointBot` 📖	CompOp	5 math math: `pointBotFunctor_map_hom`, `pointBotFunctor_obj`, `pointBotPresheafFiberIso_inv`, `instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId`, `pointBot_fiber`
`pointBotFunctor` 📖	CompOp	2 math math: `pointBotFunctor_map_hom`, `pointBotFunctor_obj`
`pointBotPresheafFiberIso` 📖	CompOp	1 math math: `pointBotPresheafFiberIso_inv`
`pointsBot` 📖	CompOp	2 math math: `isConservative_pointsBot`, `instSmallPointBotPointsBotOfSmall`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasEnoughPointsBot` 📖	mathematical	—	`HasEnoughPoints` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.locallySmall_of_essentiallySmall` `CategoryTheory.essentiallySmall_of_small_of_locallySmall` `UnivLE.small` `univLE_of_max` `UnivLE.self` `CategoryTheory.locallySmall_of_univLE` `instSmallPointBotPointsBotOfSmall` `isConservative_pointsBot`
`instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Functor.obj` `CategoryTheory.evaluation` `Opposite.op` `Point.presheafFiber` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `pointBot` `Point.toPresheafFiberNatTrans` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `CategoryTheory.types` `CategoryTheory.shrinkYoneda` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.shrinkYonedaObjObjEquiv` `CategoryTheory.CategoryStruct.id`	—	`CategoryTheory.NatTrans.isIso_iff_isIso_app` `CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal`
`instSmallPointBotPointsBotOfSmall` 📖	mathematical	—	`CategoryTheory.ObjectProperty.Small` `Point` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Point.instCategory` `pointsBot`	—	`CategoryTheory.ObjectProperty.instSmallOfObjOfSmall`
`isConservative_pointsBot` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `pointsBot`	—	`CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'` `CategoryTheory.instHasSheafifyBotGrothendieckTopology` `Equiv.surjective` `Equiv.injective` `CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm` `CategoryTheory.Sieve.downward_closed`
`pointBotFunctor_map_hom` 📖	mathematical	—	`Point.Hom.hom` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `pointBot` `CategoryTheory.Functor.map` `Point` `Point.instCategory` `pointBotFunctor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.shrinkYoneda` `Opposite.op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—
`pointBotFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Point` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Point.instCategory` `pointBotFunctor` `pointBot`	—	—
`pointBotPresheafFiberIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `Point.presheafFiber` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `pointBot` `CategoryTheory.Functor.obj` `CategoryTheory.evaluation` `Opposite.op` `pointBotPresheafFiberIso` `Point.toPresheafFiberNatTrans` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.types` `CategoryTheory.shrinkYoneda` `EquivLike.toFunLike` `Opposite.unop` `Equiv.instEquivLike` `Equiv.symm` `CategoryTheory.shrinkYonedaObjObjEquiv` `CategoryTheory.CategoryStruct.id`	—	—
`pointBot_fiber` 📖	mathematical	—	`Point.fiber` `Bot.bot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `pointBot` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor` `CategoryTheory.types` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.shrinkYoneda` `Opposite.op`	—	—

---

← Back to Index