Structures · Geometry
AlgebraicGeometry.Smooth
A morphism of schemes f : X ⟶ Y is smooth if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is smooth.
- Shape
- One type argument · adds smooth_appLE
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Every AlgebraicGeometry.Smooth is also a
Provided automatically by
Concrete types that are instances2
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Opens.toScheme
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- AlgebraicGeometry.Scheme.Hom.smooth_appLE
- AlgebraicGeometry.Smooth.smooth_appLE
- AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top
- AlgebraicGeometry.smooth_comp
- AlgebraicGeometry.Scheme.Hom.instIsIsoNormalizationPullbackOfSmooth
- AlgebraicGeometry.instSmoothSndScheme
- AlgebraicGeometry.instFlatOfSmooth
- AlgebraicGeometry.instSmoothFstScheme
- AlgebraicGeometry.instSmoothMorphismRestrict
- AlgebraicGeometry.Smooth.exists_isStandardSmooth
- AlgebraicGeometry.instSmoothResLE
- AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth