# Documentation

Mathlib.LinearAlgebra.Multilinear.TensorProduct

# Constructions relating multilinear maps and tensor products. #

@[simp]
theorem MultilinearMap.domCoprod_apply {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [] {N₁ : Type u_6} [] [Module R N₁] {N₂ : Type u_7} [] [Module R N₂] {N : Type u_8} [] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) (v : ι₁ ι₂N) :
↑() v = (a fun i => v ()) ⊗ₜ[R] b fun i => v ()
def MultilinearMap.domCoprod {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [] {N₁ : Type u_6} [] [Module R N₁] {N₂ : Type u_7} [] [Module R N₂] {N : Type u_8} [] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) :
MultilinearMap R (fun x => N) (TensorProduct R N₁ N₂)

Given two multilinear maps (ι₁ → N) → N₁ and (ι₂ → N) → N₂, this produces the map (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂ by taking the coproduct of the domain and the tensor product of the codomain.

This can be thought of as combining Equiv.sumArrowEquivProdArrow.symm with TensorProduct.map, noting that the two operations can't be separated as the intermediate result is not a MultilinearMap.

While this can be generalized to work for dependent Π i : ι₁, N'₁ i instead of ι₁ → N, doing so introduces Sum.elim N'₁ N'₂ types in the result which are difficult to work with and not defeq to the simple case defined here. See this zulip thread.

Instances For
def MultilinearMap.domCoprod' {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [] {N₁ : Type u_6} [] [Module R N₁] {N₂ : Type u_7} [] [Module R N₂] {N : Type u_8} [] [Module R N] :
TensorProduct R (MultilinearMap R (fun x => N) N₁) (MultilinearMap R (fun x => N) N₂) →ₗ[R] MultilinearMap R (fun x => N) (TensorProduct R N₁ N₂)

A more bundled version of MultilinearMap.domCoprod that maps ((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.

Instances For
@[simp]
theorem MultilinearMap.domCoprod'_apply {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [] {N₁ : Type u_6} [] [Module R N₁] {N₂ : Type u_7} [] [Module R N₂] {N : Type u_8} [] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) :
MultilinearMap.domCoprod' (a ⊗ₜ[R] b) =
theorem MultilinearMap.domCoprod_domDomCongr_sumCongr {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {ι₃ : Type u_4} {ι₄ : Type u_5} [] {N₁ : Type u_6} [] [Module R N₁] {N₂ : Type u_7} [] [Module R N₂] {N : Type u_8} [] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) (σa : ι₁ ι₃) (σb : ι₂ ι₄) :

When passed an Equiv.sumCongr, MultilinearMap.domDomCongr distributes over MultilinearMap.domCoprod.