English
The map domCoprodDep' is linear in each factor; in particular, c ∙ (a ⊗ b) and (a ⊗ c ∙ b) behave linearly with respect to scalar multiplication and addition.
Русский
Функция domCoprodDep' линейна по каждому компоненту: скалярное умножение и сумма передаются через domCoprodDep'.
LaTeX
$$$domCoprodDep' (c\cdot a \otimes b) = c \cdot domCoprodDep' (a \otimes b), \; domCoprodDep' (a \otimes (c\cdot b)) = c \cdot domCoprodDep' (a \otimes b), \\ domCoprodDep' (a_1 \otimes b_1) + domCoprodDep' (a_2 \otimes b_2) = domCoprodDep' (a_1 \otimes b_1 + a_2 \otimes b_2).$$$
Lean4
/-- 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](
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Instances.20on.20.60sum.2Eelim.20A.20B.20i.60/near/218484619).
-/
@[simps! apply]
def domCoprod (a : MultilinearMap R (fun _ : ι₁ => N) N₁) (b : MultilinearMap R (fun _ : ι₂ => N) N₂) :
MultilinearMap R (fun _ : ι₁ ⊕ ι₂ => N) (N₁ ⊗[R] N₂) :=
domCoprodDep a b
