lTensor_mkQ — Mathlib

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)

Похожие утверждения