UniqueGluing

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

Statistics

Metric	Count
Definitions IsCompatible, sectionPairwise, IsGluing, IsSheafUniqueGluing, objPairwiseOfFamily	5
Theorems isSheafUniqueGluing, isSheafUniqueGluing_types, isGluing_iff_pairwise, isSheaf_iff_isSheafUniqueGluing, isSheaf_iff_isSheafUniqueGluing_types, isSheaf_of_isSheafUniqueGluing_types, eq_of_locally_eq, eq_of_locally_eq', eq_of_locally_eq_iff, eq_of_locally_eq₂, existsUnique_gluing, existsUnique_gluing'	12
Total	17

TopCat.Presheaf

Definitions

Name	Category	Theorems
IsCompatible 📖	MathDef	—
IsGluing 📖	MathDef	4 math math: IsSheaf.isSheafUniqueGluing_types, TopCat.Sheaf.existsUnique_gluing, isGluing_iff_pairwise, IsSheaf.isSheafUniqueGluing
IsSheafUniqueGluing 📖	MathDef	2 math math: isSheaf_iff_isSheafUniqueGluing_types, isSheaf_iff_isSheafUniqueGluing
objPairwiseOfFamily 📖	CompOp	1 math math: isGluing_iff_pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGluing_iff_pairwise 📖	mathematical	—	IsGluing CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.NatTrans.app Opposite CategoryTheory.Pairwise CategoryTheory.Category.opposite CategoryTheory.Pairwise.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt 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 CategoryTheory.Limits.Cone.π objPairwiseOfFamily	—	CategoryTheory.Limits.Cone.w
isSheaf_iff_isSheafUniqueGluing 📖	mathematical	—	IsSheaf IsSheafUniqueGluing	—	isSheaf_iff_isSheaf_comp' isSheaf_iff_isSheafUniqueGluing_types
isSheaf_iff_isSheafUniqueGluing_types 📖	mathematical	—	IsSheaf CategoryTheory.types IsSheafUniqueGluing Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory	—	Subtype.prop
isSheaf_of_isSheafUniqueGluing_types 📖	mathematical	IsSheafUniqueGluing CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory	IsSheaf	—	isSheaf_iff_isSheafUniqueGluing_types

TopCat.Presheaf.IsCompatible

Definitions

Name	Category	Theorems
sectionPairwise 📖	CompOp	—

TopCat.Presheaf.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheafUniqueGluing 📖	mathematical	TopCat.Presheaf.IsSheaf TopCat.Presheaf.IsCompatible	ExistsUnique CategoryTheory.ToType CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.Presheaf.IsGluing	—	isSheafUniqueGluing_types TopCat.Presheaf.isSheaf_iff_isSheaf_comp'
isSheafUniqueGluing_types 📖	mathematical	TopCat.Presheaf.IsSheaf CategoryTheory.types TopCat.Presheaf.IsCompatible Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory	ExistsUnique CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.Presheaf.IsGluing	—	CategoryTheory.Limits.Types.isLimit_iff isSheafPairwiseIntersections Subtype.prop

TopCat.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_locally_eq 📖	—	DFunLike.coe 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 iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopologicalSpace.Opens.leSupr	—	—	CategoryTheory.Functor.map_comp existsUnique_gluing
eq_of_locally_eq' 📖	—	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	le_antisymm iSup_le eq_of_locally_eq CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Functor.map_comp CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl CategoryTheory.Functor.map_id CategoryTheory.ConcreteCategory.id_apply
eq_of_locally_eq_iff 📖	mathematical	—	DFunLike.coe 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 iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct TopologicalSpace.Opens.leSupr	—	eq_of_locally_eq
eq_of_locally_eq₂ 📖	—	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice DFunLike.coe CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op CategoryTheory.ConcreteCategory.hom CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—	eq_of_locally_eq' le_trans sup_le_iff le_iSup
existsUnique_gluing 📖	mathematical	TopCat.Presheaf.IsCompatible CategoryTheory.Sheaf.val TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology	ExistsUnique CategoryTheory.ToType CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.Presheaf.IsGluing	—	TopCat.Presheaf.IsSheaf.isSheafUniqueGluing CategoryTheory.Sheaf.cond
existsUnique_gluing' 📖	mathematical	TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.Presheaf.IsCompatible CategoryTheory.Sheaf.val Preorder.smallCategory Opens.grothendieckTopology	ExistsUnique CategoryTheory.ToType CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite Opposite.op	—	le_antisymm iSup_le existsUnique_gluing CategoryTheory.ConcreteCategory.comp_apply CategoryTheory.Functor.map_comp CategoryTheory.eqToHom_op CategoryTheory.eqToHom_trans CategoryTheory.eqToHom_refl CategoryTheory.Functor.map_id CategoryTheory.ConcreteCategory.id_apply

---

← Back to Index