Structures · Category theory
CategoryTheory.MorphismProperty.IsStableUnderBaseChange
A morphism property is IsStableUnderBaseChange if the base change of such a morphism
still falls in the class.
- Shape
- One type argument · adds of_isPullback
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- CategoryTheory.Functor
- AlgebraicGeometry.Scheme
- TopCat
- SSet
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by204
- CategoryTheory.MorphismProperty.Over.pullback
- AlgebraicGeometry.Scheme.Cover.pullbackHom
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone
- CategoryTheory.MorphismProperty.of_isPullback
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.prop_trans
- CategoryTheory.MorphismProperty.pretopology
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued
- AlgebraicGeometry.Scheme.pretopology
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData
- AlgebraicGeometry.Scheme.Cover.toPresieveOver
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.trans
- AlgebraicGeometry.Scheme.Cover.toPresieveOverProp
- AlgebraicGeometry.Scheme.Cover.pullbackHom_map
- CategoryTheory.MorphismProperty.Over.pullbackComp
- AlgebraicGeometry.Scheme.smallPretopology
- CategoryTheory.MorphismProperty.Over.mapPullbackAdj
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimit
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOver
- CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback
- AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp'
- CategoryTheory.MorphismProperty.Over.pullbackMapHomPullback
- AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff
- CategoryTheory.MorphismProperty.coverage
- AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc
- CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso
- CategoryTheory.MorphismProperty.overPullbackMap
- AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
- CategoryTheory.MorphismProperty.iff_of_isPullback
- AlgebraicGeometry.Scheme.overPretopology
- CategoryTheory.MorphismProperty.Over.pullbackCongr
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone
- CategoryTheory.MorphismProperty.pullbackLift_fst_snd
- AlgebraicGeometry.Scheme.smallGrothendieckTopology_eq_toGrothendieck_smallPretopology
- CategoryTheory.MorphismProperty.Over.pullbackCongr_hom_app_left_fst
- CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology
- CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq
- AlgebraicGeometry.Scheme.mem_pretopology_iff
- AlgebraicGeometry.Scheme.locallyCoverDense_of_le
- CategoryTheory.MorphismProperty.eq_of_isomorphisms_descendsAlong
- AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst
- CategoryTheory.MorphismProperty.relative_map
- AlgebraicGeometry.Scheme.Cover.toPresieveOver_le_arrows_iff
- CategoryTheory.MorphismProperty.grothendieckTopology
Ancestors0
No ancestors.