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

Stream: Is there code for X?

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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, }

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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

import linear_algebra.tensor_product
import linear_algebra.multilinear

open_locale tensor_product

namespace sum.elim

instance {ι₁ ι₂ : 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 {ι₁ ι₂ : 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


end sum.elim

-- gh-5178
namespace function

/-- Dependent version of update_comp_eq_of_injective -/
lemma update_comp_eq_of_injective' {α β : Sort*} {γ : β → Sort*} [decidable_eq α] [decidable_eq β]
  (g : Π b, γ b) {f : α → β} (hf : function.injective f) (i : α) (a : γ (f i)) :
  (λ j, function.update g (f i) a (f j)) = function.update (λ i, g (f i)) i a :=
begin
  ext j,
  by_cases h : j = i,
  { rw h, simp },
  { have : f j ≠ f i := hf.ne h,
    simp [h, this] }
end

/-- Dependent version of update_comp_eq_of_not_mem_range -/
lemma update_comp_eq_of_not_mem_range' {α β : Type*} {γ : β → Type*} [decidable_eq β]
  (g : Π b, γ b) {f : α → β} {i : β} (a : γ i) (h : i ∉ set.range f) :
  (λ j, (function.update g i a) (f j)) = (λ j, g (f j)) :=
begin
  ext p,
  have : f p ≠ i,
  { by_contradiction H,
    push_neg at H,
    rw ← H at h,
    exact h (set.mem_range_self _) },
  simp [this],
end

end function

namespace multilinear_map

universes u

variables  {ι₁ ι₂ : Type*} [decidable_eq ι₁] [decidable_eq ι₂]
  (R : Type*) [comm_semiring R]
  {M : ι₁ → Type u} [∀ i, add_comm_monoid (M i)] [∀ i, semimodule R (M i)]
  {N : ι₂ → Type u} [∀ 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']

def of_tmul_aux
  (a : multilinear_map R M M') (b : multilinear_map R N N') :
  multilinear_map R (λ (i : ι₁ ⊕ ι₂), i.elim M N) (M' ⊗[R] N')
  :=
{ to_fun := λ v, a (λ i, v (sum.inl i)) ⊗ₜ b (λ i, v (sum.inr i)),
  map_add' := λ v i p q, begin
    cases i,
    {
      have : ∀ {α β : Type*} (a : α),
        (sum.inl a : α ⊕ β) ∉ set.range (@sum.inr α β) := by simp,
      iterate 3 {
        rw [function.update_comp_eq_of_injective' _ sum.injective_inl,
            function.update_comp_eq_of_not_mem_range' _ _ (this i)],},
      rw [a.map_add, tensor_product.add_tmul],
    },
    {
      have : ∀ {α β : Type*} (b : β),
        (sum.inr b : α ⊕ β) ∉ set.range (@sum.inl α β) := by simp,
      iterate 3 {
        rw [function.update_comp_eq_of_injective' _ sum.injective_inr,
            function.update_comp_eq_of_not_mem_range' _ _ (this i)],},
      rw [b.map_add, tensor_product.tmul_add],
    }
  end,
  map_smul' := λ v i c p, begin
    cases i,
    {
      have : ∀ {α β : Type*} (a : α),
        (sum.inl a : α ⊕ β) ∉ set.range (@sum.inr α β) := by simp,
      iterate 2 {
        rw [function.update_comp_eq_of_injective' _ sum.injective_inl,
            function.update_comp_eq_of_not_mem_range' _ _ (this i)],},
      rw [a.map_smul, tensor_product.smul_tmul'],
    },
    {
      have : ∀ {α β : Type*} (b : β),
        (sum.inr b : α ⊕ β) ∉ set.range (@sum.inl α β) := by simp,
      iterate 2 {
        rw [function.update_comp_eq_of_injective' _ sum.injective_inr,
            function.update_comp_eq_of_not_mem_range' _ _ (this i)]},
      rw [b.map_smul, tensor_product.tmul_smul],
    },
  end }

/-- Given a tensor product of two multilinear maps, produce a single multilinear map over the
sum of their indices into the tensor product of their codomains. -/
def of_tmul :
  multilinear_map R M M' ⊗ multilinear_map R N N' →ₗ[R]
  multilinear_map R (λ (i : ι₁ ⊕ ι₂), i.elim M N) (M' ⊗[R] N') :=
tensor_product.lift $ linear_map.mk₂ R (of_tmul_aux R)
  (λ m₁ m₂ n, by { ext, simp [of_tmul_aux, tensor_product.add_tmul] })
  (λ c m n,   by { ext, simp [of_tmul_aux, tensor_product.smul_tmul'] })
  (λ m n₁ n₂, by { ext, simp [of_tmul_aux, tensor_product.tmul_add] })
  (λ c m n,   by { ext, simp [of_tmul_aux, tensor_product.tmul_smul] })

@[simp] lemma of_tmul_apply_tmul (a : multilinear_map R M M') (b : multilinear_map R N N') (v) :
  of_tmul R (a ⊗ₜ b) v = a (λ i, v (sum.inl i)) ⊗ₜ b (λ i, v (sum.inr i)) := rfl

end multilinear_map

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