Standard smooth charts over an affine target

If f : X ⟶ Y is smooth of relative dimension n and Y is affine, then every point of X has an affine open neighbourhood W on which the map Γ(Y, ⊤) → Γ(X, W) induced by f is standard smooth of relative dimension n. The defining charts of SmoothOfRelativeDimension n only provide this over some affine open of Y; shrinking them to basic opens and using that standard smoothness is stable under localization away from an element brings the source of the ring map up to all of Y.

It also records that smoothness on an open subscheme U ⊆ X yields standard smooth charts of f itself around the points of U, as for the smooth locus of a family of curves.

Main declarations

• SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension_appLE_top, in Mathlib's AlgebraicGeometry namespace: standard smooth charts whose ring map starts at the global sections of the affine target.
• SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension_of_comp_ι: standard smooth charts of f inside an open U ⊆ X on which f is smooth.

References

The proof is adapted from Mathlib's proof of AlgebraicGeometry.SmoothOfRelativeDimension.smoothOfRelativeDimension_comp in Mathlib.AlgebraicGeometry.Morphisms.Smooth (Apache-2.0): the same shrinking of the charts to basic opens via exists_basicOpen_le_appLE_of_appLE_of_isAffine, followed by composing with the localization away from r, here taken from the global sections of the affine target rather than from a chart of a second smooth morphism.

theorem AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension_appLE_top {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] (n : ℕ) [SmoothOfRelativeDimension n f] (x : ↥X) : ∃ (W : ↑X.affineOpens), x ∈ ↑W ∧ RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑W ⋯))

If f : X ⟶ Y is smooth of relative dimension n and Y is affine, then around every point of X there is an affine open W such that Γ(Y, ⊤) → Γ(X, W) is standard smooth of relative dimension n.

theorem AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension_of_comp_ι {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (n : ℕ) [SmoothOfRelativeDimension n (CategoryTheory.CategoryStruct.comp U.ι f)] {x : ↥X} (hx : x ∈ U) : ∃ (W : ↑Y.affineOpens) (V : ↑X.affineOpens) (_ : ↑V ≤ U) (_ : x ∈ ↑V) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑W), RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑W) (↑V) e))

If f : X ⟶ Y restricted to an open subscheme U ⊆ X is smooth of relative dimension n, then every point of U has an affine open neighbourhood V ⊆ U lying over an affine open W of Y such that Γ(Y, W) → Γ(X, V) is standard smooth of relative dimension n.

theorem TauCeti.AlgebraicGeometry.exists_isStandardSmoothOfRelativeDimension (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n (X ↘ AlgebraicGeometry.Spec ↧R)] (x : ↥X) : ∃ (W : ↑X.affineOpens), x ∈ ↑W ∧ RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom ((AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R X).app (Opposite.op ↑W)))

Around every point of a scheme smooth of relative dimension n over Spec R, there is an affine open whose ring of functions is standard smooth of relative dimension n over R.