feat(linear_algebra/multilinear): Add multilinear_map.coprod (#5182)

src/linear_algebra/multilinear.lean

@@ -558,6 +558,74 @@ instance : semimodule R' (multilinear_map A M₁ M₂) :=
 
 end semimodule
 
+
+section dom_coprod
+
+open_locale tensor_product
+
+variables {ι₁ ι₂ : Type*} [decidable_eq ι₁] [decidable_eq ι₂]
+variables {N₁ : Type*} [add_comm_monoid N₁] [semimodule R N₁]
+variables {N₂ : Type*} [add_comm_monoid N₂] [semimodule R N₂]
+variables {N : Type*} [add_comm_monoid N] [semimodule R 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](
+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 dom_coprod
+  (a : multilinear_map R (λ _ : ι₁, N) N₁) (b : multilinear_map R (λ _ : ι₂, N) N₂) :
+  multilinear_map R (λ _ : ι₁ ⊕ ι₂, N) (N₁ ⊗[R] N₂) :=
+have inl_disjoint : ∀ {α β : Type*} (a : α),
+  (sum.inl a : α ⊕ β) ∉ set.range (@sum.inr α β) := by simp,
+have inr_disjoint : ∀ {α β : Type*} (b : β),
+  (sum.inr b : α ⊕ β) ∉ set.range (@sum.inl α β) := by simp,
+{ to_fun := λ v, a (λ i, v (sum.inl i)) ⊗ₜ b (λ i, v (sum.inr i)),
+  map_add' := λ v i p q, begin
+    cases i,
+    { iterate 3 {
+        rw [function.update_comp_eq_of_injective' _ sum.injective_inl,
+            function.update_comp_eq_of_not_mem_range' _ _ (inl_disjoint i)],},
+      rw [a.map_add, tensor_product.add_tmul], },
+    { iterate 3 {
+        rw [function.update_comp_eq_of_injective' _ sum.injective_inr,
+            function.update_comp_eq_of_not_mem_range' _ _ (inr_disjoint i)],},
+      rw [b.map_add, tensor_product.tmul_add], }
+  end,
+  map_smul' := λ v i c p, begin
+    cases i,
+    { iterate 2 {
+        rw [function.update_comp_eq_of_injective' _ sum.injective_inl,
+            function.update_comp_eq_of_not_mem_range' _ _ (inl_disjoint i)],},
+      rw [a.map_smul, tensor_product.smul_tmul'], },
+    { iterate 2 {
+        rw [function.update_comp_eq_of_injective' _ sum.injective_inr,
+            function.update_comp_eq_of_not_mem_range' _ _ (inr_disjoint i)]},
+      rw [b.map_smul, tensor_product.tmul_smul], },
+  end }
+
+/-- A more bundled version of `multilinear_map.dom_coprod` that maps
+`((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂)` to `(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂`. -/
+def dom_coprod' :
+  multilinear_map R (λ _ : ι₁, N) N₁ ⊗[R] multilinear_map R (λ _ : ι₂, N) N₂ →ₗ[R]
+  multilinear_map R (λ _ : ι₁ ⊕ ι₂, N) (N₁ ⊗[R] N₂) :=
+tensor_product.lift $ linear_map.mk₂ R (dom_coprod)
+  (λ m₁ m₂ n, by { ext, simp only [dom_coprod_apply, tensor_product.add_tmul, add_apply] })
+  (λ c m n,   by { ext, simp only [dom_coprod_apply, tensor_product.smul_tmul', smul_apply] })
+  (λ m n₁ n₂, by { ext, simp only [dom_coprod_apply, tensor_product.tmul_add, add_apply] })
+  (λ c m n,   by { ext, simp only [dom_coprod_apply, tensor_product.tmul_smul, smul_apply] })
+
+end dom_coprod
+
 section
 
 variables (R ι) (A : Type*) [comm_semiring A] [algebra R A] [fintype ι]