English
A kernel identity for tensor product with a quotient by an ideal I expresses ker(TensorProduct.mk R (R ⧸ I) Q 1) as I times the top submodule, aligning with standard short-exactness behavior in tensoring with quotients.
Русский
Ядро тензорного произведения с квотой по идеалу I равно I умноженному на верхний подмодуль.
LaTeX
$$ker(TensorProduct.mk R (R ⧸ I) Q 1) = I • ⊤$$
Lean4
theorem inverse_of_rightInverse_apply {h : P → N} (hgh : Function.RightInverse h g) (y : N ⊗[R] Q) :
(rTensor.inverse_of_rightInverse Q hfg hgh) ((rTensor Q g) y) =
Submodule.Quotient.mk (p := LinearMap.range (rTensor Q f)) y :=
by
simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]
rw [exact_iff] at hfg
apply LinearMap.congr_fun
apply TensorProduct.ext'
intro n q
suffices Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by simpa
rw [Submodule.Quotient.eq, ← TensorProduct.sub_tmul]
apply le_comap_range_rTensor f
rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]
