English
Let a and b be multilinear maps on the left and right parts of a family indexed by ι1 ⊕ ι2, mapping to N1 and N2 respectively. Then there exists an induced multilinear map domCoprodDep from the full family N to the tensor product N1 ⊗R N2 given by v ↦ a (i1 ↦ v(inl i1)) ⊗ b (i2 ↦ v(inr i2)). This construction is multilinear in the natural sense.
Русский
Пусть a и b — мультилинейные отображения, действующие на левой и правой частях семейства, индексируемого ι1 ⊕ ι2, с кодами в N1 и N2 соответственно. Тогда существует порожденное мультилинейное отображение domCoprodDep: N → N1 ⊗R N2, заданное формулой v ↦ a (i1 ↦ v(inl i1)) ⊗ b (i2 ↦ v(inr i2)). Это отображение линейно по каждому аргументу.
LaTeX
$$$\text{Let } a:\mathrm{MultilinearMap}\,R\,(\lambda i_1. N(\mathrm{Sum}.inl\,i_1))\,N_1\text{ and } b:\mathrm{MultilinearMap}\,R\,(\lambda i_2. N(\mathrm{Sum}.inr\,i_2))\,N_2. \\text{There exists }\; domCoprodDep:\mathrm{MultilinearMap}\,R\,N\,(N_1\otimes_R N_2) \\text{defined by } domCoprodDep\,v = a(\lambda i_1. v(\mathrm{inl}\,i_1)) \otimes b(\lambda i_2. v(\mathrm{inr}\,i_2)).$$$
Lean4
/-- 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₂`. -/
@[simps apply]
def domCoprodDep (a : MultilinearMap R (fun i₁ ↦ N (.inl i₁)) N₁) (b : MultilinearMap R (fun i₂ ↦ N (.inr i₂)) N₂) :
MultilinearMap R N (N₁ ⊗[R] N₂)
where
toFun v := a (fun i₁ ↦ v (.inl i₁)) ⊗ₜ b (fun i₂ ↦ v (.inr i₂))
map_update_add' := by
rintro _ _ (_ | _) _ _
· letI := Classical.decEq ι₁; simp
· letI := Classical.decEq ι₂; simp
map_update_smul' := by
rintro _ m (i₁ | i₂) p q
· letI := Classical.decEq ι₁; simp
· letI := Classical.decEq ι₂; simp
