Theorems · Definition · linear algebra

TensorProduct.VanishesTrivially

(R : Type u_1) →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommGroup N] → [Module R N] → {ι : Type u_4} → [Fintype ι] → (ι → M) → (ι → N) → Prop

An expression $\sum_i m_i \otimes n_i$ in $M \otimes N$ vanishes trivially if there exist a finite index type $\kappa$ = Fin k, elements $(y_j)_{j \in \kappa}$ of $N$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$ such that for all $i$, $$n_i = \sum_j a_{ij} y_j$$ and for all $j$, $$\sum_i a_{ij} m_i = 0.$$ Note that this condition is not symmetric in $M$ and $N$. (The terminology "trivial" comes from [Stacks 00HK](https://stacks.math.columbia.edu/tag/00HK).)

Defined in

Mathlib.LinearAlgebra.TensorProduct.Vanishing

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleAddCommGroupModuleFintype