Constructions relating multilinear maps and tensor products.

def MultilinearMap.domCoprodDep {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} [(i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [(i : ι₁ ⊕ ι₂) → Module R (N i)] (a : MultilinearMap R (fun (i₁ : ι₁) => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun (i₂ : ι₂) => N (Sum.inr i₂)) N₂) : MultilinearMap R N (TensorProduct R N₁ N₂)

Given a family of modules N indexed by a type ι₁ ⊕ ι₂, a multilinear map from the modules N (.inl i₁) to N₁ and a multilinear map from the modules N (.inr i₁) to N₂, this is the induced multilinear map from all the modules N i to N₁ ⊗ N₂.

@[simp]

theorem MultilinearMap.domCoprodDep_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} [(i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [(i : ι₁ ⊕ ι₂) → Module R (N i)] (a : MultilinearMap R (fun (i₁ : ι₁) => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun (i₂ : ι₂) => N (Sum.inr i₂)) N₂) (v : (i : ι₁ ⊕ ι₂) → N i) : (a.domCoprodDep b) v = (a fun (i₁ : ι₁) => v (Sum.inl i₁)) ⊗ₜ[R] b fun (i₂ : ι₂) => v (Sum.inr i₂)

def MultilinearMap.domCoprodDep' {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} [(i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [(i : ι₁ ⊕ ι₂) → Module R (N i)] : TensorProduct R (MultilinearMap R (fun (i₁ : ι₁) => N (Sum.inl i₁)) N₁) (MultilinearMap R (fun (i₂ : ι₂) => N (Sum.inr i₂)) N₂) →ₗ[R] MultilinearMap R N (TensorProduct R N₁ N₂)

A more bundled version of MultilinearMap.domCoprodDep, as a linear map from the tensor product of spaces of multilinear maps.

@[simp]

theorem MultilinearMap.domCoprodDep'_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} [(i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [(i : ι₁ ⊕ ι₂) → Module R (N i)] (a : MultilinearMap R (fun (i₁ : ι₁) => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun (i₂ : ι₂) => N (Sum.inr i₂)) N₂) : domCoprodDep' (a ⊗ₜ[R] b) = a.domCoprodDep b

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.

@[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 : (i : ι₁ ⊕ ι₂) → (fun (x : ι₁ ⊕ ι₂) => N) i) : (a.domCoprod 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] : 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₂) : domCoprod' (a ⊗ₜ[R] b) = a.domCoprod 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 : ι₂ ≃ ι₄) : domDomCongr (σa.sumCongr σb) (a.domCoprod b) = (domDomCongr σa a).domCoprod (domDomCongr σb b)

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