English
Formally unramified is preserved under localization at a prime: localization at a prime ideal yields a formally unramified map.
Русский
Формально немрамированность сохраняется при локализации вprime: локализация по prime-идеалу даёт формально немрамированный отображение.
LaTeX
$$$\\text{OfLocalizationPrime}(\\mathrm{FrmUnramified})$$$
Lean4
theorem ofLocalizationPrime : OfLocalizationPrime FormallyUnramified :=
by
intro R S _ _ f H
algebraize [f]
rw [FormallyUnramified, ← Algebra.unramifiedLocus_eq_univ_iff, Set.eq_univ_iff_forall]
intro x
let Rₓ := Localization.AtPrime (x.asIdeal.comap f)
let Sₓ := Localization.AtPrime x.asIdeal
have := Algebra.FormallyUnramified.of_isLocalization (Rₘ := Rₓ) (x.asIdeal.comap f).primeCompl
letI : Algebra Rₓ Sₓ := (Localization.localRingHom _ _ _ rfl).toAlgebra
have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _
exact Algebra.FormallyUnramified.comp R Rₓ Sₓ
