vanishesTrivially_iff_sum_tmul_eq_zero

English

If the generated m_i cover M, then VanishesTrivially R m n is equivalent to the tensor sum equalling zero: VanishesTrivially R m n ⇔ ∑ i m_i ⊗ n_i = 0.

Русский

Если порождающие m_i покрывают M, то исчезновение тривиально эквивалентно нулю тензорной суммы: VanishesTrivially R m n ⇔ ∑ i m_i ⊗ n_i = 0.

LaTeX

$$$ \\text{VanishesTrivially}_R(m, n) \\iff \\sum_i m_i \\otimes n_i = 0$$$

Lean4

/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term].

Assume that the $m_i$ generate $M$. Then the expression $\sum_i m_i \otimes n_i$ vanishes
trivially if and only if it vanishes. -/
theorem vanishesTrivially_iff_sum_tmul_eq_zero (hm : Submodule.span R (Set.range m) = ⊤) :
    VanishesTrivially R m n ↔ ∑ i, m i ⊗ₜ n i = (0 : M ⊗[R] N) :=
  ⟨sum_tmul_eq_zero_of_vanishesTrivially R, vanishesTrivially_of_sum_tmul_eq_zero R hm⟩

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