Structures · Category theory
CategoryTheory.MorphismProperty.IsLocalAtTarget
A property of morphisms P in C is local at the target with respect to the precoverage K if
it respects isomorphisms, and:
P holds for f : X ⟶ Y if and only if it holds for the restrictions of f to Uᵢ for a
0-hypercover {Uᵢ} of Y in the precoverage K.
- Shape
- 2 explicit arguments · adds pullbackSnd, of_forall_pullbackSnd
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- AlgebraicGeometry.Scheme
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- CategoryTheory.MorphismProperty.IsLocalAtTarget.pullbackSnd
- CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target
- CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover
- CategoryTheory.MorphismProperty.IsLocalAtTarget.of_forall_pullbackSnd
- CategoryTheory.MorphismProperty.of_zeroHypercover_target
- CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover
- CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback
- CategoryTheory.eq_of_zeroHypercover_target
- CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects
- CategoryTheory.MorphismProperty.IsLocalAtTarget.of_le
- CategoryTheory.MorphismProperty.IsLocalAtTarget.inf
- CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_forall_pullbackSnd