Documentation Verification Report

PrecoverageToGrothendieck

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

Statistics

Metric	Count
Definitions `toPrecoverage`, `toGrothendieck`	2
Theorems `arrows_mem_toPrecoverage_iff`, `instHasIsosToPrecoverage`, `instIsStableUnderBaseChangeToPrecoverage`, `instIsStableUnderCompositionToPrecoverage`, `mem_toPrecoverage_iff`, `toGrothendieck_toPrecoverage_le`, `toPrecoverage_monotone`, `toPrecoverage_top`, `isSheafFor_iff_of_iso`, `galoisConnection_toGrothendieck_toPrecoverage`, `generate_mem_toGrothendieck`, `isSheaf_toGrothendieck_iff`, `le_toPrecoverage_toGrothendieck`, `mem_toGrothendieck_iff`, `mem_toGrothendieck_iff_of_isStableUnderComposition`, `toGrothendieck_bot`, `toGrothendieck_eq_sInf`, `toGrothendieck_le_iff_le_toPrecoverage`, `toGrothendieck_mono`, `toGrothendieck_monotone`, `toGrothendieck_toPretopology_eq_toGrothendieck`, `isSheafFor_of_mem_precoverage`, `comp_iff_of_preservesPairwisePullbacks`, `isSheafFor_ofArrows_comp_iff`, `isSheafFor_singleton_iff_of_iso`	25
Total	27

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
`toPrecoverage` 📖	CompOp	12 math math: `CategoryTheory.Precoverage.toGrothendieck_le_iff_le_toPrecoverage`, `instIsStableUnderBaseChangeToPrecoverage`, `CategoryTheory.Precoverage.galoisConnection_toGrothendieck_toPrecoverage`, `instHasIsosToPrecoverage`, `toGrothendieck_toPrecoverage_le`, `instIsStableUnderCompositionToPrecoverage`, `mem_toPrecoverage_iff`, `toPrecoverage_monotone`, `arrows_mem_toPrecoverage_iff`, `CategoryTheory.Precoverage.le_toPrecoverage_toGrothendieck`, `OneHypercover.toZeroHypercover_toPreZeroHypercover`, `toPrecoverage_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`arrows_mem_toPrecoverage_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.Sieve.arrows` `CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve`	—	`mem_toPrecoverage_iff` `CategoryTheory.Sieve.generate_sieve`
`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_toPrecoverage_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `toPrecoverage` `CategoryTheory.Sieve` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `instDFunLikeSetSieve` `CategoryTheory.Sieve.generate`	—	—
`toGrothendieck_toPrecoverage_le` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `instLEGrothendieckTopology` `CategoryTheory.Precoverage.toGrothendieck` `toPrecoverage`	—	`GaloisConnection.l_u_le` `CategoryTheory.Precoverage.galoisConnection_toGrothendieck_toPrecoverage`
`toPrecoverage_monotone` 📖	mathematical	—	`Monotone` `CategoryTheory.GrothendieckTopology` `CategoryTheory.Precoverage` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.Precoverage.instPartialOrder` `toPrecoverage`	—	`GaloisConnection.monotone_u` `CategoryTheory.Precoverage.galoisConnection_toGrothendieck_toPrecoverage`
`toPrecoverage_top` 📖	mathematical	—	`toPrecoverage` `Top.top` `CategoryTheory.GrothendieckTopology` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `CategoryTheory.Precoverage` `CategoryTheory.Precoverage.instTop`	—	`GaloisConnection.u_top` `CategoryTheory.Precoverage.galoisConnection_toGrothendieck_toPrecoverage`

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
`toGrothendieck` 📖	CompOp	27 math math: `CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology`, `toGrothendieck_le_iff_le_toPrecoverage`, `CategoryTheory.Coverage.toGrothendieck_toPrecoverage`, `locallyCoverDense_of_map_functorPullback_mem`, `galoisConnection_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`, `CategoryTheory.GrothendieckTopology.toGrothendieck_toPrecoverage_le`, `mem_toGrothendieck_iff`, `toGrothendieck_comap_eq_inducedTopology`, `generate_mem_toGrothendieck`, `CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy`, `mem_toGrothendieck_iff_of_isStableUnderComposition`, `toGrothendieck_comap_le_inducedTopology`, `CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le`, `toGrothendieck_toCoverage`, `toGrothendieck_toPretopology_eq_toGrothendieck`, `toGrothendieck_monotone`, `toGrothendieck_bot`, `toGrothendieck_eq_sInf`, `CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget`, `le_toPrecoverage_toGrothendieck`, `isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`galoisConnection_toGrothendieck_toPrecoverage` 📖	mathematical	—	`GaloisConnection` `CategoryTheory.Precoverage` `CategoryTheory.GrothendieckTopology` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.GrothendieckTopology.instPartialOrder` `toGrothendieck` `CategoryTheory.GrothendieckTopology.toPrecoverage`	—	`toGrothendieck_le_iff_le_toPrecoverage`
`generate_mem_toGrothendieck` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings`	`CategoryTheory.Sieve` `Set` `Set.instMembership` `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`
`le_toPrecoverage_toGrothendieck` 📖	mathematical	—	`CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.GrothendieckTopology.toPrecoverage` `toGrothendieck`	—	`GaloisConnection.le_u_l` `galoisConnection_toGrothendieck_toPrecoverage`
`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_bot` 📖	mathematical	—	`toGrothendieck` `Bot.bot` `CategoryTheory.Precoverage` `instBot` `CategoryTheory.GrothendieckTopology` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `CategoryTheory.GrothendieckTopology.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`GaloisConnection.l_bot` `galoisConnection_toGrothendieck_toPrecoverage`
`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_le_iff_le_toPrecoverage` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `toGrothendieck` `CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.GrothendieckTopology.toPrecoverage`	—	`CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff` `generate_mem_toGrothendieck`
`toGrothendieck_mono` 📖	mathematical	`CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`CategoryTheory.GrothendieckTopology` `CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology` `toGrothendieck`	—	`toGrothendieck_monotone`
`toGrothendieck_monotone` 📖	mathematical	—	`Monotone` `CategoryTheory.Precoverage` `CategoryTheory.GrothendieckTopology` `PartialOrder.toPreorder` `instPartialOrder` `CategoryTheory.GrothendieckTopology.instPartialOrder` `toGrothendieck`	—	`GaloisConnection.monotone_l` `galoisConnection_toGrothendieck_toPrecoverage`
`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