Structures · Category theory
CategoryTheory.Precoverage.IsStableUnderBaseChange
A precoverage is stable under base change if pullbacks of covering presieves
are covering presieves.
Use Precoverage.mem_coverings_of_isPullback for less universe restrictions.
Note: This is stronger than the analogous requirement for a Pretopology, because
IsPullback does not imply equality with the (arbitrarily) chosen pullbacks in C.
- Defined in
- Mathlib.CategoryTheory.Sites.Precoverage
- Shape
- One type argument · adds mem_coverings_of_isPullback
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- AlgebraicGeometry.Scheme
- TopCat
How is a type an instance?
Loading the hierarchy index…
Assumed by49
- CategoryTheory.Precoverage.ZeroHypercover.pullback₁
- CategoryTheory.Precoverage.toCoverage
- CategoryTheory.Precoverage.toPretopology
- CategoryTheory.Precoverage.ZeroHypercover.pullback₂
- CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck
- CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition
- CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft
- CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget
- CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology
- CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem
- CategoryTheory.Precoverage.toGrothendieck_comap_eq_restrictedTopology
- CategoryTheory.Precoverage.pullbackArrows_mem
- CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight
- CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage
- CategoryTheory.MorphismProperty.coverPreserving_comap_forget
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- CategoryTheory.Precoverage.ZeroHypercover.inter
- CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover
- CategoryTheory.Precoverage.toGrothendieck_toCoverage
- CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange
- CategoryTheory.Precoverage.toCoverage_toPrecoverage
- CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff
- CategoryTheory.Precoverage.mem_coverings_of_isPullback
- CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.Precoverage.IsStableUnderBaseChange.mem_coverings_of_isPullback
- CategoryTheory.Pseudofunctor.IsStack.of_precoverage
- CategoryTheory.Precoverage.ZeroHypercover.pullback₁.congr_simp
- CategoryTheory.Precoverage.toPretopology_toPrecoverage
- CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover
- CategoryTheory.eq_of_zeroHypercover_target
- CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover
- CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover
- CategoryTheory.Precoverage.instRespectsIsoOfIsStableUnderBaseChange
- CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology
- CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover
- CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁
- CategoryTheory.Precoverage.toPretopology.congr_simp
- CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft
- CategoryTheory.MorphismProperty.sourceLocalClosure.instIsStableUnderBaseChangeOfIsStableUnderBaseChangeOfHasPullbacks
- CategoryTheory.Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan
- CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft.congr_simp
- CategoryTheory.Precoverage.toCoverage.congr_simp
- CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy
- CategoryTheory.Precoverage.instIsStableUnderBaseChangeMin
- CategoryTheory.Precoverage.toCoverage_le_toCoverage
- CategoryTheory.Precoverage.ZeroHypercover.isPullback_of_forall_isPullback
- CategoryTheory.Precoverage.ZeroHypercover.instIsLocalAtTargetIsomorphisms
Ancestors0
No ancestors.