localization_away — Mathlib

English

Base change preserves standard smoothness with localization, i.e., if a base change is performed along a localization, the result remains standard smooth.

Русский

Базовое изменение при локализации сохраняет стандартную гладкость.

LaTeX

$$$\mathrm{baseChange\_IsStandardSmooth}(R,S,T) \Rightarrow \mathrm{IsStandardSmooth}(T, T\otimes_R S)$$$

Lean4

theorem localization_away (r : R) [IsLocalization.Away r S] : IsStandardSmoothOfRelativeDimension 0 R S where
  out :=
    ⟨_, _, _, inferInstance, SubmersivePresentation.localizationAway S r,
      Presentation.localizationAway_dimension_zero r⟩

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