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.
This can be thought of as combining
tensor_product.map, noting that the two operations can't be separated as the intermediate result
is not a
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
multilinear_map.dom_coprod that maps
((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to
(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.