localization_map — Mathlib

English

If e: A ≃ₐ[R] B is an algebra equivalence and A is unramified over R, then B is unramified over R.

Русский

Если e: A ≃ₐ[R] B — алгебра-эквивалентность и A неразветвлено над R, то B неразветвлено над R.

LaTeX

$$$[\text{Unramified } R A] \Rightarrow [\text{Unramified } R B]$ при $e: A \simeq_R B$$$

Lean4

theorem localization_map [FormallyUnramified R S] : FormallyUnramified Rₘ Sₘ :=
  by
  haveI : FormallyUnramified S Sₘ := FormallyUnramified.of_isLocalization (M.map (algebraMap R S))
  haveI : FormallyUnramified R Sₘ := FormallyUnramified.comp R S Sₘ
  exact FormallyUnramified.localization_base M

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