PrecoverageToGrothendieck

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

Statistics

Metric	Count
Definitions Saturate, toGrothendieck	2
Theorems isSheafFor_iff_of_iso, generate_mem_toGrothendieck, isSheaf_toGrothendieck_iff, mem_toGrothendieck_iff, mem_toGrothendieck_iff_of_isStableUnderComposition, toGrothendieck_eq_sInf, toGrothendieck_mono, toGrothendieck_toPretopology_eq_toGrothendieck, isSheafFor_of_mem_precoverage, comp_iff_of_preservesPairwisePullbacks, isSheafFor_ofArrows_comp_iff, isSheafFor_singleton_iff_of_iso	12
Total	14

CategoryTheory.PreZeroHypercover

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheafFor_iff_of_iso 📖	mathematical	—	CategoryTheory.Presieve.IsSheafFor presieve₀	—	CategoryTheory.Presieve.isSheafFor_iff_generate CategoryTheory.Sieve.ofArrows.eq_1 sieve₀.eq_1 sieve₀_eq_of_iso

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
Saturate 📖	CompData	2 math math: CategoryTheory.Coverage.saturate_iff_saturate_toPrecoverage, mem_toGrothendieck_iff
toGrothendieck 📖	CompOp	17 math math: toGrothendieck_le_iff_le_toPrecoverage, CategoryTheory.Coverage.toGrothendieck_toPrecoverage, isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small, toGrothendieck_mono, CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage, CategoryTheory.Pseudofunctor.IsStack.of_precoverage, isSheaf_toGrothendieck_iff, ZeroHypercover.toOneHypercover_toPreOneHypercover, mem_toGrothendieck_iff, generate_mem_toGrothendieck, CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy, mem_toGrothendieck_iff_of_isStableUnderComposition, toGrothendieck_toCoverage, toGrothendieck_toPretopology_eq_toGrothendieck, toGrothendieck_eq_sInf, CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget, isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
generate_mem_toGrothendieck 📖	mathematical	CategoryTheory.Presieve Set Set.instMembership coverings	CategoryTheory.Sieve DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve toGrothendieck CategoryTheory.Sieve.generate	—	—
isSheaf_toGrothendieck_iff 📖	mathematical	—	CategoryTheory.Presieve.IsSheaf toGrothendieck CategoryTheory.Presieve.IsSheafFor CategoryTheory.Sieve.arrows CategoryTheory.Sieve.pullback CategoryTheory.Sieve.generate	—	CategoryTheory.Presieve.IsSheaf.isSheafFor CategoryTheory.Sieve.generate_sieve CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.Sieve.pullback_top CategoryTheory.Presieve.isSheafFor_top CategoryTheory.Sieve.pullback_comp CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Functor.map_comp CategoryTheory.op_comp CategoryTheory.Category.assoc CategoryTheory.Sieve.pullback_id Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.types_comp_apply
mem_toGrothendieck_iff 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve toGrothendieck Saturate	—	—
mem_toGrothendieck_iff_of_isStableUnderComposition 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve toGrothendieck CategoryTheory.Presieve coverings Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CategoryTheory.instCompleteLatticePresieve CategoryTheory.Sieve.arrows	—	CategoryTheory.Sieve.le_generate mem_coverings_of_isIso CategoryTheory.IsIso.id hasPullbacks_of_mem pullbackArrows_mem CategoryTheory.Sieve.generate_le_iff CategoryTheory.Sieve.pullbackArrows_comm CategoryTheory.Sieve.pullback_monotone mem_iff_exists_zeroHypercover ZeroHypercover.mem₀ CategoryTheory.Presieve.ofArrows_le_iff CategoryTheory.GrothendieckTopology.superset_covering generate_mem_toGrothendieck
toGrothendieck_eq_sInf 📖	mathematical	—	toGrothendieck InfSet.sInf CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instInfSet setOf	—	le_antisymm le_sInf_iff CategoryTheory.GrothendieckTopology.top_mem CategoryTheory.GrothendieckTopology.pullback_stable CategoryTheory.GrothendieckTopology.transitive sInf_le
toGrothendieck_mono 📖	mathematical	CategoryTheory.Precoverage Preorder.toLE PartialOrder.toPreorder instPartialOrder	CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology toGrothendieck	—	generate_mem_toGrothendieck
toGrothendieck_toPretopology_eq_toGrothendieck 📖	mathematical	—	CategoryTheory.Pretopology.toGrothendieck toPretopology toGrothendieck	—	CategoryTheory.GrothendieckTopology.ext Set.ext mem_toGrothendieck_iff_of_isStableUnderComposition instHasPullbacksOfHasPullbacks

CategoryTheory.Presieve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheafFor_ofArrows_comp_iff 📖	mathematical	—	IsSheafFor ofArrows CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	—	CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.PreZeroHypercover.isSheafFor_iff_of_iso
isSheafFor_singleton_iff_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	IsSheafFor singleton	—	ofArrows_pUnit isSheafFor_ofArrows_comp_iff

CategoryTheory.Presieve.IsSheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheafFor_of_mem_precoverage 📖	mathematical	CategoryTheory.Presieve.IsSheaf CategoryTheory.Precoverage.toGrothendieck CategoryTheory.Presieve Set Set.instMembership CategoryTheory.Precoverage.coverings	CategoryTheory.Presieve.IsSheafFor	—	CategoryTheory.Sieve.generate_sieve CategoryTheory.Sieve.pullback_id CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff

CategoryTheory.Presieve.IsSheafFor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_iff_of_preservesPairwisePullbacks 📖	mathematical	—	CategoryTheory.Presieve.IsSheafFor CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.op CategoryTheory.Functor.obj CategoryTheory.Presieve.map	—	CategoryTheory.Presieve.HasPairwisePullbacks.map_of_preservesPairwisePullbacks CategoryTheory.Presieve.exists_eq_ofArrows CategoryTheory.Presieve.map_ofArrows CategoryTheory.Presieve.instHasPullbackOfHasPairwisePullbacksOfArrows CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve CategoryTheory.Limits.hasPullback_of_preservesPullback CategoryTheory.Limits.pullbackComparison_comp_fst CategoryTheory.op_comp CategoryTheory.Functor.map_comp CategoryTheory.Limits.pullbackComparison_comp_snd CategoryTheory.isIso_iff_bijective CategoryTheory.Functor.map_isIso CategoryTheory.isIso_op CategoryTheory.Limits.instIsIsoPullbackComparison

---

← Back to Index