Structures · Geometry
AlgebraicGeometry.UniversallyOpen
A morphism of schemes f : X ⟶ Y is universally open if the base change X ×[Y] Y' ⟶ Y'
along any morphism Y' ⟶ Y is (topologically) an open map.
- Shape
- One type argument · adds universally_isOpenMap
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- CategoryTheory.Limits.pullback
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- AlgebraicGeometry.Scheme.Hom.isOpenMap
- AlgebraicGeometry.UniversallyOpen.universally_isOpenMap
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen
- AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian
- AlgebraicGeometry.UniversallyOpen.out
- AlgebraicGeometry.UniversallyOpen.snd
- AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1
- AlgebraicGeometry.UniversallyOpen.fst
- AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen_1
- AlgebraicGeometry.GeometricallyConnected.comp
- AlgebraicGeometry.GeometricallyIrreducible.comp
- AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian
- AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1
- AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen
- AlgebraicGeometry.UniversallyOpen.instCompScheme
Ancestors0
No ancestors.