Coverage

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

Statistics

Metric	Count
Definitions Coverage, gi, instCoeFunForallSetPresieve, instPartialOrder, instSemilatticeSup, toGrothendieck, toPrecoverage, toCoverage, toCoverage, FactorsThru, FactorsThruAlong, toCoverage	12
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, mem_toCoverage_iff, isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange, isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small, toCoverage_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	29
Total	41

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

CategoryTheory.Coverage

Definitions

Name	Category	Theorems
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
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, pullback, toGrothendieck_toPrecoverage, saturate_iff_saturate_toPrecoverage, CategoryTheory.MorphismProperty.coverage_toPrecoverage, 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 CategoryTheory.Sieve OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice 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 Set Set.instMembership 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 Set Set.instMembership CategoryTheory.Precoverage.coverings toPrecoverage CategoryTheory.Presieve.FactorsThruAlong	—	—
saturate_iff_saturate_toPrecoverage 📖	mathematical	—	Saturate CategoryTheory.Precoverage.Saturate toPrecoverage	—	—
saturate_of_superset 📖	mathematical	CategoryTheory.Sieve Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.Sieve.instCompleteLattice Saturate	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.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	2 math math: CategoryTheory.Coverage.toGrothendieck_eq_sInf, mem_toCoverage_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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	—	—

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_toCoverage 📖	mathematical	—	CategoryTheory.Coverage.toGrothendieck toCoverage toGrothendieck	—	—

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 📖	mathematical	FactorsThru IsSheafFor CategoryTheory.Presieve IsSeparatedFor FactorsThruAlong	IsSheafFor	—	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.arrows	—	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