Closed

📁 Source: Mathlib/CategoryTheory/Sites/Closed.lean

Statistics

Metric	Count
Definitions Closed, closedSieves, IsClosed, close, closureOperator, topologyOfClosureOperator	6
Theorems closedSieves_map_coe, closedSieves_obj, close_apply, close_close, close_eq_self_of_isClosed, close_eq_top_iff_mem, close_isClosed, closureOperator_isClosed, covers_iff_mem_of_isClosed, isClosed_iff_close_eq_self, isClosed_pullback, le_close, le_close_of_isClosed, monotone_close, pullback_close, classifier_isSheaf, le_topology_of_closedSieves_isSheaf, topologyOfClosureOperator_close, topologyOfClosureOperator_self, topologyOfClosureOperator_sieves, topology_eq_iff_same_sheaves	21
Total	27

CategoryTheory

Definitions

Name	Category	Theorems
Closed 📖	CompData	—
topologyOfClosureOperator 📖	CompOp	3 math math: topologyOfClosureOperator_self, topologyOfClosureOperator_sieves, topologyOfClosureOperator_close

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
classifier_isSheaf 📖	mathematical	—	Presieve.IsSheaf Functor.closedSieves	—	Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor Sieve.ext GrothendieckTopology.covers_iff_mem_of_isClosed Sieve.inter_apply Sieve.mem_iff_pullback_eq_top GrothendieckTopology.covers_iff GrothendieckTopology.superset_covering Sieve.pullback_monotone inf_le_left GrothendieckTopology.arrow_intersect GrothendieckTopology.pullback_stable le_antisymm Sieve.downward_closed Presieve.compatible_iff_sieveCompatible Sieve.pullback_eq_top_of_mem Sieve.le_pullback_bind GrothendieckTopology.close_isClosed GrothendieckTopology.pullback_close GrothendieckTopology.le_close_of_isClosed le_rfl GrothendieckTopology.le_close
le_topology_of_closedSieves_isSheaf 📖	mathematical	Presieve.IsSheaf Functor.closedSieves	GrothendieckTopology GrothendieckTopology.instLEGrothendieckTopology	—	GrothendieckTopology.close_eq_top_iff_mem GrothendieckTopology.close_isClosed Presieve.IsSeparatedFor.ext Presieve.IsSheafFor.isSeparatedFor Sieve.pullback_top GrothendieckTopology.pullback_close Sieve.pullback_eq_top_of_mem GrothendieckTopology.top_mem
topologyOfClosureOperator_close 📖	mathematical	DFunLike.coe ClosureOperator Sieve PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Sieve.instCompleteLattice ClosureOperator.instFunLike Sieve.pullback	GrothendieckTopology.close topologyOfClosureOperator	—	Sieve.ext Sieve.mem_iff_pullback_eq_top
topologyOfClosureOperator_self 📖	mathematical	—	topologyOfClosureOperator GrothendieckTopology.closureOperator GrothendieckTopology.pullback_close	—	GrothendieckTopology.ext GrothendieckTopology.pullback_close Set.ext GrothendieckTopology.close_eq_top_iff_mem
topologyOfClosureOperator_sieves 📖	mathematical	DFunLike.coe ClosureOperator Sieve PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Sieve.instCompleteLattice ClosureOperator.instFunLike Sieve.pullback	GrothendieckTopology.sieves topologyOfClosureOperator setOf Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—
topology_eq_iff_same_sheaves 📖	mathematical	—	Presieve.IsSheaf	—	le_antisymm le_topology_of_closedSieves_isSheaf classifier_isSheaf

CategoryTheory.Functor

Definitions

Name	Category	Theorems
closedSieves 📖	CompOp	3 math math: closedSieves_obj, closedSieves_map_coe, CategoryTheory.classifier_isSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedSieves_map_coe 📖	mathematical	—	CategoryTheory.Sieve Opposite.unop CategoryTheory.GrothendieckTopology.IsClosed map Opposite CategoryTheory.Category.opposite CategoryTheory.types closedSieves CategoryTheory.Sieve.pullback Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
closedSieves_obj 📖	mathematical	—	obj Opposite CategoryTheory.Category.opposite CategoryTheory.types closedSieves CategoryTheory.Sieve Opposite.unop CategoryTheory.GrothendieckTopology.IsClosed	—	—

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
IsClosed 📖	MathDef	5 math math: CategoryTheory.Functor.closedSieves_obj, closureOperator_isClosed, close_isClosed, CategoryTheory.Functor.closedSieves_map_coe, isClosed_iff_close_eq_self
close 📖	CompOp	11 math math: close_eq_self_of_isClosed, monotone_close, close_apply, close_eq_top_iff_mem, close_close, le_close_of_isClosed, close_isClosed, le_close, CategoryTheory.topologyOfClosureOperator_close, isClosed_iff_close_eq_self, pullback_close
closureOperator 📖	CompOp	2 math math: CategoryTheory.topologyOfClosureOperator_self, closureOperator_isClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
close_apply 📖	mathematical	—	CategoryTheory.Sieve.arrows close Covers	—	—
close_close 📖	mathematical	—	close	—	ClosureOperator.idempotent
close_eq_self_of_isClosed 📖	mathematical	IsClosed	close	—	isClosed_iff_close_eq_self
close_eq_top_iff_mem 📖	mathematical	—	close Top.top CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology instDFunLikeSetSieve	—	transitive top_mem eq_top_iff pullback_stable
close_isClosed 📖	mathematical	—	IsClosed close	—	arrow_trans
closureOperator_isClosed 📖	mathematical	—	ClosureOperator.IsClosed CategoryTheory.Sieve PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice closureOperator IsClosed	—	—
covers_iff_mem_of_isClosed 📖	mathematical	IsClosed	Covers CategoryTheory.Sieve.arrows	—	arrow_max
isClosed_iff_close_eq_self 📖	mathematical	—	IsClosed close	—	ClosureOperator.isClosed_iff
isClosed_pullback 📖	mathematical	IsClosed	CategoryTheory.Sieve.pullback	—	covers_iff CategoryTheory.Sieve.pullback_comp
le_close 📖	mathematical	—	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice close	—	covering_of_eq_top CategoryTheory.Sieve.pullback_eq_top_of_mem
le_close_of_isClosed 📖	mathematical	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice IsClosed	close	—	superset_covering CategoryTheory.Sieve.pullback_monotone
monotone_close 📖	mathematical	—	Monotone CategoryTheory.Sieve PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice close	—	ClosureOperator.monotone
pullback_close 📖	mathematical	—	close CategoryTheory.Sieve.pullback	—	le_antisymm le_close_of_isClosed CategoryTheory.Sieve.pullback_monotone le_close isClosed_pullback close_isClosed CategoryTheory.Sieve.pullback_comp

---

← Back to Index