Sites

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

Statistics

Metric	Count
Definitions coveringOfPresieve, presieveOfCovering, homOfIndex, indexOfHom, presieveOfCoveringAux, isTerminalOfEmpty, isTerminalOfEqEmpty, restrictHomEquivHom	8
Theorems coverPreserving, coverDense_iff_isBasis, coverDense_inducedFunctor, iSup_eq_of_mem_grothendieck, coveringOfPresieve_apply, covering_presieve_eq_self, isSheaf_of_isOpenEmbedding, indexOfHom_spec, mem_grothendieckTopology, extend_hom_app, hom_ext, instIsContinuousCompGrothendieckTopology, compatiblePreserving, functor_isContinuous, compatiblePreserving_opens_map, coverPreserving_opens_map, instIsContinuousOpensCarrierMapGrothendieckTopology, instRepresentablyFlatOpensCarrierMap	18
Total	26

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverPreserving 📖	mathematical	IsOpenMap TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CoverPreserving TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology functor	—	Set.mem_image_of_mem

TopCat.Opens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverDense_iff_isBasis 📖	mathematical	—	CategoryTheory.Functor.IsCoverDense TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology TopologicalSpace.Opens.IsBasis Set.range CategoryTheory.Functor.obj	—	TopologicalSpace.Opens.isBasis_iff_nbhd CategoryTheory.Functor.IsCoverDense.is_cover
coverDense_inducedFunctor 📖	mathematical	TopologicalSpace.Opens.IsBasis TopCat.carrier TopCat.str Set.range TopologicalSpace.Opens	CategoryTheory.Functor.IsCoverDense CategoryTheory.InducedCategory CategoryTheory.InducedCategory.instCategory Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.inducedFunctor Opens.grothendieckTopology	—	coverDense_iff_isBasis

TopCat.Presheaf

Definitions

Name	Category	Theorems
coveringOfPresieve 📖	CompOp	3 math math: coveringOfPresieve.iSup_eq_of_mem_grothendieck, covering_presieve_eq_self, coveringOfPresieve_apply
presieveOfCovering 📖	CompOp	2 math math: presieveOfCovering.indexOfHom_spec, presieveOfCovering.mem_grothendieckTopology
presieveOfCoveringAux 📖	CompOp	13 math math: generateEquivalenceOpensLe_functor'_obj_obj, generateEquivalenceOpensLe_unitIso, generateEquivalenceOpensLe_inverse'_obj_obj_right_as, generateEquivalenceOpensLe_inverse'_obj_obj_hom, whiskerIsoMapGenerateCocone_inv_hom, covering_presieve_eq_self, generateEquivalenceOpensLe_functor, generateEquivalenceOpensLe_counitIso, whiskerIsoMapGenerateCocone_hom_hom, generateEquivalenceOpensLe_inverse'_obj_obj_left, generateEquivalenceOpensLe_functor'_map, generateEquivalenceOpensLe_inverse'_map, generateEquivalenceOpensLe_inverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coveringOfPresieve_apply 📖	mathematical	—	coveringOfPresieve TopologicalSpace.Opens TopCat.carrier TopCat.str Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	—	—
covering_presieve_eq_self 📖	mathematical	—	presieveOfCoveringAux TopologicalSpace.Opens TopCat.carrier TopCat.str Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder coveringOfPresieve	—	Set.ext Preorder.subsingleton_hom
isSheaf_of_isOpenEmbedding 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier IsSheaf	CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Functor.op IsOpenMap.functor Topology.IsOpenEmbedding.isOpenMap	—	Topology.IsOpenEmbedding.isOpenMap Topology.IsOpenEmbedding.functor_isContinuous CategoryTheory.Functor.op_comp_isSheaf

TopCat.Presheaf.coveringOfPresieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iSup_eq_of_mem_grothendieck 📖	mathematical	CategoryTheory.Sieve TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve Opens.grothendieckTopology CategoryTheory.Sieve.generate	iSup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.Presheaf.coveringOfPresieve	—	le_antisymm iSup_le TopologicalSpace.Opens.mem_iSup

