lTensor_exact — Mathlib

English

The right-exactness results yield a description of the kernel of the induced map on quotients in terms of the image of the left-tensored map, i.e., ker(lTensor Q N.mkQ) = range(lTensor Q N.subtype).

Русский

Кернель индуцированного отображения совпадает с образoм левого тензорного отображения.

LaTeX

$$ker(lTensor Q N.mkQ) = range(lTensor Q N.subtype)$$

Lean4

/-- Tensoring an exact pair on the left gives an exact pair -/
theorem lTensor_exact : Exact (lTensor Q f) (lTensor Q g) :=
  by
  rw [exact_iff, ← Submodule.ker_mkQ (p := range (lTensor Q f)), ← lTensor.inverse_comp_lTensor Q hfg hg]
  apply symm
  apply LinearMap.ker_comp_of_ker_eq_bot
  rw [LinearMap.ker_eq_bot]
  exact (lTensor.equiv Q hfg hg).symm.injective

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