English
The algebra isomorphism sends mk' of the localization to mk' in the target localization with the mapped element and a witness in M.
Русский
Алгебраическое изоморфизм отображает mk' локализации в mk' целевой локализации с образованным элементом и свидетелем в M.
LaTeX
$$$\text{algEquiv_mk'}(x,y) : \text{algEquiv } M S (\text{mk'} (Localization M) x y) = \text{mk'} S x y$$$
Lean4
/-- Definition of the natural algebra induced by the localization of an algebra.
Given an algebra `R → S`, a submonoid `R` of `M`, and a localization `Rₘ` for `M`,
let `Sₘ` be the localization of `S` to the image of `M` under `algebraMap R S`.
Then this is the natural algebra structure on `Rₘ → Sₘ`, such that the entire square commutes,
where `localization_map.map_comp` gives the commutativity of the underlying maps.
This instance can be helpful if you define `Sₘ := Localization (Algebra.algebraMapSubmonoid S M)`,
however we will instead use the hypotheses `[Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]` in lemmas
since the algebra structure may arise in different ways.
-/
noncomputable def localizationAlgebra : Algebra Rₘ Sₘ :=
(map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :
Rₘ →+* Sₘ).toAlgebra
