lTensor_injective_iff_injective — Mathlib

English

If exactness holds after rTensor with M, then the range of l12 is contained in the kernel of l23.

Русский

Если после rTensor-s M последовательность точна, то образ l12 принадлежит ядру l23.

LaTeX

$$If $l_{12}:N_1\to N_2$, $l_{23}:N_2\to N_3$ and $\mathrm{Function.Exact}(l_{12}\!\rTensor M)(l_{23}\!\rTensor M)$, then $\operatorname{Im}(l_{12}) \subseteq \ker(l_{23})$.$$

Lean4

@[simp]
theorem lTensor_injective_iff_injective [Module.FaithfullyFlat R M] :
    Function.Injective (f.lTensor M) ↔ Function.Injective f :=
  by
  rw [← LinearMap.exact_zero_iff_injective (M ⊗[R] Unit), ← LinearMap.exact_zero_iff_injective Unit]
  conv_rhs => rw [← lTensor_exact_iff_exact R M]
  simp

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