mathlib documentation

linear_algebra.multilinear.tensor_product

Constructions relating multilinear maps and tensor products. #

def multilinear_map.dom_coprod {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_semiring R] [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_6} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] {N : Type u_8} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) :
multilinear_map R (λ (_x : ι₁ ι₂), N) (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.sum_arrow_equiv_prod_arrow.symm with tensor_product.map, noting that the two operations can't be separated as the intermediate result is not a multilinear_map.

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.

Equations
@[simp]
theorem multilinear_map.dom_coprod_apply {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_semiring R] [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_6} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] {N : Type u_8} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) (v : ι₁ ι₂ → N) :
(a.dom_coprod b) v = a (λ (i : ι₁), v (sum.inl i)) ⊗ₜ[R] b (λ (i : ι₂), v (sum.inr i))
def multilinear_map.dom_coprod' {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_semiring R] [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_6} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] {N : Type u_8} [add_comm_monoid N] [module R N] :
multilinear_map R (λ (_x : ι₁), N) N₁ multilinear_map R (λ (_x : ι₂), N) N₂ →ₗ[R] multilinear_map R (λ (_x : ι₁ ι₂), N) (N₁ N₂)

A more bundled version of multilinear_map.dom_coprod that maps ((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.

Equations
@[simp]
theorem multilinear_map.dom_coprod'_apply {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} [comm_semiring R] [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_6} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] {N : Type u_8} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) :
theorem multilinear_map.dom_coprod_dom_dom_congr_sum_congr {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {ι₃ : Type u_4} {ι₄ : Type u_5} [comm_semiring R] [decidable_eq ι₁] [decidable_eq ι₂] [decidable_eq ι₃] [decidable_eq ι₄] {N₁ : Type u_6} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_7} [add_comm_monoid N₂] [module R N₂] {N : Type u_8} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) (σa : ι₁ ι₃) (σb : ι₂ ι₄) :

When passed an equiv.sum_congr, multilinear_map.dom_dom_congr distributes over multilinear_map.dom_coprod.