English
Localizing a formally smooth algebra preserves formal smoothness: R → R_m and S → S_m with appropriate towers imply FormallySmooth R_m S_m.
Русский
Локализация формально гладкой алгебры сохраняет формальную гладкость: R → R_m и S → S_m с подходящими тензорными торами дают FormallySmooth R_m S_m.
LaTeX
$$$[\operatorname{FormallySmooth} R S] \Rightarrow \operatorname{FormallySmooth} R_m S_m$$$
Lean4
theorem of_isLocalization : FormallySmooth R Rₘ := by
constructor
intro Q _ _ I e f
have : ∀ x : M, IsUnit (algebraMap R Q x) := by
intro x
apply (IsNilpotent.isUnit_quotient_mk_iff ⟨2, e⟩).mp
convert (IsLocalization.map_units Rₘ x).map f
simp only [Ideal.Quotient.mk_algebraMap, AlgHom.commutes]
let this : Rₘ →ₐ[R] Q := { IsLocalization.lift this with commutes' := IsLocalization.lift_eq this }
use this
apply AlgHom.coe_ringHom_injective
refine IsLocalization.ringHom_ext M ?_
ext
simp
