rTensor_mkQ — Mathlib

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)

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