Documentation Verification Report

Coverage

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

Statistics

Metric	Count
Definitions `Coverage`, `Saturate`, `covering`, `gi`, `instCoeFunForallSetPresieve`, `instPartialOrder`, `instSemilatticeSup`, `ofGrothendieck`, `toGrothendieck`, `toPrecoverage`, `toCoverage`, `toPrecoverage`, `toCoverage`, `FactorsThru`, `FactorsThruAlong`, `toCoverage`	16
Theorems `pullback`, `eq_top_pullback`, `ext`, `ext_iff`, `mem_toGrothendieck`, `mem_toGrothendieck_sieves_of_superset`, `pullback`, `saturate_iff_saturate_toPrecoverage`, `saturate_of_superset`, `sup_covering`, `toGrothendieck_eq_sInf`, `toGrothendieck_toPrecoverage`, `instHasIsosToPrecoverage`, `instIsStableUnderBaseChangeToPrecoverage`, `instIsStableUnderCompositionToPrecoverage`, `mem_toCoverage_iff`, `mem_toPrecoverage_iff`, `isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange`, `isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small`, `toCoverage_toPrecoverage`, `toGrothendieck_le_iff_le_toPrecoverage`, `toGrothendieck_toCoverage`, `isSheaf_iff_isLimit_coverage`, `isSheaf_sup`, `pullbackArrows`, `factorsThruAlong_id`, `factorsThru_of_le`, `factorsThru_top`, `isSheafFor_of_factorsThru`, `isSheaf_coverage`, `isSheaf_sup`, `le_of_factorsThru_sieve`, `mem_toCoverage`, `toGrothendieck_toCoverage`, `ofGrothendieck_iff`	35
Total	51

CategoryTheory

Definitions

Name	Category	Theorems
`Coverage` 📖	CompData	5 math math: `extensive_regular_generate_coherent`, `Coverage.toGrothendieck_eq_sInf`, `Coverage.sup_covering`, `Presheaf.isSheaf_sup`, `Presieve.isSheaf_sup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofGrothendieck_iff` 📖	mathematical	—	`Presieve` `Set` `Set.instMembership` `Precoverage.coverings` `Coverage.toPrecoverage` `GrothendieckTopology.toCoverage` `Sieve` `DFunLike.coe` `GrothendieckTopology` `GrothendieckTopology.instDFunLikeSetSieve` `Sieve.generate`	—	`GrothendieckTopology.mem_toCoverage_iff`

CategoryTheory.Coverage

Definitions

