English
For φ and hφ as above, map preserves the basic generators: map φ hφ (Localization.mk n d) = Localization.mk (φ n) ⟨φ d, hφ d.prop⟩.
Русский
При указанных φ и hφ отображение сохраняет строение локализации: map φ hφ (Localization.mk n d) = Localization.mk (φ n) ⟨φ d, hφ d.prop⟩.
LaTeX
$$$\mathrm{map}\,\phi\,\mathrm{h}\!\mathrm{φ}\bigl(\mathrm{Localization.mk}(n,d)\bigr) = \mathrm{Localization.mk}(\phi(n))\langle \phi(d), h\!\phi(d)\text{.prop} \rangle$$$
Lean4
theorem map_apply_ofFractionRing_mk [MonoidHomClass F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ S[X]⁰.comap φ) (n : R[X])
(d : R[X]⁰) :
map φ hφ (ofFractionRing (Localization.mk n d)) = ofFractionRing (Localization.mk (φ n) ⟨φ d, hφ d.prop⟩) := by
simp only [map, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_ofFractionRing_mk, Submonoid.mem_comap.mp (hφ d.2),
↓reduceDIte]
