Documentation Verification Report

Alexandrov

📁 Source: Mathlib/Topology/Sheaves/Alexandrov.lean

Statistics

Metric	Count
Definitions `generator`, `isLimit`, `lowerCone`, `principalOpen`, `principals`, `principalsKanExtension`, `projSup`	7
Theorems `exists_le_of_le_sup`, `isSheaf_principalsKanExtension`, `lowerCone_pt`, `lowerCone_π_app`, `principalOpen_le`, `principalOpen_le_iff`, `principals_map`, `principals_obj`, `projSup_map`, `projSup_obj`, `self_mem_principalOpen`, `isSheaf_of_isRightKanExtension`	12
Total	19

Alexandrov

Definitions

Name	Category	Theorems
`generator` 📖	CompOp	2 math math: `lowerCone_π_app`, `lowerCone_pt`
`isLimit` 📖	CompOp	—
`lowerCone` 📖	CompOp	2 math math: `lowerCone_π_app`, `lowerCone_pt`
`principalOpen` 📖	CompOp	8 math math: `principals_map`, `principalOpen_le_iff`, `principals_obj`, `self_mem_principalOpen`, `lowerCone_π_app`, `principalOpen_le`, `projSup_obj`, `projSup_map`
`principals` 📖	CompOp	6 math math: `principals_map`, `principals_obj`, `lowerCone_π_app`, `projSup_obj`, `lowerCone_pt`, `projSup_map`
`principalsKanExtension` 📖	CompOp	3 math math: `lowerCone_π_app`, `lowerCone_pt`, `isSheaf_principalsKanExtension`
`projSup` 📖	CompOp	3 math math: `lowerCone_π_app`, `projSup_obj`, `projSup_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_le_of_le_sup` 📖	—	`TopologicalSpace.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `principalOpen` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	—	—
`isSheaf_principalsKanExtension` 📖	mathematical	—	`TopCat.Presheaf.IsSheaf` `principalsKanExtension` `TopCat.carrier` `TopCat.str`	—	`TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover`
`lowerCone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.StructuredArrow` `Preorder.smallCategory` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `principals` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.comp` `generator` `lowerCone` `CategoryTheory.ObjectProperty.FullSubcategory` `TopCat.carrier` `TopCat.of` `TopCat.str` `Preorder.toLE` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.op` `CategoryTheory.ObjectProperty.ι` `principalsKanExtension`	—	—
`lowerCone_π_app` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.StructuredArrow` `Preorder.smallCategory` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `principals` `CategoryTheory.instCategoryStructuredArrow` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.ObjectProperty.FullSubcategory` `TopCat.carrier` `TopCat.of` `TopCat.str` `Preorder.toLE` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.ObjectProperty.ι` `principalsKanExtension` `generator` `CategoryTheory.Limits.Cone.π` `lowerCone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `TopCat.Presheaf.SheafCondition.OpensLeCover` `TopCat.Presheaf.SheafCondition.instCategoryOpensLeCover` `projSup` `CategoryTheory.Limits.limit.π` `principalOpen` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.CategoryStruct.id` `CategoryTheory.CategoryStruct.opposite`	—	—
`principalOpen_le` 📖	mathematical	`Preorder.toLE`	`TopologicalSpace.Opens` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `principalOpen`	—	`le_trans`
`principalOpen_le_iff` 📖	mathematical	—	`TopologicalSpace.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `principalOpen` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	—	`self_mem_principalOpen` `TopologicalSpace.Opens.isOpen` `Topology.IsUpperSet.isOpen_iff_isUpperSet`
`principals_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Preorder.smallCategory` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `principals` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `principalOpen` `LE.le.hom`	—	—
`principals_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Preorder.smallCategory` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `principals` `Opposite.op` `principalOpen`	—	—
`projSup_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.StructuredArrow` `Preorder.smallCategory` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `principals` `CategoryTheory.instCategoryStructuredArrow` `TopCat.Presheaf.SheafCondition.OpensLeCover` `TopCat.of` `TopCat.Presheaf.SheafCondition.instCategoryOpensLeCover` `projSup` `Quiver.Hom.op` `CategoryTheory.ObjectProperty.FullSubcategory` `TopCat.carrier` `TopCat.str` `Preorder.toLE` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ObjectProperty.FullSubcategory.category` `principalOpen` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.ObjectProperty.homMk` `CategoryTheory.homOfLE` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	—
`projSup_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.StructuredArrow` `Preorder.smallCategory` `Opposite` `TopologicalSpace.Opens` `CategoryTheory.Category.opposite` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `principals` `CategoryTheory.instCategoryStructuredArrow` `TopCat.Presheaf.SheafCondition.OpensLeCover` `TopCat.of` `TopCat.Presheaf.SheafCondition.instCategoryOpensLeCover` `projSup` `TopCat.carrier` `TopCat.str` `Preorder.toLE` `principalOpen` `CategoryTheory.Comma.right` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit`	—	—
`self_mem_principalOpen` 📖	mathematical	—	`TopologicalSpace.Opens` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `principalOpen`	—	`le_refl`

Topology.IsUpperSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf_of_isRightKanExtension` 📖	mathematical	—	`CategoryTheory.Presheaf.IsSheaf` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opens.grothendieckTopology`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits` `CategoryTheory.Functor.instIsRightKanExtensionPointwiseRightKanExtensionPointwiseRightKanExtensionCounit` `TopCat.Presheaf.isSheaf_iso_iff` `Alexandrov.isSheaf_principalsKanExtension`

---

← Back to Index