English
Localization of a base ring yields a formally smooth base: R ⟶ R_m is formally smooth.
Русский
Локализация базового кольца даёт формально гладкое расширение: R ⟶ R_m формально гладкое.
LaTeX
$$$\operatorname{FormallySmooth}(R, R_m)$$$
Lean4
theorem localization_base [FormallySmooth R Sₘ] : FormallySmooth Rₘ Sₘ :=
by
constructor
intro Q _ _ I e f
letI := ((algebraMap Rₘ Q).comp (algebraMap R Rₘ)).toAlgebra
letI : IsScalarTower R Rₘ Q := IsScalarTower.of_algebraMap_eq' rfl
let f : Sₘ →ₐ[Rₘ] Q :=
by
refine { FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) with commutes' := ?_ }
intro r
change
(RingHom.comp (FormallySmooth.lift I ⟨2, e⟩ (f.restrictScalars R) : Sₘ →+* Q) (algebraMap _ _)) r =
algebraMap _ _ r
congr 1
refine IsLocalization.ringHom_ext M ?_
rw [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq, AlgHom.comp_algebraMap]
use f
ext
simp [f]
