Constructions relating multilinear maps and tensor products. #
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.
While this can be generalized to work for dependent
Π i : ι₁, N'₁ i instead of
ι₁ → N, doing so
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.
A more bundled version of
MultilinearMap.domCoprod that maps
((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to
(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.