English
In the setting of right-exactness, the equality ker(lTensor Q N.mkQ) = range(lTensor Q N.subtype) describes the exactness at the left end for the quotient map induced by N.
Русский
Утверждается равенство между ядром и образом для модуля N в левом конце квотирования.
LaTeX
$$ker(lTensor Q N.mkQ) = range(lTensor Q N.subtype)$$
Lean4
/-- Right-exactness of tensor product -/
theorem lTensor_mkQ (N : Submodule R M) : ker (lTensor Q (N.mkQ)) = range (lTensor Q N.subtype) :=
by
rw [← exact_iff]
exact lTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)