The multilinear map associated to an alternating map

The space of multilinear maps over an algebra over R is a module over R, for the pointwise addition and scalar multiplication.

The evaluation map from ι → N to N at a given i is alternating when ι is subsingleton.

Composing a alternating map with a linear map on the left gives again an alternating map.

Composing a alternating map with the same linear map on each argument gives again an alternating map.

Construct a linear equivalence between maps from a linear equivalence between domains.

Produce an alternating_map out of a multilinear_map, by summing over all argument permutations.

Elements which are considered equivalent if they differ only by swaps within α or β

summand used in alternating_map.dom_coprod

Like multilinear_map.dom_coprod, but ensures the result is also alternating.

Note that this is usually defined (for instance, as used in Proposition 22.24 in [GQ11]) 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 fin_sum_fin_equiv and algebra.lmul'.

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