Documentation Verification Report

PairwiseIntersections

📁 Source: Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean

Statistics

Metric	Count
Definitions `IsSheafPairwiseIntersections`, `IsSheafPreservesLimitPairwiseIntersections`, `pairwiseCoconeIso`, `pairwiseDiagramIso`, `pairwiseToOpensLeCover`, `pairwiseToOpensLeCoverMap`, `pairwiseToOpensLeCoverObj`, `isLimitOpensLeCoverEquivPairwise`, `interUnionPullbackCone`, `interUnionPullbackConeLift`, `isLimitPullbackCone`, `isProductOfDisjoint`	12
Theorems `isSheafPairwiseIntersections`, `isSheafPreservesLimitPairwiseIntersections`, `instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover`, `instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover`, `pairwiseToOpensLeCover_map`, `pairwiseToOpensLeCover_obj`, `isSheafOpensLeCover_iff_isSheafPairwiseIntersections`, `isSheaf_iff_isSheafPairwiseIntersections`, `isSheaf_iff_isSheafPreservesLimitPairwiseIntersections`, `interUnionPullbackConeLift_left`, `interUnionPullbackConeLift_right`, `interUnionPullbackCone_fst`, `interUnionPullbackCone_pt`, `interUnionPullbackCone_snd`	14
Total	26

TopCat.Presheaf

Definitions

Name	Category	Theorems
`IsSheafPairwiseIntersections` 📖	MathDef	2 math math: `isSheaf_iff_isSheafPairwiseIntersections`, `isSheafOpensLeCover_iff_isSheafPairwiseIntersections`
`IsSheafPreservesLimitPairwiseIntersections` 📖	MathDef	1 math math: `isSheaf_iff_isSheafPreservesLimitPairwiseIntersections`
`isLimitOpensLeCoverEquivPairwise` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheafOpensLeCover_iff_isSheafPairwiseIntersections` 📖	mathematical	—	`IsSheafOpensLeCover` `IsSheafPairwiseIntersections`	—	`Equiv.nonempty_congr`
`isSheaf_iff_isSheafPairwiseIntersections` 📖	mathematical	—	`IsSheaf` `IsSheafPairwiseIntersections`	—	`isSheaf_iff_isSheafOpensLeCover` `isSheafOpensLeCover_iff_isSheafPairwiseIntersections`
`isSheaf_iff_isSheafPreservesLimitPairwiseIntersections` 📖	mathematical	—	`IsSheaf` `IsSheafPreservesLimitPairwiseIntersections`	—	`IsSheaf.isSheafPreservesLimitPairwiseIntersections` `isSheaf_iff_isSheafPairwiseIntersections`

TopCat.Presheaf.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheafPairwiseIntersections` 📖	mathematical	`TopCat.Presheaf.IsSheaf`	`CategoryTheory.Limits.IsLimit` `Opposite` `CategoryTheory.Pairwise` `CategoryTheory.Category.opposite` `CategoryTheory.Pairwise.instCategory` `CategoryTheory.Functor.comp` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Functor.op` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Pairwise.diagram` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cocone.op` `CategoryTheory.Pairwise.cocone`	—	`Nonempty.map` `isSheafOpensLeCover`
`isSheafPreservesLimitPairwiseIntersections` 📖	mathematical	`TopCat.Presheaf.IsSheaf`	`CategoryTheory.Limits.PreservesLimit` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Pairwise` `CategoryTheory.Pairwise.instCategory` `CategoryTheory.Functor.op` `CategoryTheory.Pairwise.diagram`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `isSheafPairwiseIntersections`

TopCat.Presheaf.SheafCondition

Definitions

