isSmoothOfRelativeDimension_isStableUnderBaseChange

English

If a morphism f is smooth of relative dimension n, then any base change of f is also smooth of relative dimension n.

Русский

Если морфизм f гладок относительной размерности n, то любая базовая замена f сохраняет гладкость и размерность n.

LaTeX

$$IsSmoothOfRelativeDimension(n) is stable under base change$$

Lean4

/-- Smooth of relative dimension `n` is stable under base change. -/
theorem isSmoothOfRelativeDimension_isStableUnderBaseChange :
    MorphismProperty.IsStableUnderBaseChange (@IsSmoothOfRelativeDimension n) :=
  HasRingHomProperty.isStableUnderBaseChange <|
    locally_isStableUnderBaseChange isStandardSmoothOfRelativeDimension_respectsIso
      (isStandardSmoothOfRelativeDimension_isStableUnderBaseChange n)

Похожие утверждения