Structures · Category theory
CategoryTheory.Precoverage.IsStableUnderComposition
A precoverage is stable under composition if the indexed composition
of coverings is again a covering.
Use Precoverage.comp_mem_coverings for less universe restrictions.
Note: This is stronger than the analogous requirement for a Pretopology, because
this is in general not equal to a Presieve.bind.
- Defined in
- Mathlib.CategoryTheory.Sites.Precoverage
- Shape
- One type argument · adds comp_mem_coverings
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 by28
- CategoryTheory.Precoverage.ZeroHypercover.bind
- CategoryTheory.Precoverage.toPretopology
- CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck
- CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition
- 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.ZeroHypercover.pushforward
- CategoryTheory.PreZeroHypercover.mem_of_iso
- CategoryTheory.Precoverage.comp_mem_coverings
- CategoryTheory.Pseudofunctor.IsPrestack.of_precoverage
- CategoryTheory.MorphismProperty.coverPreserving_comap_forget
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- CategoryTheory.Precoverage.ZeroHypercover.inter
- CategoryTheory.Precoverage.IsStableUnderComposition.comp_mem_coverings
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.Pseudofunctor.IsStack.of_precoverage
- CategoryTheory.Precoverage.toPretopology_toPrecoverage
- CategoryTheory.Precoverage.ZeroHypercover.pushforward_toPreZeroHypercover
- CategoryTheory.Precoverage.instIsStableUnderCompositionMin
- CategoryTheory.Precoverage.instIsStableUnderCompositionComap
- CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover
- CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology
- CategoryTheory.Precoverage.toPretopology.congr_simp
- CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft
- CategoryTheory.PreZeroHypercover.mem_iff_of_iso
- CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover
Ancestors0
No ancestors.