Precoverage

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

Statistics

Metric	Count
Definitions `PreservesPairwisePullbacks`, `Precoverage`, `HasIsos`, `HasPullbacks`, `IsStableUnderBaseChange`, `IsStableUnderComposition`, `IsStableUnderSup`, `PullbacksPreservedBy`, `comap`, `coverings`, `instBot`, `instCoeFunForallSetPresieve`, `instCompleteLattice`, `instInfSet`, `instMax`, `instMin`, `instPartialOrder`, `instSupSet`, `instTop`	19
Theorems `preservesLimit`, `preservesLimit_cospan_of_mem_presieve`, `mem_coverings_of_isIso`, `hasPullbacks_of_mem`, `mem_coverings_of_isPullback`, `comp_mem_coverings`, `sup_mem_coverings`, `preservesPairwisePullbacks_of_mem`, `comap_comp`, `comap_id`, `comap_inf`, `comp_mem_coverings`, `ext`, `ext_iff`, `hasPairwisePullbacks_of_mem`, `hasPullbacks_of_mem`, `instHasIsosComap`, `instHasIsosMin`, `instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan`, `instHasPullbacksOfHasPullbacks`, `instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan`, `instIsStableUnderBaseChangeMin`, `instIsStableUnderCompositionComap`, `instIsStableUnderCompositionMin`, `instIsStableUnderSupMin`, `instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan`, `mem_comap_iff`, `mem_coverings_of_isIso`, `mem_coverings_of_isPullback`, `preservesPairwisePullbacks_of_mem`, `pullbackArrows_mem`, `sup_mem_coverings`, `map_of_preservesPairwisePullbacks`, `instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan`	34
Total	53

CategoryTheory

Definitions

