## Stream: Is there code for X?

### Topic: The tensor product of two multilinear maps is a multiline...

#### Eric Wieser (Dec 01 2020 at 20:09):

Is there an equiv between the tensor product of two multilinear maps and the map over the tensor product of the inputs?

#### Reid Barton (Dec 01 2020 at 20:27):

I can't parse this--an equiv should be between two types but neither side seems to be a type.

#### Eric Wieser (Dec 01 2020 at 21:18):

I'll paste a prototype once I've worked out how to summon the instances I need to write it

#### Eric Wieser (Dec 01 2020 at 21:21):

The short version is (multilinear_map R M M' ⊗[R] multilinear_map R N N') ≃ multilinear_map R (λ (i : ι₁ ⊕ ι₂), i.elim M N) (M' ⊗[R] N')

#### Eric Wieser (Dec 01 2020 at 21:30):

The long version is:

import linear_algebra.tensor_product
import linear_algebra.multilinear

open_locale tensor_product

instance sum.elim.add_comm_monoid {ι₁ ι₂ : Type}
{M : ι₁ → Type*} [∀ i, add_comm_monoid (M i)]
{N : ι₂ → Type*} [∀ i, add_comm_monoid (N i)]
(i : ι₁ ⊕ ι₂)
: add_comm_monoid (i.elim M N) := by cases i; dsimp; apply_instance

instance sum.elim.semimodule {ι₁ ι₂ : Type} [decidable_eq ι₁] [decidable_eq ι₂]
(R : Type*) [semiring R]
{M : ι₁ → Type*} [∀ i, add_comm_monoid (M i)] [∀ i, semimodule R (M i)]
{N : ι₂ → Type*} [∀ i, add_comm_monoid (N i)] [∀ i, semimodule R (N i)]
(i : ι₁ ⊕ ι₂)
: semimodule R (i.elim M N) := by cases i; dsimp; apply_instance

def multilinear.tmul_aux {ι₁ ι₂ : Type} [decidable_eq ι₁] [decidable_eq ι₂]
(R : Type*) [comm_semiring R]
{M : ι₁ → Type*} [∀ i, add_comm_monoid (M i)] [∀ i, semimodule R (M i)]
{N : ι₂ → Type*} [∀ i, add_comm_monoid (N i)] [∀ i, semimodule R (N i)]
{M' : Type*} [add_comm_monoid M'] [semimodule R M']
{N' : Type*} [add_comm_monoid N'] [semimodule R N']
(a : multilinear_map R M M') (b : multilinear_map R N N') :
multilinear_map R (sum.elim M N) (M' ⊗[R] N')
:=
{ to_fun := λ v, a (λ i, v (sum.inl i)) ⊗ₜ b (λ i, v (sum.inr i)),
map_smul' := sorry }

def multilinear.tmul {ι₁ ι₂ : Type} [decidable_eq ι₁] [decidable_eq ι₂]
(R : Type*) [comm_semiring R]
{M : ι₁ → Type*} [∀ i, add_comm_monoid (M i)] [∀ i, semimodule R (M i)]
{N : ι₂ → Type*} [∀ i, add_comm_monoid (N i)] [∀ i, semimodule R (N i)]
{M' : Type*} [add_comm_monoid M'] [semimodule R M']
{N' : Type*} [add_comm_monoid N'] [semimodule R N'] :
(multilinear_map R M M' ⊗[R] multilinear_map R N N') ≃ₗ[R]
multilinear_map R (sum.elim M N) (M' ⊗[R] N')
:=
{ to_fun := λ m,
{ to_fun := multilinear.tmul_aux R sorry sorry, -- split up the tensor product
map_smul' := sorry },
inv_fun := sorry,
left_inv := sorry,
right_inv := sorry,
map_smul' := sorry, }


#### Eric Wieser (Dec 01 2020 at 21:30):

This is way overgeneralized for what I actually need, but maybe bits of it already exist

#### Reid Barton (Dec 01 2020 at 22:02):

There is a map in the -> direction but in general it isn't an isomorphism

#### Eric Wieser (Dec 01 2020 at 22:06):

Ok, guess I overgeneralized. I only care about tmul_aux really.

#### Eric Wieser (Dec 01 2020 at 22:07):

Which I think I can unsorry, but I wanted to check it doesn't exist somewhere

#### Eric Wieser (Dec 02 2020 at 09:42):

Here's the full sorry-free definition of tmux_aux (now multilinear_map.of_tmul):

Edit: #5179 so this doesn't get lost.

Last updated: May 07 2021 at 21:10 UTC