Theorems · Theorem · linear algebra

TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective

∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N],
  (∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n) ↔
    ∀ (M' : Submodule R M), Function.Injective ⇑(LinearMap.rTensor N M'.subtype)

Every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially if and only if for every submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Vanishing

Cited by

2 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleAddCommGroupModule