English
The kernel localization map is a localizing linear map; i.e., the localized module structure is obtained by the localization functor.
Русский
Локализующее отображение ядра является локализующим линейным отображением; структура локализации образуется через локализационный функтор.
LaTeX
$$$IsLocalizedModule\\ M\\big( \\mathrm{toKerIsLocalization}(S, Q, g, hy) \\big)$$$
Lean4
/-- The canonical linear map from the kernel of `g` to the kernel of its localization
is localizing. In other words, localization commutes with taking kernels. -/
theorem toKerIsLocalization_isLocalizedModule (hT : Submonoid.map g M = T) :
IsLocalizedModule M (toKerIsLocalization S Q g (hT.symm ▸ Submonoid.le_comap_map M)) :=
by
let e := LinearEquiv.ofEq _ _ (IsLocalization.ker_map (S := S) Q g hT).symm
convert_to IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ Algebra.idealMap S (RingHom.ker g))
apply IsLocalizedModule.of_linearEquiv