Name	Category	Theorems
`Precoverage` 📖	CompData	13 math math: `Precoverage.instHasIsosMin`, `Precoverage.toGrothendieck_le_iff_le_toPrecoverage`, `AlgebraicGeometry.Scheme.precoverage_mono`, `MorphismProperty.precoverage_monotone`, `Precoverage.instIsStableUnderSupMin`, `Precoverage.instIsStableUnderBaseChangeMin`, `Precoverage.instIsStableUnderCompositionMin`, `Precoverage.Small.inf`, `AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap`, `MorphismProperty.precoverage_inf`, `Precoverage.le_of_zeroHypercover`, `AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage`, `Precoverage.comap_inf`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan` 📖	mathematical	—	`Functor.PreservesPairwisePullbacks`	—	`Limits.PreservesLimitsOfShape.preservesLimit`

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`PreservesPairwisePullbacks` 📖	CompData	3 math math: `CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem`, `CategoryTheory.Precoverage.preservesPairwisePullbacks_of_mem`, `CategoryTheory.instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesLimit_cospan_of_mem_presieve` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	`PreservesPairwisePullbacks.preservesLimit`

CategoryTheory.Functor.PreservesPairwisePullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesLimit` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan`	—	—

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
`HasIsos` 📖	CompData	9 math math: `instHasIsosMin`, `CategoryTheory.MorphismProperty.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso`, `CategoryTheory.GrothendieckTopology.instHasIsosToPrecoverage`, `AlgebraicGeometry.Scheme.instHasIsosPrecoverageOfContainsIdentitiesOfRespectsIso`, `HasIsos.of_preZeroHypercoverFamily`, `instHasIsosComap`, `instHasIsosFinite`, `AlgebraicGeometry.Scheme.instHasIsosQcPrecoverage`, `CategoryTheory.Types.instHasIsosJointlySurjectivePrecoverage`
`HasPullbacks` 📖	CompData	3 math math: `AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks`, `instHasPullbacksOfHasPullbacks`, `instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan`
`IsStableUnderBaseChange` 📖	CompData	10 math math: `CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage`, `CategoryTheory.GrothendieckTopology.instIsStableUnderBaseChangeToPrecoverage`, `instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan`, `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangePrecoverageOfIsStableUnderBaseChange`, `instIsStableUnderBaseChangeMin`, `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeJointlySurjectivePrecoverage`, `CategoryTheory.instIsStableUnderBaseChangeJointlySurjectivePrecoverage`, `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange`, `IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms`, `AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeQcPrecoverage`
`IsStableUnderComposition` 📖	CompData	8 math math: `AlgebraicGeometry.Scheme.instIsStableUnderCompositionQcPrecoverage`, `CategoryTheory.GrothendieckTopology.instIsStableUnderCompositionToPrecoverage`, `instIsStableUnderCompositionComap`, `instIsStableUnderCompositionMin`, `AlgebraicGeometry.Scheme.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition`, `CategoryTheory.Types.instIsStableUnderCompositionJointlySurjectivePrecoverage`, `IsStableUnderComposition.of_preZeroHypercoverFamily`, `CategoryTheory.MorphismProperty.instIsStableUnderCompositionPrecoverageOfIsStableUnderComposition`
`IsStableUnderSup` 📖	CompData	4 math math: `instIsStableUnderSupMin`, `IsStableUnderSup.of_preZeroHypercoverFamily`, `AlgebraicGeometry.Scheme.instIsStableUnderSupQcPrecoverage`, `CategoryTheory.Types.instIsStableUnderSupJointlySurjectivePrecoverage`
`PullbacksPreservedBy` 📖	CompData	1 math math: `instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan`
`comap` 📖	CompOp	14 math math: `CategoryTheory.isStableUnderBaseChange_comap_jointlySurjectivePrecoverage`, `CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff`, `instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan`, `CategoryTheory.MorphismProperty.comap_precoverage`, `instIsStableUnderCompositionComap`, `instHasIsosComap`, `CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff`, `instSmallComap`, `CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget`, `comap_inf`, `comap_id`, `instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan`, `mem_comap_iff`, `comap_comp`
`coverings` 📖	CompOp	47 math math: `CategoryTheory.GrothendieckTopology.mem_toPretopology`, `ZeroHypercover.Small.exists_restrictIndex_mem`, `CategoryTheory.Coverage.ext_iff`, `CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff`, `CategoryTheory.MorphismProperty.ofArrows_mem_precoverage`, `AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology`, `AlgebraicGeometry.Scheme.bot_mem_precoverage`, `CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff`, `AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff`, `preZeroHypercoverFamily_property`, `CategoryTheory.Pretopology.mem_toGrothendieck`, `CategoryTheory.PreZeroHypercover.presieve₀_mem_iff_of_iso`, `mem_coverings_of_isIso`, `mem_finite_iff`, `CategoryTheory.Pretopology.ext_iff`, `CategoryTheory.MorphismProperty.bot_mem_precoverage`, `AlgebraicGeometry.Scheme.singleton_mem_precoverage_iff`, `AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff`, `HasIsos.mem_coverings_of_isIso`, `CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff`, `mem_toGrothendieck_iff_of_isStableUnderComposition`, `mem_iff_exists_zeroHypercover`, `ZeroHypercover.presieve₀_mem_of_iso`, `CategoryTheory.ofGrothendieck_iff`, `ext_iff`, `ofArrows_mem_finite`, `CategoryTheory.Pretopology.has_isos`, `ZeroHypercover.Small.mem₀`, `CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff`, `CategoryTheory.Pretopology.mem_inf`, `CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff`, `AlgebraicGeometry.Scheme.ofArrows_mem_precoverage_iff`, `CategoryTheory.Presieve.mem_comap_jointlySurjectivePrecoverage_iff`, `CategoryTheory.Pretopology.ofArrows_mem_finite`, `CategoryTheory.Pretopology.mem_sInf`, `ZeroHypercover.mem₀`, `CategoryTheory.Pretopology.mem_toCoverage`, `CategoryTheory.Coverage.sup_covering`, `AlgebraicGeometry.Scheme.mem_pretopology_iff`, `AlgebraicGeometry.Scheme.Cover.mem_pretopology`, `CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff`, `CategoryTheory.Pretopology.mem_ofGrothendieck`, `CategoryTheory.Pretopology.le_def`, `CategoryTheory.GrothendieckTopology.mem_toCoverage_iff`, `AlgebraicGeometry.Scheme.pretopology_cover`, `CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff`, `mem_comap_iff`
`instBot` 📖	CompOp	—
`instCoeFunForallSetPresieve` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instInfSet` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instMin` 📖	CompOp	7 math math: `instHasIsosMin`, `instIsStableUnderSupMin`, `instIsStableUnderBaseChangeMin`, `instIsStableUnderCompositionMin`, `Small.inf`, `CategoryTheory.MorphismProperty.precoverage_inf`, `comap_inf`
`instPartialOrder` 📖	CompOp	6 math math: `toGrothendieck_le_iff_le_toPrecoverage`, `AlgebraicGeometry.Scheme.precoverage_mono`, `CategoryTheory.MorphismProperty.precoverage_monotone`, `AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap`, `le_of_zeroHypercover`, `AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage`
`instSupSet` 📖	CompOp	—
`instTop` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_comp` 📖	mathematical	—	`comap` `CategoryTheory.Functor.comp`	—	`ext` `Set.ext` `CategoryTheory.Presieve.exists_eq_ofArrows` `CategoryTheory.Presieve.map_ofArrows`
`comap_id` 📖	mathematical	—	`comap` `CategoryTheory.Functor.id`	—	`ext` `Set.ext` `CategoryTheory.Presieve.map_id`
`comap_inf` 📖	mathematical	—	`comap` `CategoryTheory.Precoverage` `instMin`	—	—
`comp_mem_coverings` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings` `CategoryTheory.Presieve.ofArrows`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`le_antisymm` `CategoryTheory.Presieve.ofArrows.mk'` `CategoryTheory.Presieve.ofArrows.obj_idx` `CategoryTheory.Presieve.ofArrows.eq_eqToHom_comp_hom_idx` `IsStableUnderComposition.comp_mem_coverings` `CategoryTheory.Presieve.ofArrows.hom_idx` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.Category.id_comp`
`ext` 📖	—	`coverings`	—	—	—
`ext_iff` 📖	mathematical	—	`coverings`	—	`ext`
`hasPairwisePullbacks_of_mem` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings`	`CategoryTheory.Presieve.HasPairwisePullbacks`	—	`CategoryTheory.Presieve.HasPullbacks.hasPullback` `hasPullbacks_of_mem`
`hasPullbacks_of_mem` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings`	`CategoryTheory.Presieve.HasPullbacks`	—	`HasPullbacks.hasPullbacks_of_mem`
`instHasIsosComap` 📖	mathematical	—	`HasIsos` `comap`	—	`CategoryTheory.Presieve.map_singleton` `mem_coverings_of_isIso` `CategoryTheory.Functor.map_isIso`
`instHasIsosMin` 📖	mathematical	—	`HasIsos` `CategoryTheory.Precoverage` `instMin`	—	`mem_coverings_of_isIso`
`instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan` 📖	mathematical	—	`HasPullbacks` `comap`	—	`hasPullbacks_of_mem` `CategoryTheory.Presieve.hasPullback` `CategoryTheory.Presieve.map_map` `CategoryTheory.Limits.HasPullback.of_createsLimit`
`instHasPullbacksOfHasPullbacks` 📖	mathematical	—	`HasPullbacks`	—	`CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks`
`instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan` 📖	mathematical	—	`IsStableUnderBaseChange` `comap`	—	`CategoryTheory.Presieve.map_ofArrows` `mem_coverings_of_isPullback` `CategoryTheory.Functor.map_isPullback` `CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit`
`instIsStableUnderBaseChangeMin` 📖	mathematical	—	`IsStableUnderBaseChange` `CategoryTheory.Precoverage` `instMin`	—	`mem_coverings_of_isPullback`
`instIsStableUnderCompositionComap` 📖	mathematical	—	`IsStableUnderComposition` `comap`	—	`CategoryTheory.Presieve.map_ofArrows` `CategoryTheory.Functor.map_comp` `comp_mem_coverings`
`instIsStableUnderCompositionMin` 📖	mathematical	—	`IsStableUnderComposition` `CategoryTheory.Precoverage` `instMin`	—	`comp_mem_coverings`
`instIsStableUnderSupMin` 📖	mathematical	—	`IsStableUnderSup` `CategoryTheory.Precoverage` `instMin`	—	`sup_mem_coverings`
`instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan` 📖	mathematical	—	`PullbacksPreservedBy`	—	`CategoryTheory.instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan`
`mem_comap_iff` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings` `comap` `CategoryTheory.Functor.obj` `CategoryTheory.Presieve.map`	—	—
`mem_coverings_of_isIso` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings` `CategoryTheory.Presieve.singleton`	—	`HasIsos.mem_coverings_of_isIso`
`mem_coverings_of_isPullback` 📖	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings` `CategoryTheory.Presieve.ofArrows` `CategoryTheory.IsPullback`	—	—	`le_antisymm` `CategoryTheory.Presieve.ofArrows.mk'` `CategoryTheory.Presieve.ofArrows.obj_idx` `CategoryTheory.Presieve.ofArrows.hom_idx` `CategoryTheory.eqToHom_trans_assoc` `CategoryTheory.Category.id_comp` `IsStableUnderBaseChange.mem_coverings_of_isPullback`
`preservesPairwisePullbacks_of_mem` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings`	`CategoryTheory.Functor.PreservesPairwisePullbacks`	—	`PullbacksPreservedBy.preservesPairwisePullbacks_of_mem`
`pullbackArrows_mem` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings`	`CategoryTheory.Presieve.pullbackArrows`	—	`CategoryTheory.Presieve.exists_eq_ofArrows` `CategoryTheory.Presieve.hasPullback` `CategoryTheory.Presieve.instHasPullbacksOfArrowsOfHasPullback` `CategoryTheory.Presieve.ofArrows_pullback` `mem_coverings_of_isPullback` `CategoryTheory.IsPullback.flip` `CategoryTheory.IsPullback.of_hasPullback`
`sup_mem_coverings` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `coverings`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticePresieve`	—	`IsStableUnderSup.sup_mem_coverings`

CategoryTheory.Precoverage.HasIsos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_coverings_of_isIso` 📖	mathematical	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `CategoryTheory.Presieve.singleton`	—	—