Name	Category	Theorems
`Saturate` 📖	CompData	2 math math: `saturate_iff_saturate_toPrecoverage`, `mem_toGrothendieck`
`covering` 📖	CompOp	—
`gi` 📖	CompOp	—
`instCoeFunForallSetPresieve` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	1 math math: `toGrothendieck_eq_sInf`
`instSemilatticeSup` 📖	CompOp	4 math math: `CategoryTheory.extensive_regular_generate_coherent`, `sup_covering`, `CategoryTheory.Presheaf.isSheaf_sup`, `CategoryTheory.Presieve.isSheaf_sup`
`ofGrothendieck` 📖	CompOp	—
`toGrothendieck` 📖	CompOp	11 math math: `CategoryTheory.extensive_regular_generate_coherent`, `CategoryTheory.Presheaf.isSheaf_iff_isLimit_coverage`, `toGrothendieck_toPrecoverage`, `toGrothendieck_eq_sInf`, `mem_toGrothendieck_sieves_of_superset`, `CategoryTheory.Pretopology.toGrothendieck_toCoverage`, `mem_toGrothendieck`, `CategoryTheory.Presieve.isSheaf_coverage`, `CategoryTheory.Precoverage.toGrothendieck_toCoverage`, `CategoryTheory.Presheaf.isSheaf_sup`, `CategoryTheory.Presieve.isSheaf_sup`
`toPrecoverage` 📖	CompOp	9 math math: `ext_iff`, `toGrothendieck_toPrecoverage`, `saturate_iff_saturate_toPrecoverage`, `CategoryTheory.MorphismProperty.coverage_toPrecoverage`, `CategoryTheory.ofGrothendieck_iff`, `CategoryTheory.Precoverage.toCoverage_toPrecoverage`, `CategoryTheory.Pretopology.mem_toCoverage`, `sup_covering`, `CategoryTheory.GrothendieckTopology.mem_toCoverage_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_pullback` 📖	mathematical	`CategoryTheory.Sieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `CategoryTheory.Sieve.arrows`	`CategoryTheory.Sieve.pullback` `Top.top` `OrderTop.toTop` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`CategoryTheory.Sieve.ext` `CategoryTheory.Sieve.downward_closed`
`ext` 📖	—	`CategoryTheory.Precoverage.coverings` `toPrecoverage`	—	—	—
`ext_iff` 📖	mathematical	—	`CategoryTheory.Precoverage.coverings` `toPrecoverage`	—	`ext`
`mem_toGrothendieck` 📖	mathematical	—	`CategoryTheory.Sieve` `Set` `Set.instMembership` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `toGrothendieck` `Saturate`	—	—
`mem_toGrothendieck_sieves_of_superset` 📖	mathematical	`CategoryTheory.Presieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticePresieve` `CategoryTheory.Sieve.arrows` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage`	`CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `toGrothendieck`	—	`saturate_of_superset` `CategoryTheory.Sieve.generate_le_iff`
`pullback` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage`	`CategoryTheory.Presieve.FactorsThruAlong`	—	—
`saturate_iff_saturate_toPrecoverage` 📖	mathematical	—	`Saturate` `CategoryTheory.Precoverage.Saturate` `toPrecoverage`	—	—
`saturate_of_superset` 📖	—	`CategoryTheory.Sieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.Sieve.instCompleteLattice` `Saturate`	—	—	`eq_top_pullback`
`sup_covering` 📖	mathematical	—	`CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.Coverage` `SemilatticeSup.toMax` `instSemilatticeSup` `Set` `CategoryTheory.Presieve` `Set.instUnion`	—	—
`toGrothendieck_eq_sInf` 📖	mathematical	—	`toGrothendieck` `InfSet.sInf` `CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instInfSet` `setOf` `CategoryTheory.Coverage` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.GrothendieckTopology.toCoverage`	—	`le_antisymm` `le_sInf` `CategoryTheory.GrothendieckTopology.top_mem` `CategoryTheory.GrothendieckTopology.transitive` `sInf_le`
`toGrothendieck_toPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage.toGrothendieck` `toPrecoverage` `toGrothendieck`	—	`toGrothendieck.eq_1` `CategoryTheory.GrothendieckTopology.copy_eq`

CategoryTheory.Coverage.Saturate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pullback` 📖	mathematical	`CategoryTheory.Coverage.Saturate`	`CategoryTheory.Sieve.pullback`	—	`CategoryTheory.Coverage.pullback` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Coverage.saturate_of_superset` `CategoryTheory.Sieve.pullback_comp`

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`toCoverage` 📖	CompOp	3 math math: `CategoryTheory.Coverage.toGrothendieck_eq_sInf`, `CategoryTheory.ofGrothendieck_iff`, `mem_toCoverage_iff`
`toPrecoverage` 📖	CompOp	6 math math: `CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage`, `instIsStableUnderBaseChangeToPrecoverage`, `instHasIsosToPrecoverage`, `instIsStableUnderCompositionToPrecoverage`, `mem_toPrecoverage_iff`, `OneHypercover.toZeroHypercover_toPreZeroHypercover`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasIsosToPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage.HasIsos` `toPrecoverage`	—	`CategoryTheory.Sieve.generate_of_singleton_isSplitEpi` `CategoryTheory.IsSplitEpi.of_iso`
`instIsStableUnderBaseChangeToPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage.IsStableUnderBaseChange` `toPrecoverage`	—	`mem_toPrecoverage_iff` `CategoryTheory.Sieve.ofArrows.eq_1` `CategoryTheory.Sieve.ofArrows_eq_pullback_of_isPullback` `pullback_stable`
`instIsStableUnderCompositionToPrecoverage` 📖	mathematical	—	`CategoryTheory.Precoverage.IsStableUnderComposition` `toPrecoverage`	—	`mem_toPrecoverage_iff` `CategoryTheory.Presieve.bindOfArrows_ofArrows` `bindOfArrows`
`mem_toCoverage_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `CategoryTheory.Coverage.toPrecoverage` `toCoverage` `CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve` `CategoryTheory.Sieve.generate`	—	—
`mem_toPrecoverage_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve` `CategoryTheory.Sieve.generate`	—	—

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
`toCoverage` 📖	CompOp	2 math math: `toGrothendieck_toCoverage`, `toCoverage_toPrecoverage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheaf` `toGrothendieck` `CategoryTheory.Presieve.IsSheafFor`	—	`toCoverage_toPrecoverage` `CategoryTheory.Coverage.toGrothendieck_toPrecoverage` `CategoryTheory.Presieve.isSheaf_coverage`
`isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small` 📖	mathematical	—	`CategoryTheory.Presieve.IsSheaf` `toGrothendieck` `CategoryTheory.Presieve.IsSheafFor` `CategoryTheory.PreZeroHypercover.presieve₀` `ZeroHypercover.toPreZeroHypercover`	—	`isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange` `ZeroHypercover.mem₀` `CategoryTheory.Presieve.exists_eq_preZeroHypercover` `CategoryTheory.Presieve.isSheafFor_iff_generate` `CategoryTheory.Presieve.isSheafFor_subsieve` `instSmallOfSmall` `CategoryTheory.Sieve.generate_mono` `ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks` `CategoryTheory.Sieve.pullbackArrows_comm` `ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀` `CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback` `CategoryTheory.PreZeroHypercover.presieve₀_pullback₁` `ZeroHypercover.pullback₂_toPreZeroHypercover`
`toCoverage_toPrecoverage` 📖	mathematical	—	`CategoryTheory.Coverage.toPrecoverage` `toCoverage`	—	—
`toGrothendieck_le_iff_le_toPrecoverage` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `toGrothendieck` `CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.GrothendieckTopology.toPrecoverage`	—	`toGrothendieck_toCoverage` `GaloisInsertion.gc`
`toGrothendieck_toCoverage` 📖	mathematical	—	`CategoryTheory.Coverage.toGrothendieck` `toCoverage` `toGrothendieck`	—	`le_antisymm` `generate_mem_toGrothendieck` `CategoryTheory.GrothendieckTopology.top_mem` `CategoryTheory.GrothendieckTopology.transitive` `CategoryTheory.GrothendieckTopology.pullback_stable`

CategoryTheory.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSheaf_iff_isLimit_coverage` 📖	mathematical	—	`IsSheaf` `CategoryTheory.Coverage.toGrothendieck` `CategoryTheory.Limits.IsLimit` `Opposite` `CategoryTheory.Presieve.category` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve.generate` `CategoryTheory.Category.opposite` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.id` `CategoryTheory.Comma.left` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.fromPUnit` `CategoryTheory.Comma.hom` `CategoryTheory.Functor.comp` `CategoryTheory.Functor.op` `CategoryTheory.Presieve.diagram` `CategoryTheory.Functor.mapCone` `CategoryTheory.Limits.Cocone.op` `CategoryTheory.Presieve.cocone`	—	—
`isSheaf_sup` 📖	mathematical	—	`IsSheaf` `CategoryTheory.Coverage.toGrothendieck` `CategoryTheory.Coverage` `SemilatticeSup.toMax` `CategoryTheory.Coverage.instSemilatticeSup`	—	`CategoryTheory.Presieve.isSheaf_sup`

CategoryTheory.Presieve

Definitions

Name	Category	Theorems
`FactorsThru` 📖	MathDef	3 math math: `factorsThruAlong_id`, `factorsThru_of_le`, `factorsThru_top`
`FactorsThruAlong` 📖	MathDef	3 math math: `CategoryTheory.Coverage.pullback`, `factorsThruAlong_id`, `FactorsThruAlong.pullbackArrows`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`factorsThruAlong_id` 📖	mathematical	—	`FactorsThruAlong` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `FactorsThru`	—	`CategoryTheory.Category.comp_id`
`factorsThru_of_le` 📖	mathematical	`CategoryTheory.Presieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticePresieve`	`FactorsThru`	—	`CategoryTheory.Category.id_comp`
`factorsThru_top` 📖	mathematical	—	`FactorsThru` `Top.top` `CategoryTheory.Presieve` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.instCompleteLatticePresieve` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`factorsThru_of_le` `le_top`
`isSheafFor_of_factorsThru` 📖	—	`FactorsThru` `IsSheafFor` `IsSeparatedFor` `FactorsThruAlong`	—	—	`IsSeparatedFor.ext` `CategoryTheory.Functor.map_comp` `CategoryTheory.types_comp_apply` `CategoryTheory.op_comp` `CategoryTheory.Category.assoc`
`isSheaf_coverage` 📖	mathematical	—	`IsSheaf` `CategoryTheory.Coverage.toGrothendieck` `IsSheafFor`	—	`CategoryTheory.Coverage.toGrothendieck_toPrecoverage` `CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff` `CategoryTheory.Sieve.pullback_id` `CategoryTheory.Coverage.pullback` `isSheafFor_of_factorsThru` `CategoryTheory.Category.id_comp` `IsSheafFor.isSeparatedFor`
`isSheaf_sup` 📖	mathematical	—	`IsSheaf` `CategoryTheory.Coverage.toGrothendieck` `CategoryTheory.Coverage` `SemilatticeSup.toMax` `CategoryTheory.Coverage.instSemilatticeSup`	—	`isSheaf_of_le` `GaloisConnection.monotone_l` `GaloisInsertion.gc` `le_sup_left` `le_sup_right` `isSheaf_coverage`
`le_of_factorsThru_sieve` 📖	mathematical	`FactorsThru` `CategoryTheory.Sieve.arrows`	`CategoryTheory.Presieve` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticePresieve`	—	`CategoryTheory.Sieve.downward_closed`

CategoryTheory.Presieve.FactorsThruAlong

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pullbackArrows` 📖	mathematical	—	`CategoryTheory.Presieve.FactorsThruAlong` `CategoryTheory.Presieve.pullbackArrows`	—	`CategoryTheory.Presieve.hasPullback` `CategoryTheory.Limits.pullback.condition`

CategoryTheory.Pretopology

Definitions

Name	Category	Theorems
`toCoverage` 📖	CompOp	3 math math: `CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology`, `toGrothendieck_toCoverage`, `mem_toCoverage`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_toCoverage` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `CategoryTheory.Coverage.toPrecoverage` `toCoverage` `toPrecoverage`	—	—
`toGrothendieck_toCoverage` 📖	mathematical	—	`CategoryTheory.Coverage.toGrothendieck` `toCoverage` `toGrothendieck`	—	`CategoryTheory.GrothendieckTopology.ext` `Set.ext` `mem_toGrothendieck` `CategoryTheory.Coverage.mem_toGrothendieck` `CategoryTheory.Sieve.le_generate` `has_isos` `CategoryTheory.IsIso.id` `le_top` `transitive` `CategoryTheory.Coverage.saturate_of_superset` `CategoryTheory.Sieve.generate_le_iff`

---

← Back to Index