English
Let f: X → Y be a morphism of schemes and n a natural number. Then f is smooth of relative dimension n if and only if it is locally of standard smoothness of relative dimension n; equivalently, around every point of X there exists a localization of the target such that the localized morphism is standard smooth of relative dimension n.
Русский
Пусть f: X → Y — морфизм схем и n ∈ ℕ. Тогда f гладок относительно размерности n локально тогда и только тогда, когда локально относительно применить локализацию к целевой схеме так, чтобы получившийся морфизм был стандартно гладким относительно размерности n.
LaTeX
$$$IsSmoothOfRelativeDimension\,n\,f \;\Longleftrightarrow\; Locally\,(IsStandardSmoothOfRelativeDimension\,n)\,f$$$
Lean4
/-- The property of scheme morphisms `IsSmoothOfRelativeDimension n` is associated with the ring
homomorphism property `Locally (IsStandardSmoothOfRelativeDimension n)`. -/
instance : HasRingHomProperty (@IsSmoothOfRelativeDimension n) (Locally (IsStandardSmoothOfRelativeDimension n)) :=
by
apply HasRingHomProperty.locally_of_iff
· exact (isStandardSmoothOfRelativeDimension_localizationPreserves n).away
· exact isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n
· intro X Y f
rw [isSmoothOfRelativeDimension_iff]
