English
Let f: M → N and g: N → P be linear maps over a commutative ring R, with the exactness condition im(f) = ker(g). For any corresponding f' and g' with exactness, the kernel of the induced map on tensor products satisfies ker(TensorProduct.map g g') = range(lTensor N f') ⊔ range(rTensor N' f).
Русский
Пусть f: M → N и g: N → P — линейные отображения над коммутативной кольцом R, такие что образ f совпадает с ядром g. Для любых соответствующих f' и g' с точностью, ядро отображения на тензорном произведении удовлетворяет ker(TensorProduct.map g g') = range(lTensor N f') ⊔ range(rTensor N' f).
LaTeX
$$$\\ker(\\mathrm{TensorProduct.map}\\ g\\ g') = \\mathrm{range}(\\mathrm{lTensor}\\ N\\ f') \\; \\sqcup \\; \\mathrm{range}(\\mathrm{rTensor}\\ N'\\ f)$$$
Lean4
/-- Kernel of a product map (right-exactness of tensor product) -/
theorem map_ker : ker (TensorProduct.map g g') = range (lTensor N f') ⊔ range (rTensor N' f) :=
by
rw [← lTensor_comp_rTensor]
rw [ker_comp]
rw [← Exact.linearMap_ker_eq (rTensor_exact N' hfg hg)]
rw [← Submodule.comap_map_eq]
apply congr_arg₂ _ rfl
rw [range_eq_map, ← Submodule.map_comp, rTensor_comp_lTensor, Submodule.map_top]
rw [← lTensor_comp_rTensor, range_eq_map, Submodule.map_comp, Submodule.map_top]
rw [range_eq_top.mpr (rTensor_surjective M' hg), Submodule.map_top]
rw [Exact.linearMap_ker_eq (lTensor_exact P hfg' hg')]
