Constructions relating multilinear maps and tensor products.

@[simp]

theorem MultilinearMap.domCoprod_apply {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : Type u_8} [AddCommMonoid N] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) (v : ι₁ ⊕ ι₂ → N) : ↑(MultilinearMap.domCoprod a b) v = (↑a fun i => v (Sum.inl i)) ⊗ₜ[R] ↑b fun i => v (Sum.inr i)

def MultilinearMap.domCoprod {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : Type u_8} [AddCommMonoid N] [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.

def MultilinearMap.domCoprod' {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : Type u_8} [AddCommMonoid N] [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₂.

@[simp]

theorem MultilinearMap.domCoprod'_apply {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : Type u_8} [AddCommMonoid N] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) : ↑MultilinearMap.domCoprod' (a ⊗ₜ[R] b) = MultilinearMap.domCoprod a b

theorem MultilinearMap.domCoprod_domDomCongr_sumCongr {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {ι₃ : Type u_4} {ι₄ : Type u_5} [CommSemiring R] {N₁ : Type u_6} [AddCommMonoid N₁] [Module R N₁] {N₂ : Type u_7} [AddCommMonoid N₂] [Module R N₂] {N : Type u_8} [AddCommMonoid N] [Module R N] (a : MultilinearMap R (fun x => N) N₁) (b : MultilinearMap R (fun x => N) N₂) (σa : ι₁ ≃ ι₃) (σb : ι₂ ≃ ι₄) : MultilinearMap.domDomCongr (Equiv.sumCongr σa σb) (MultilinearMap.domCoprod a b) = MultilinearMap.domCoprod (MultilinearMap.domDomCongr σa a) (MultilinearMap.domDomCongr σb b)

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