Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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')

view this post on Zulip 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_add' := sorry,
  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_add' := sorry,
    map_smul' := sorry },
  inv_fun := sorry,
  left_inv := sorry,
  right_inv := sorry,
  map_add' := sorry,
  map_smul' := sorry, }

view this post on Zulip Eric Wieser (Dec 01 2020 at 21:30):

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

view this post on Zulip Reid Barton (Dec 01 2020 at 22:02):

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

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:06):

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

view this post on Zulip Eric Wieser (Dec 01 2020 at 22:07):

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

view this post on Zulip 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