Documentation

Mathlib.LinearAlgebra.TensorProduct.Vanishing

Vanishing of elements in a tensor product of two modules #

Let $M$ and $N$ be modules over a commutative ring $R$. Recall that every element of $M \otimes N$ can be written as a finite sum $\sum_{i} m_i \otimes n_i$ of pure tensors (TensorProduct.exists_finset). We would like to determine under what circumstances such an expression vanishes.

Let us say that an expression $\sum_{i \in \iota} m_i \otimes n_i$ in $M \otimes N$ vanishes trivially (TensorProduct.VanishesTrivially) if there exist a finite index type $\kappa$, 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.$$ (The terminology "trivial" comes from Stacks 00HK.) It is not difficult to show (TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially) that if $\sum_i m_i \otimes n_i$ vanishes trivially, then it vanishes; that is, $\sum_i m_i \otimes n_i = 0$.

The equational criterion for vanishing (TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero), which appears as [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term], states that if the elements $m_i$ generate the module $M$, then $\sum_i m_i \otimes n_i = 0$ if and only if the expression $\sum_i m_i \otimes n_i$ vanishes trivially.

We also prove the following generalization (TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective). If the submodule $M' \subseteq M$ generated by the $m_i$ satisfies the property that the induced map $M' \otimes N \to M \otimes N$ is injective, then $\sum_i m_i \otimes n_i = 0$ if and only if the expression $\sum_i m_i \otimes n_i$ vanishes trivially. (In the case that $M = R$, this yields the equational criterion for flatness Module.Flat.iff_forall_isTrivialRelation.)

Conversely (TensorProduct.rTensor_injective_of_forall_vanishesTrivially), suppose that for every equation $\sum_i m_i \otimes n_i = 0$, the expression $\sum_i m_i \otimes n_i$ vanishes trivially. Then the induced map $M' \otimes N \to M \otimes N$ is injective for every submodule $M' \subseteq M$.

References #

TODO #

@[reducible, inline]
abbrev TensorProduct.VanishesTrivially (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] (m : ιM) (n : ιN) :

An expression $\sum_i m_i \otimes n_i$ in $M \otimes N$ vanishes trivially if there exist a finite index type $\kappa$, 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.)

Equations
Instances For
    theorem TensorProduct.sum_tmul_eq_zero_of_vanishesTrivially (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ιM} {n : ιN} (hmn : TensorProduct.VanishesTrivially R m n) :
    i : ι, m i ⊗ₜ[R] n i = 0

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

    If the expression $\sum_i m_i \otimes n_i$ vanishes trivially, then it vanishes. That is, $\sum_i m_i \otimes n_i = 0$.

    theorem TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ιM} {n : ιN} (hm : Submodule.span R (Set.range m) = ) (hmn : i : ι, m i ⊗ₜ[R] n i = 0) :

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

    Assume that the $m_i$ generate $M$. If the expression $\sum_i m_i \otimes n_i$ vanishes, then it vanishes trivially.

    theorem TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ιM} {n : ιN} (hm : Submodule.span R (Set.range m) = ) :
    TensorProduct.VanishesTrivially R m n i : ι, m i ⊗ₜ[R] n i = 0

    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 TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ιM} {n : ιN} (hm : Function.Injective (LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)) (hmn : i : ι, m i ⊗ₜ[R] n i = 0) :

    Equational criterion for vanishing [A. Altman and S. Kleiman, A term of commutative algebra (Lemma 8.16)][altman2021term], forward direction, generalization.

    Assume that the submodule $M' \subseteq M$ generated by the $m_i$ satisfies the property that the map $M' \otimes N \to M \otimes N$ is injective. If the expression $\sum_i m_i \otimes n_i$ vanishes, then it vanishes trivially.

    theorem TensorProduct.vanishesTrivially_iff_sum_tmul_eq_zero_of_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] {ι : Type u} [Fintype ι] {m : ιM} {n : ιN} (hm : Function.Injective (LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype)) :
    TensorProduct.VanishesTrivially R m n i : ι, m i ⊗ₜ[R] n i = 0

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

    Assume that the submodule $M' \subseteq M$ generated by the $m_i$ satisfies the property that the map $M' \otimes N \to M \otimes N$ is injective. Then the expression $\sum_i m_i \otimes n_i$ vanishes trivially if and only if it vanishes.

    theorem TensorProduct.rTensor_injective_of_forall_vanishesTrivially (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (hMN : ∀ {ι : Type u} [inst : Fintype ι] {m : ιM} {n : ιN}, i : ι, m i ⊗ₜ[R] n i = 0TensorProduct.VanishesTrivially R m n) (M' : Submodule R M) :

    Converse of TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective.

    Assume that every expression $\sum_i m_i \otimes n_i$ which vanishes also vanishes trivially. Then, for every submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.

    theorem TensorProduct.forall_vanishesTrivially_iff_forall_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] :
    (∀ {ι : Type u} [inst : Fintype ι] {m : ιM} {n : ιN}, i : ι, m i ⊗ₜ[R] n i = 0TensorProduct.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.

    theorem TensorProduct.forall_vanishesTrivially_iff_forall_FG_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] :
    (∀ {ι : Type u} [inst : Fintype ι] {m : ιM} {n : ιN}, i : ι, m i ⊗ₜ[R] n i = 0TensorProduct.VanishesTrivially R m n) ∀ (M' : Submodule R M), M'.FGFunction.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 finitely generated submodule $M' \subseteq M$, the map $M' \otimes N \to M \otimes N$ is injective.

    theorem TensorProduct.rTensor_injective_of_forall_FG_rTensor_injective (R : Type u) [CommRing R] {M : Type u} [AddCommGroup M] [Module R M] {N : Type u} [AddCommGroup N] [Module R N] (hMN : ∀ (M' : Submodule R M), M'.FGFunction.Injective (LinearMap.rTensor N M'.subtype)) (M' : Submodule R M) :

    If the map $M' \otimes N \to M \otimes N$ is injective for every finitely generated submodule $M' \subseteq M$, then it is in fact injective for every submodule $M' \subseteq M$.