English
Localization preserves smooth locus under the canonical map A → A_f^−, i.e., the preimage of smooth locus equals the smooth locus after localization.
Русский
Локализация сохраняет гладкость локуса под канонической связью A → A_f^−; прообраз гладкого локуса совпадает с локусом после локализации.
LaTeX
$$$\mathrm{comap}_{\mathrm{algebraMap}}^{-1}\big(\mathrm{smoothLocus}(R,A)\big) = \mathrm{smoothLocus}(R, A_f)$$$
Lean4
theorem smoothLocus_comap_of_isLocalization {Af : Type u} [CommRing Af] [Algebra A Af] [Algebra R Af]
[IsScalarTower R A Af] (f : A) [IsLocalization.Away f Af] :
PrimeSpectrum.comap (algebraMap A Af) ⁻¹' smoothLocus R A = smoothLocus R Af :=
by
ext p
let q := PrimeSpectrum.comap (algebraMap A Af) p
have : IsLocalization.AtPrime (Localization.AtPrime p.asIdeal) q.asIdeal :=
IsLocalization.isLocalization_isLocalization_atPrime_isLocalization (.powers f) _ p.asIdeal
refine Algebra.FormallySmooth.iff_of_equiv ?_
exact (IsLocalization.algEquiv q.asIdeal.primeCompl _ _).restrictScalars R
