English
The domCoprod map equals the sum over all summands.
Русский
Карта domCoprod равна сумме по всем summand.
LaTeX
$$$$a\,\text{domCoprod } b = \sum_{σ} \text{domCoprod.summand}(a,b,σ).$$$$
Lean4
/-- Like `MultilinearMap.domCoprod`, but ensures the result is also alternating.
Note that this is usually defined (for instance, as used in Proposition 22.24 in [Gallier2011Notes])
over integer indices `ιa = Fin n` and `ιb = Fin m`, as
$$
(f \wedge g)(u_1, \ldots, u_{m+n}) =
\sum_{\operatorname{shuffle}(m, n)} \operatorname{sign}(\sigma)
f(u_{\sigma(1)}, \ldots, u_{\sigma(m)}) g(u_{\sigma(m+1)}, \ldots, u_{\sigma(m+n)}),
$$
where $\operatorname{shuffle}(m, n)$ consists of all permutations of $[1, m+n]$ such that
$\sigma(1) < \cdots < \sigma(m)$ and $\sigma(m+1) < \cdots < \sigma(m+n)$.
Here, we generalize this by replacing:
* the product in the sum with a tensor product
* the filtering of $[1, m+n]$ to shuffles with an isomorphic quotient
* the additions in the subscripts of $\sigma$ with an index of type `Sum`
The specialized version can be obtained by combining this definition with `finSumFinEquiv` and
`LinearMap.mul'`.
-/
@[simps]
def domCoprod (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] (N₁ ⊗[R'] N₂) :=
{
∑ σ : Perm.ModSumCongr ιa ιb,
domCoprod.summand a b
σ with
toFun := fun v => (⇑(∑ σ : Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ)) v
map_eq_zero_of_eq' := fun v i j hv hij => by
rw [MultilinearMap.sum_apply]
exact
Finset.sum_involution (fun σ _ => Equiv.swap i j • σ)
(fun σ _ => domCoprod.summand_add_swap_smul_eq_zero a b σ hv hij)
(fun σ _ => mt <| domCoprod.summand_eq_zero_of_smul_invariant a b σ hv hij) (fun σ _ => Finset.mem_univ _)
fun σ _ => Equiv.swap_smul_involutive i j σ }
