R^m tensor R^n = R^{m x n}

Stream: Is there code for X?

[Kevin Buzzard]

Do we have any of the following? (given one, the others should be straightforward I hope...)

import Mathlib.RingTheory.TensorProduct.Basic

open scoped TensorProduct

variable {R : Type*} [CommRing R] (m n : Type*)

def isom [Finite m] : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] ((m × n) → R) := sorry

def isom' [Finite n] : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] ((m × n) → R) := sorry

def isom'' [Finite m] : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] (m → n → R) := sorry

def isom''' [Finite n] : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] (m → n → R) := sorry

I only need the variant where both m and n are finite, but my instinct is that you only need one of them to be finite. Just to be clear, I don't want a random isomorphism (if m and n are finite then one can construct such a thing via a dimension count), I want the map sending f : m -> R tensor g : n -> R to the function sending (a,b) to f a * g b.

[Eric Wieser]

I think this is basically docs#Basis.tensorProduct, right?

[Eric Wieser]

... maybe with quite a few extra steps

[Eric Wieser]

docs#finsuppTensorFinsupp is much closer

[Eric Wieser]

and docs#finsuppTensorFinsuppLid even more so

[Kevin Buzzard]

The problem with these is that in the examples above one of m -> R and n -> R may not be a finsupp.

[Kevin Buzzard]

Aah, I can use docs#finsuppTensorFinsuppLid with kappa={1} and N=n->R :-)

[Kevin Buzzard]

or docs#TensorProduct.finsuppScalarLeft and then I don't need an artificial singleton type. Thanks!

[Kevin Buzzard]

PS shame this doesn't work:

def isom'' [Finite m] : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] (m → n → R) := calc
  ((m → R) ⊗[R] (n → R)) ≃ₗ[R] ((m →₀ R) ⊗[R] (n → R)) := by sorry
  _                      ≃ₗ[R] (m →₀ (n → R)) := by sorry
  _                      ≃ₗ[R] m → n → R := by sorry

(errors everywhere)

[Eric Wieser]

There's a PR somewhere that makes (a worse version of) that work

[Kevin Buzzard]

noncomputable def isom'' [Finite m] [DecidableEq m] : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] (m → n → R) :=
  (LinearEquiv.rTensor (n → R) (Finsupp.linearEquivFunOnFinite R R m).symm : ((m → R) ⊗[R] (n → R)) ≃ₗ[R] ((m →₀ R) ⊗[R] (n → R))).trans
  ((TensorProduct.finsuppScalarLeft _ _ _ : ((m →₀ R) ⊗[R] (n → R)) ≃ₗ[R] (m →₀ (n → R))).trans
  ((Finsupp.linearEquivFunOnFinite R _ m) : (m →₀ (n → R)) ≃ₗ[R] m → n → R))