Structures · Geometry
AlgebraicGeometry.SmoothOfRelativeDimension
A morphism of schemes f : X ⟶ Y is smooth of relative dimension n if for each x : X there
exists an affine open neighborhood V of x and an affine open neighborhood U of
f.base x with V ≤ f ⁻¹ᵁ U such that the induced map Γ(Y, U) ⟶ Γ(X, V) is
standard smooth of relative dimension n.
- Shape
- 2 explicit arguments · adds exists_isStandardSmoothOfRelativeDimension
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- OfNat.ofNat
- HAdd.hAdd
How is a type an instance?
Loading the hierarchy index…
Assumed by5
- AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension
- AlgebraicGeometry.SmoothOfRelativeDimension.smooth
- AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatCompScheme
- AlgebraicGeometry.smoothOfRelativeDimension_comp
- AlgebraicGeometry.IsSmoothOfRelativeDimension.isSmooth
Ancestors0
No ancestors.