localization_base — Mathlib

English

Another facet of localization: in a diagram with R_m and S_m, étaleness persists under base changes of the base ring.

Русский

Ещё одна грань локализации: в диаграмме с R_m и S_m étale сохраняется при смене основания.

LaTeX

$$$[\text{FormallyEtale}(R,S_m)] \Rightarrow \text{FormallyEtale}(R_m,S_m)$$$

Lean4

theorem localization_base [FormallyEtale R Sₘ] : FormallyEtale Rₘ Sₘ :=
  FormallyEtale.iff_unramified_and_smooth.mpr
    ⟨FormallyUnramified.localization_base M, FormallySmooth.localization_base M⟩

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