English
The canonical mapping shows that the localized kernel equals the kernel after extending scalars to the localization: localized'_ker_eq_ker_localizedMap.
Русский
Каноническое отображение показывает, что локализованное ядро совпадает с ядром после расширения скаляра до локализации: localized'_ker_eq_ker_localizedMap.
LaTeX
$$$\ker g\; localized'\; S\; p\; f = \ker\Big(\mathrm{map}\; p\; f\; f'\; g\Big).extendScalars\;p\;S$$$
Lean4
/-- The canonical map to the kernel of the localization of `g` is localizing.
In other words, localization commutes with kernels. -/
theorem toKerLocalized_isLocalizedModule (g : M →ₗ[R] P) : IsLocalizedModule p (toKerIsLocalized p f f' g) :=
let e : Submodule.localized' S p f (ker g) ≃ₗ[S] ker ((map p f f' g).extendScalarsOfIsLocalization p S) :=
LinearEquiv.ofEq _ _ (localized'_ker_eq_ker_localizedMap S p f f' g)
IsLocalizedModule.of_linearEquiv p (Submodule.toLocalized' S p f (ker g)) (e.restrictScalars R)
