English
Given an R-extension P → S and a multiplicative submonoid M of S, one can form a localized extension P.Ring → S' by localizing the base and lifting through IsLocalization. This yields a new extension with Ring equal to the localization of P.Ring and S' as the target.
Русский
Заданному R-расширению P→S и мультипликативному подмоноиду M S можно построить локализацию P.Ring → S', получив новое расширение с Ring равным локализации P.Ring.
LaTeX
$$$\\text{localization}(P,M):\\ \\mathrm{Extension}\\ R S'$, где\\ Ring = \\mathrm{Localization}(M\\!:\\!\\text{comap}(\\text{algebraMap }P.Ring S) M)$$$
Lean4
/-- An `R`-extension `P → S` gives an `R`-extension `Pₘ → Sₘ`.
Note that this is different from `baseChange` as the base does not change.
-/
noncomputable def localization (P : Extension.{w} R S) : Extension R S'
where
Ring := Localization (M.comap (algebraMap P.Ring S))
algebra₂ :=
(IsLocalization.lift (M := (M.comap (algebraMap P.Ring S))) (g := (algebraMap S S').comp (algebraMap P.Ring S))
(by simpa using fun x hx ↦ IsLocalization.map_units S' ⟨_, hx⟩)).toAlgebra
isScalarTower :=
by
letI : Algebra (Localization (M.comap (algebraMap P.Ring S))) S' :=
(IsLocalization.lift (M := (M.comap (algebraMap P.Ring S))) (g := (algebraMap S S').comp (algebraMap P.Ring S))
(by simpa using fun x hx ↦ IsLocalization.map_units S' ⟨_, hx⟩)).toAlgebra
apply IsScalarTower.of_algebraMap_eq'
rw [RingHom.algebraMap_toAlgebra, IsScalarTower.algebraMap_eq R P.Ring (Localization _), ← RingHom.comp_assoc,
IsLocalization.lift_comp, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
σ s := Localization.mk (P.σ (IsLocalization.sec M s).1) ⟨P.σ (IsLocalization.sec M s).2, by simp⟩
algebraMap_σ
s := by
simp [RingHom.algebraMap_toAlgebra, Localization.mk_eq_mk', IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul,
IsUnit.coe_liftRight, IsLocalization.sec_spec]
