English
There is a canonical linear equivalence between the localization of a submodule M′ and its realization as a submodule inside the localized module: M′.localized p ≃_Localization(p) LocalizedModule p M′.
Русский
Существует каноническое линейное эквивалентность между локализацией подмодуля M′ и его реализацией как подмодуля внутри локализованного модуля: M′.localized p ≃ Localization(p) LocalizedModule p M′.
LaTeX
$$$M'.\mathrm{localized}_p \cong_{\mathrm{Localization}(p)} \mathrm{LocalizedModule}_p M'$$$
Lean4
/-- The canonical isomorphism between the localization of a submodule and its realization
as a submodule in the localized module. -/
noncomputable def localizedEquiv : M'.localized p ≃ₗ[Localization p] LocalizedModule p M' :=
have := IsLocalization.linearMap_compatibleSMul p
IsLocalizedModule.linearEquiv p (M'.toLocalized p) (LocalizedModule.mkLinearMap _ _) |>.restrictScalars _
