Structures · Category theory
CategoryTheory.MorphismProperty.DescendsAlong
P descends along Q if whenever Q holds for X ⟶ Z,
P holds for X ×[Z] Y ⟶ X implies P holds for Y ⟶ Z.
- Shape
- 2 explicit arguments · adds of_isPullback
Extends0
Extends nothing: this is a root of the hierarchy.
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 by14
- CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong
- CategoryTheory.MorphismProperty.iff_of_isPullback
- CategoryTheory.MorphismProperty.DescendsAlong.of_isPullback
- CategoryTheory.MorphismProperty.eq_of_isomorphisms_descendsAlong
- CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong
- CategoryTheory.MorphismProperty.of_pullback_snd_of_descendsAlong
- CategoryTheory.MorphismProperty.DescendsAlong.inf
- AlgebraicGeometry.HasAffineProperty.descendsAlong_of_affineAnd
- AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget
- CategoryTheory.MorphismProperty.instDescendsAlongDiagonalOfRespectsIsoOfIsStableUnderBaseChange
- CategoryTheory.MorphismProperty.pullback_fst_iff
- CategoryTheory.MorphismProperty.DescendsAlong.of_le
- CategoryTheory.MorphismProperty.pullback_snd_iff
- CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
Ancestors0
No ancestors.