CategoryTheory.Precoverage.HasPullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPullbacks_of_mem` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings`	`CategoryTheory.Presieve.HasPullbacks`	—	—

CategoryTheory.Precoverage.IsStableUnderBaseChange

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_coverings_of_isPullback` 📖	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `CategoryTheory.Presieve.ofArrows` `CategoryTheory.IsPullback`	—	—	—

CategoryTheory.Precoverage.IsStableUnderComposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_mem_coverings` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings` `CategoryTheory.Presieve.ofArrows`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—

CategoryTheory.Precoverage.IsStableUnderSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sup_mem_coverings` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CategoryTheory.instCompleteLatticePresieve`	—	—

CategoryTheory.Precoverage.PullbacksPreservedBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preservesPairwisePullbacks_of_mem` 📖	mathematical	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings`	`CategoryTheory.Functor.PreservesPairwisePullbacks`	—	—

CategoryTheory.Presieve.HasPairwisePullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_of_preservesPairwisePullbacks` 📖	mathematical	—	`CategoryTheory.Presieve.HasPairwisePullbacks` `CategoryTheory.Functor.obj` `CategoryTheory.Presieve.map`	—	`has_pullbacks` `CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve` `CategoryTheory.Limits.hasPullback_of_preservesPullback`

---

← Back to Index