English
Let I be an ideal of R. The ideal map of I into S equals the composition of the localized-to-S map with the localized equivalence coming from localization, i.e., the structure of how I sits in S via localization is given by a canonical linear-isomorphism followed by the localized map.
Русский
Пусть I — идеал R. Отображение I в S через идеал-мэппинг равно композиции локализации и локализованного тождественного отображения, полученного из локализации.
LaTeX
$$$\\mathrm{Algebra.idealMap}_S I = (\\mathrm{LinearEquiv.ofEq}(\\operatorname{Localized}_0^{p}(\\mathrm{Algebra.linearMap}_{R}^{S}) I)\\text{ toLinearMap}) \\circ \\mathrm{Submodule.toLocalized}_p(\\mathrm{Algebra.linearMap}_{R}^{S}) I$$$
Lean4
theorem idealMap_eq_ofEq_comp_toLocalized₀ (I : Ideal R) :
Algebra.idealMap S I =
(LinearEquiv.ofEq _ _ <| Ideal.localized₀_eq_restrictScalars_map S p I).toLinearMap ∘ₗ
Submodule.toLocalized₀ p (Algebra.linearMap R S) I :=
rfl
