English
Analogous right-exactness result for rTensor with mkQ; describes the kernel equality for the right tensor map with quotients.
Русский
Аналогично для правого тензора: ядро отображения mkQ для rTensor описывается через образ правого тензора.
LaTeX
$$ker( rTensor Q N.mkQ ) = range( rTensor Q N.subtype )$$
Lean4
/-- Right-exactness of tensor product (`rTensor`) -/
theorem rTensor_mkQ (N : Submodule R M) : ker (rTensor Q N.mkQ) = range (rTensor Q N.subtype) :=
by
rw [← exact_iff]
exact rTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)