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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.property
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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.property
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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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