Structures · Category theory
CategoryTheory.Precoverage.HasPullbacks
A precoverage has pullbacks, if every covering presieve has pullbacks along arbitrary morphisms.
- Defined in
- Mathlib.CategoryTheory.Sites.Precoverage
- Shape
- One type argument · adds hasPullbacks_of_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances1
- AlgebraicGeometry.Scheme
How is a type an instance?
Loading the hierarchy index…
Assumed by31
- CategoryTheory.Precoverage.toCoverage
- CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff_of_zeroHypercover
- CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition
- CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target
- CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget
- CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover
- CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology
- CategoryTheory.MorphismProperty.of_zeroHypercover_target
- CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem
- CategoryTheory.Precoverage.toGrothendieck_comap_eq_restrictedTopology
- CategoryTheory.Precoverage.HasPullbacks.hasPullbacks_of_mem
- CategoryTheory.MorphismProperty.coverPreserving_comap_forget
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover
- CategoryTheory.Precoverage.toGrothendieck_toCoverage
- CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange
- CategoryTheory.Precoverage.toCoverage_toPrecoverage
- CategoryTheory.Precoverage.hasPullbacks_of_mem
- CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small
- CategoryTheory.Precoverage.hasPairwisePullbacks_of_mem
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange
- CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology
- CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft
- CategoryTheory.Precoverage.instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan
- CategoryTheory.Precoverage.toCoverage.congr_simp
- CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks
- CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy
- CategoryTheory.Precoverage.toCoverage_le_toCoverage
- CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_small
Ancestors0
No ancestors.