Documentation Verification Report

Closed

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

Statistics

Metric	Count
Definitions `Closed`, `closedSieves`, `sieves`, `IsClosed`, `close`, `closureOperator`, `topologyOfClosureOperator`	7
Theorems `closedSieves_obj`, `sieves_map`, `sieves_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`, `mem_iff_isSheafFor_closedSieves`, `monotone_close`, `pullback_close`, `classifier_isSheaf`, `le_topology_of_closedSieves_isSheaf`, `topologyOfClosureOperator_close`, `topologyOfClosureOperator_self`, `topologyOfClosureOperator_sieves`, `topology_eq_iff_same_sheaves`	23
Total	30

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` `Subfunctor.toFunctor` `Opposite` `Category.opposite` `Functor.sieves` `Functor.closedSieves`	—	`Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor` `Sieve.ext` `GrothendieckTopology.covers_iff_mem_of_isClosed` `GrothendieckTopology.covers_iff` `GrothendieckTopology.superset_covering` `Sieve.pullback_monotone` `inf_le_left` `GrothendieckTopology.arrow_intersect` `GrothendieckTopology.pullback_stable` `le_antisymm` `Sieve.mem_iff_pullback_eq_top` `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` `Subfunctor.toFunctor` `Opposite` `Category.opposite` `Functor.sieves` `Functor.closedSieves`	`GrothendieckTopology` `GrothendieckTopology.instLEGrothendieckTopology`	—	`GrothendieckTopology.mem_iff_isSheafFor_closedSieves`
`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` `DFunLike.coe` `ClosureOperator` `Sieve` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Sieve.instCompleteLattice` `ClosureOperator.instFunLike`	—	`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` `Sieve` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Sieve.instCompleteLattice` `ClosureOperator.instFunLike` `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	6 math math: `closedSieves_obj`, `CategoryTheory.Sheaf.χ_hom`, `CategoryTheory.Sheaf.truth_hom`, `CategoryTheory.Sheaf.Ω_obj`, `CategoryTheory.classifier_isSheaf`, `CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves`
`sieves` 📖	CompOp	14 math math: `closedSieves_obj`, `CategoryTheory.Presheaf.comp_χ_eq`, `CategoryTheory.Presheaf.classifier_Ω`, `CategoryTheory.Presheaf.truth_app`, `CategoryTheory.Presheaf.χ_app`, `CategoryTheory.Sheaf.χ_hom`, `CategoryTheory.Sheaf.truth_hom`, `CategoryTheory.Sheaf.Ω_obj`, `CategoryTheory.Presheaf.isPullback_χ_truth`, `sieves_obj`, `sieves_map`, `CategoryTheory.GrothendieckTopology.isClosed_χ_app_apply_of_isSheaf_of_isSeparated`, `CategoryTheory.classifier_isSheaf`, `CategoryTheory.GrothendieckTopology.mem_iff_isSheafFor_closedSieves`

Theorems

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

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`IsClosed` 📖	MathDef	6 math math: `CategoryTheory.Functor.closedSieves_obj`, `isClosed_pullback`, `closureOperator_isClosed`, `close_isClosed`, `isClosed_iff_close_eq_self`, `isClosed_χ_app_apply_of_isSheaf_of_isSeparated`
`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`	`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`	`CategoryTheory.Sieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `close`	—	`superset_covering` `CategoryTheory.Sieve.pullback_monotone`
`mem_iff_isSheafFor_closedSieves` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve` `CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.Subfunctor.toFunctor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.sieves` `CategoryTheory.Functor.closedSieves` `CategoryTheory.Sieve.arrows`	—	`CategoryTheory.classifier_isSheaf` `close_eq_top_iff_mem` `close_isClosed` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.Sieve.pullback_top` `pullback_close` `CategoryTheory.Sieve.pullback_eq_top_of_mem` `top_mem`
`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