Structures · Category theory
CategoryTheory.Precoverage.HasIsos
A precoverage has isomorphisms if singleton presieves by isomorphisms are covering.
- Defined in
- Mathlib.CategoryTheory.Sites.Precoverage
- Shape
- One type argument · adds mem_coverings_of_isIso
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 by25
- CategoryTheory.Precoverage.toPretopology
- CategoryTheory.Precoverage.toGrothendieck_toPretopology_eq_toGrothendieck
- CategoryTheory.Precoverage.mem_coverings_of_isIso
- 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.Pseudofunctor.IsPrestack.of_precoverage
- CategoryTheory.MorphismProperty.coverPreserving_comap_forget
- CategoryTheory.MorphismProperty.isContinuous_comap_forget
- CategoryTheory.Precoverage.HasIsos.mem_coverings_of_isIso
- CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology
- CategoryTheory.Pseudofunctor.IsStack.of_precoverage
- CategoryTheory.Precoverage.toPretopology_toPrecoverage
- CategoryTheory.Precoverage.instContainsIdentitiesMorphismPropertyOfHasIsos
- CategoryTheory.Precoverage.ZeroHypercover.pushforward_toPreZeroHypercover
- CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology
- CategoryTheory.Precoverage.toPretopology.congr_simp
- CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft
- CategoryTheory.Precoverage.instHasIsosMin
- CategoryTheory.PreZeroHypercover.mem_iff_of_iso
- CategoryTheory.Precoverage.instHasIsosComap
Ancestors0
No ancestors.