Tensor Product nonzero

Stream: Is there code for X?

[Elena Gutierrez]

I am trying to prove the following lemma:

import Mathlib.Algebra.Algebra.Basic
import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.TensorProduct

lemma tmul_nonzero_of_nonzero {V : Type} [AddCommGroup V] [Module ℚ V] (x : V)(hx: x ≠ 0) :
    (1 : ℝ) ⊗ₜ[ℚ] x ≠ 0 := sorry

Does anyone know if this is done in Mathlib?

[Eric Wieser]

What's the math proof?

[Riccardo Brasca]

We have docs#Basis.tensorProduct, so morally we have something much stronger, and even if the literal result is not there it shouldn't be hard.

[Riccardo Brasca]

Sorry, this was nonsense.

[Riccardo Brasca]

This works, but it's probably not the best proof.

import Mathlib

lemma tmul_nonzero_of_nonzero {V : Type} [AddCommGroup V] [Module ℚ V] (x : V) (hx: x ≠ 0) :
    (1 : ℝ) ⊗ₜ[ℚ] x ≠ 0 := by
  let b := Module.Free.chooseBasis ℚ V
  let f := Algebra.TensorProduct.basisAux ℝ b
  intro h
  have : f ((1 : ℝ) ⊗ₜ[ℚ] x) = 0 := by simp [h]
  rw [Algebra.TensorProduct.basisAux_tmul, one_smul] at this
  have H : (Finsupp.mapRange (algebraMap ℚ ℝ) (by simp) (b.repr x)).support = ∅ := by simp [this]
  rw [Finsupp.support_mapRange_of_injective (by simp) (b.repr x) (algebraMap ℚ ℝ).injective] at H
  simp only [Finsupp.support_eq_empty, AddEquivClass.map_eq_zero_iff] at H
  exact hx H

[Riccardo Brasca]

Ah, this is the proof I was thinking:

import Mathlib

lemma tmul_nonzero_of_nonzero {V : Type} [AddCommGroup V] [Module ℚ V] (x : V) (hx: x ≠ 0) :
    (1 : ℝ) ⊗ₜ[ℚ] x ≠ 0 := by
  let b := Module.Free.chooseBasis ℚ V
  let B := Algebra.TensorProduct.basis ℝ b
  intro h
  apply hx
  exact b.forall_coord_eq_zero_iff.1 (fun i ↦ by simpa using B.forall_coord_eq_zero_iff.2 h i)

[Riccardo Brasca]

Essentially I introduce a ℚ-basis b of V, that gives an ℝ-basis B of ℝ ⊗ V. Now, simp is smart enough to understand that the coordinates of 1 ⊗ x satisfy the obvious relation, so we can conclude.

[Riccardo Brasca]

Here is a general version.

import Mathlib

lemma tmul_nonzero_of_nonzero {R S M : Type*} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S]
    [NoZeroSMulDivisors R S] [AddCommGroup M] [Module R M] [Module.Free R M] {x : M} (hx: x ≠ 0) :
    (1 : S) ⊗ₜ[R] x ≠ 0 :=
  let b := Module.Free.chooseBasis R M
  let B := Algebra.TensorProduct.basis S b
  fun h ↦ hx <| b.forall_coord_eq_zero_iff.1  <|
    fun i ↦ NoZeroSMulDivisors.algebraMap_injective R S <|
    by simpa using B.forall_coord_eq_zero_iff.2 h i

I don't think that mathematically it is possible to do better.

[Eric Wieser]

Or maybe mathlib wants:

lemma one_tmul_injective {R S M : Type*} [CommRing R] [Ring S] [Algebra R S] [Nontrivial S]
    [NoZeroSMulDivisors R S] [AddCommGroup M] [Module R M] [Module.Free R M] {x : M} :
    Function.Injective (fun m : M => (1 : S) ⊗ₜ[R] m) := by
  intros x y h
  have b := Module.Free.chooseBasis R M
  let B := Algebra.TensorProduct.basis S b
  rw [b.ext_elem_iff]
  simpa [B.ext_elem_iff, (NoZeroSMulDivisors.algebraMap_injective R S).eq_iff] using h

[Eric Wieser]

Is negation needed to make this true?

[Riccardo Brasca]

Eric Wieser said:

Is negation needed to make this true?

I don't think so. Using semirings in Algebra.TensorProduct.basis seems fine without any modification.

[Riccardo Brasca]

#10988

[Eric Wieser]

docs#NoZeroSMulDivisors.algebraMap_injective isn't generalized either

[Eric Wieser]

Probably we need a SMul version of docs#IsCancelMulZero

[Riccardo Brasca]

Yes, that one is probably false.

[Elena Gutierrez]

Riccardo Brasca ha dicho:

Ah, this is the proof I was thinking:

import Mathlib

lemma tmul_nonzero_of_nonzero {V : Type} [AddCommGroup V] [Module ℚ V] (x : V) (hx: x ≠ 0) :
    (1 : ℝ) ⊗ₜ[ℚ] x ≠ 0 := by
  let b := Module.Free.chooseBasis ℚ V
  let B := Algebra.TensorProduct.basis ℝ b
  intro h
  apply hx
  exact b.forall_coord_eq_zero_iff.1 (fun i ↦ by simpa using B.forall_coord_eq_zero_iff.2 h i)

Thank you so much!!

[Kevin Buzzard]

Eric Wieser said:

What's the math proof?

$\mathbb{R}$ is flat over $\mathbb{Q}$.

[Riccardo Brasca]

Kevin Buzzard said:

Eric Wieser said:

What's the math proof?

$\mathbb{R}$ is flat over $\mathbb{Q}$.

You mean faithfully flat? Flatness is not enough (the vanishing of 1 ⊗ x doesn't tell you anything at primes not in the image of the map between the Spec)

[Kevin Buzzard]

It preserves the injection from $\mathbb{Q}$ sending 1 to $v$ so flatness is enough, no?

[Riccardo Brasca]

Ah, you mean that the module is flat, not ℝ.
I mean, ℚ is a flat ℤ-module, but taking M = ℤ/2ℤ you have x ∈ M different from 0 such that 1 ⊗ x = 0 ∈ M ⊗ ℚ.

[Kevin Buzzard]

Right but there the map from $\Z$ to $M$ isn't injective, so yeah I need that too :-)

[Riccardo Brasca]

The thing is the following: we have a R-algebra S and an R-module M with 0 ≠ x ∈ M. When is x ⊗ 1 ∈ M ⊗ S ≠ 0? I see two situation:

• R → S is faithfully flat (I have to check the details, but it seems ok)
• M is flat as R-module and R → S is injective (tensor R → S with M).

[Kevin Buzzard]

Yes you're right -- I meant the second one. I guess both conditions are implied by R is a field and S is nonzero, which is what we have here

[Riccardo Brasca]

The first point holds since faithfully flat morphisms are universally injective, so, tensoring R → S (that is injective) with M we get an injective map (regardless of flatness of M).

[Antoine Chambert-Loir]

Kevin Buzzard said:

Eric Wieser said:

What's the math proof?

$\mathbb{R}$ is flat over $\mathbb{Q}$.

How do you prove this without knowing that vector spaces gave bases and essentially doing Riccardo's proof?

[Kevin Buzzard]

I was answering Eric's question, which was asked before Ricardo's contribution :-) (but I agree!)