tensor product 1 equal iff equal?

Stream: Is there code for X?

[Edison Xie]

import Mathlib

open TensorProduct

variable (K A B: Type*) [Field K] [Ring A] [Ring B] [Algebra K A] [Algebra K B]
  [Nontrivial A] [Nontrivial B] [hab : Algebra.IsCentral K (A ⊗[K] B)] (a1 a2 : A)

lemma test (h : a1 ⊗ₜ (1 : B) = a2 ⊗ₜ[K] (1 : B)) : a1 = a2 := by sorry

Do we have any theorems about it? (Or is it even true?)

[Johan Commelin]

This should follow from flatness, right?

[Eric Wieser]

@loogle "rtensor", Function.Injective

[loogle]

:search: LinearMap.lTensor_inj_iff_rTensor_inj, rTensor_injective_iff_lcomp_surjective, and 17 more

[Edison Xie]

hmmm yeah it surely should have something to do with flatness but I can't find a theorem that does the trick

[Edison Xie]

Or equivalently, should there be an injective lemma about Algebra.TensorProduct.includeLeft?

[Eric Wieser]

Is the proof just algebraMap_injective?

[Edison Xie]

(deleted)

[Edison Xie]

(deleted)

[Edison Xie]

why is it algebraMap_injective?

[Kevin Buzzard]

because algebraMap a = a tensor 1 (you have to find the right algebraMap_injective though, that's the exercise)

[Edison Xie]

Kevin Buzzard said:

because algebraMap a = a tensor 1.

you mean A ⊗[K] B as an A-algebra?

[Edison Xie]

and which algebraMap_injective are we talking about? NoZeroSmulDivisors.algebraMap_injective?

[Andrew Yang]

No this wouldn’t work because A is noncommutative so there is no algebra instance

[Edison Xie]

yeah the main problem is A is non-commutative

[Andrew Yang]

You probably want something like

lemma TensorProduct.flip_mk_injective {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N]
    [Module R M] [Module R N] [NoZeroSMulDivisors R N] [Module.Flat R M] (a : N) (ha : a ≠ 0) :
    Function.Injective ((TensorProduct.mk R M N).flip a) := by
  intro x y e
  apply (TensorProduct.rid R M).symm.injective
  apply Module.Flat.lTensor_preserves_injective_linearMap (M := M) (LinearMap.toSpanSingleton R N a)
    (smul_left_injective R ha)
  simpa using e

[Edison Xie]

Yes thank you! Is it in mathlib already? If not do you mind PR this? :))