English
Let f: N → P be a linear map of R-modules. The kernel of the induced map obtained by tensoring with M over R is exactly the image of the kernel of f under tensoring with M.
Русский
Пусть f: N → P — линейное отображение модулей над R. Ядро отображения, полученного путём тензорного умножения на M, равно образу ядра f под тензоризацией на M.
LaTeX
$$$\ker\bigl(\mathrm{AlgebraTensorModule.lTensor}(S,M,f)\bigr) = \mathrm{range}\bigl(\mathrm{AlgebraTensorModule.lTensor}(S,M,\ker f).subtype\bigr).$$$
Lean4
theorem ker_lTensor_eq [Module.Flat R M] :
LinearMap.ker (AlgebraTensorModule.lTensor S M f) =
LinearMap.range (AlgebraTensorModule.lTensor S M (LinearMap.ker f).subtype) :=
by
rw [← LinearMap.exact_iff]
exact Module.Flat.lTensor_exact M (LinearMap.exact_subtype_ker_map f)