TopCat.Presheaf.presieveOfCovering

Definitions

Name	Category	Theorems
homOfIndex 📖	CompOp	—
indexOfHom 📖	CompOp	1 math math: indexOfHom_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
indexOfHom_spec 📖	mathematical	—	TopologicalSpace.Opens TopCat.carrier TopCat.str Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice TopCat.Presheaf.presieveOfCovering indexOfHom	—	—
mem_grothendieckTopology 📖	mathematical	—	CategoryTheory.Sieve TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve Opens.grothendieckTopology CategoryTheory.Sieve.generate TopCat.Presheaf.presieveOfCovering	—	TopologicalSpace.Opens.mem_iSup CategoryTheory.Category.id_comp

TopCat.Sheaf

Definitions

Name	Category	Theorems
isTerminalOfEmpty 📖	CompOp	—
isTerminalOfEqEmpty 📖	CompOp	—
restrictHomEquivHom 📖	CompOp	1 math math: extend_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extend_hom_app 📖	mathematical	TopologicalSpace.Opens.IsBasis TopCat.carrier TopCat.str Set.range TopologicalSpace.Opens	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology DFunLike.coe Equiv Quiver.Hom CategoryTheory.Functor CategoryTheory.InducedCategory CategoryTheory.InducedCategory.instCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.inducedFunctor TopCat.Presheaf TopCat.instCategoryPresheaf EquivLike.toFunLike Equiv.instEquivLike restrictHomEquivHom Opposite.op	—	Equiv.left_inv
hom_ext 📖	—	TopologicalSpace.Opens.IsBasis TopCat.carrier TopCat.str Set.range TopologicalSpace.Opens CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder CategoryTheory.Sheaf.val Opens.grothendieckTopology Opposite.op	—	—	Equiv.injective CategoryTheory.NatTrans.ext'

TopologicalSpace.Opens

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsContinuousCompGrothendieckTopology 📖	mathematical	—	CategoryTheory.Functor.IsContinuous TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder instPartialOrder CategoryTheory.Functor.comp Opens.grothendieckTopology	—	CategoryTheory.Functor.isContinuous_comp

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compatiblePreserving 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.CompatiblePreserving TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology IsOpenMap.functor isOpenMap	—	CategoryTheory.compatiblePreservingOfDownwardsClosed isOpenMap IsOpenMap.functorFullOfMono TopCat.mono_iff_injective Topology.IsEmbedding.injective toIsEmbedding IsOpenMap.functor_faithful TopologicalSpace.Opens.ext Set.image_preimage_eq_of_subset
functor_isContinuous 📖	mathematical	Topology.IsOpenEmbedding TopCat.carrier TopCat.str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier	CategoryTheory.Functor.IsContinuous TopologicalSpace.Opens Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder IsOpenMap.functor isOpenMap Opens.grothendieckTopology	—	CategoryTheory.Functor.isContinuous_of_coverPreserving isOpenMap compatiblePreserving IsOpenMap.coverPreserving

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compatiblePreserving_opens_map 📖	mathematical	—	CategoryTheory.CompatiblePreserving TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology TopologicalSpace.Opens.map	—	CategoryTheory.compatiblePreservingOfFlat instRepresentablyFlatOpensCarrierMap
coverPreserving_opens_map 📖	mathematical	—	CategoryTheory.CoverPreserving TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder Opens.grothendieckTopology TopologicalSpace.Opens.map	—	Preorder.subsingleton_hom
instIsContinuousOpensCarrierMapGrothendieckTopology 📖	mathematical	—	CategoryTheory.Functor.IsContinuous TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map Opens.grothendieckTopology	—	CategoryTheory.Functor.isContinuous_of_coverPreserving compatiblePreserving_opens_map coverPreserving_opens_map
instRepresentablyFlatOpensCarrierMap 📖	mathematical	—	CategoryTheory.RepresentablyFlat TopologicalSpace.Opens TopCat.carrier TopCat.str Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map	—	le_inf inf_le_left inf_le_right CategoryTheory.Category.id_comp Preorder.subsingleton_hom le_top

---

← Back to Index