Name	Category	Theorems
`pairwiseCoconeIso` 📖	CompOp	—
`pairwiseDiagramIso` 📖	CompOp	—
`pairwiseToOpensLeCover` 📖	CompOp	4 math math: `pairwiseToOpensLeCover_map`, `pairwiseToOpensLeCover_obj`, `instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover`, `instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover`
`pairwiseToOpensLeCoverMap` 📖	CompOp	1 math math: `pairwiseToOpensLeCover_map`
`pairwiseToOpensLeCoverObj` 📖	CompOp	1 math math: `pairwiseToOpensLeCover_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFinalPairwiseOpensLeCoverPairwiseToOpensLeCover` 📖	mathematical	—	`CategoryTheory.Functor.Final` `CategoryTheory.Pairwise` `CategoryTheory.Pairwise.instCategory` `OpensLeCover` `instCategoryOpensLeCover` `pairwiseToOpensLeCover`	—	`CategoryTheory.isConnected_of_zigzag` `instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover` `le_inf` `LE.le.trans`
`instNonemptyStructuredArrowPairwiseOpensLeCoverPairwiseToOpensLeCover` 📖	mathematical	—	`CategoryTheory.StructuredArrow` `CategoryTheory.Pairwise` `CategoryTheory.Pairwise.instCategory` `OpensLeCover` `instCategoryOpensLeCover` `pairwiseToOpensLeCover`	—	—
`pairwiseToOpensLeCover_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Pairwise` `CategoryTheory.Pairwise.instCategory` `OpensLeCover` `instCategoryOpensLeCover` `pairwiseToOpensLeCover` `pairwiseToOpensLeCoverMap`	—	—
`pairwiseToOpensLeCover_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Pairwise` `CategoryTheory.Pairwise.instCategory` `OpensLeCover` `instCategoryOpensLeCover` `pairwiseToOpensLeCover` `pairwiseToOpensLeCoverObj`	—	—

TopCat.Sheaf

Definitions

Name	Category	Theorems
`interUnionPullbackCone` 📖	CompOp	3 math math: `interUnionPullbackCone_snd`, `interUnionPullbackCone_fst`, `interUnionPullbackCone_pt`
`interUnionPullbackConeLift` 📖	CompOp	2 math math: `interUnionPullbackConeLift_right`, `interUnionPullbackConeLift_left`
`isLimitPullbackCone` 📖	CompOp	—
`isProductOfDisjoint` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`interUnionPullbackConeLift_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `Opposite.op` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.homOfLE` `inf_le_left` `SemilatticeInf.toPartialOrder` `inf_le_right` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `interUnionPullbackConeLift` `SemilatticeSup.toPartialOrder` `le_sup_left` `CategoryTheory.Limits.PullbackCone.fst`	—	`inf_le_left` `inf_le_right` `le_sup_left` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Limits.IsLimit.fac` `TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections` `CategoryTheory.Sheaf.cond`
`interUnionPullbackConeLift_right` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `Opposite.op` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.homOfLE` `inf_le_left` `SemilatticeInf.toPartialOrder` `inf_le_right` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `interUnionPullbackConeLift` `SemilatticeSup.toPartialOrder` `le_sup_right` `CategoryTheory.Limits.PullbackCone.snd`	—	`inf_le_left` `inf_le_right` `le_sup_right` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Limits.IsLimit.fac` `TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections` `CategoryTheory.Sheaf.cond`
`interUnionPullbackCone_fst` 📖	mathematical	—	`CategoryTheory.Limits.PullbackCone.fst` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `Opposite.op` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `inf_le_left` `SemilatticeInf.toPartialOrder` `inf_le_right` `interUnionPullbackCone` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeSup.toPartialOrder` `le_sup_left`	—	`inf_le_left` `inf_le_right`
`interUnionPullbackCone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `Opposite.op` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `inf_le_left` `SemilatticeInf.toPartialOrder` `inf_le_right` `interUnionPullbackCone` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`inf_le_left` `inf_le_right`
`interUnionPullbackCone_snd` 📖	mathematical	—	`CategoryTheory.Limits.PullbackCone.snd` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.Sheaf.val` `Opens.grothendieckTopology` `Opposite.op` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `inf_le_left` `SemilatticeInf.toPartialOrder` `inf_le_right` `interUnionPullbackCone` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `SemilatticeSup.toPartialOrder` `le_sup_right`	—	`inf_le_left` `inf_le_right`

---

← Back to Index