English
The canonical linear map from ker g to ker (map) is defined by sending x in ker g to algebraMap_R_S x in the localized setting.
Русский
Каноническое линейное отображение от ядра $g$ к ядру сопряжённого отображения задаётся отправкой $x$ в ядро локализации через алгебраическое отображение.
LaTeX
$$$\\mathrm{toKerIsLocalization}(g)(x) = \\mathrm{algebraMap}_{R,S}(x) \\quad (x \\in \\ker g)$$$
Lean4
/-- The canonical linear map from the kernel of `g` to the kernel of its localization. -/
noncomputable def toKerIsLocalization (hy : M ≤ Submonoid.comap g T) :
RingHom.ker g →ₗ[R] RingHom.ker (IsLocalization.map Q g hy : S →+* Q)
where
toFun x := ⟨algebraMap R S x, by simp [RingHom.mem_ker, RingHom.mem_ker.mp x.property]⟩
map_add' x y := by simp only [Submodule.coe_add, map_add, AddMemClass.mk_add_mk]
map_smul' a
x := by simp only [SetLike.val_smul, smul_eq_mul, map_mul, id_apply, SetLike.mk_smul_of_tower_mk, Algebra.smul_def]
