Alternatization and reindexing of arguments #
Alternatizing a multilinear map commutes with reindexing its arguments along an equivalence
e : ι ≃ ι': (m.domDomCongr e).alternatization = m.alternatization.domDomCongr e. The two
signed permutation sums are matched by conjugating permutations of ι by e, which preserves
their signs. This is how a wedge product defined by alternatizing over Fin (k + l) is compared
with AlternatingMap.domCoprod, which lives on Fin k ⊕ Fin l.
theorem
MultilinearMap.alternatization_domDomCongr
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{ι' : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommGroup N]
[Module R N]
[Fintype ι]
[DecidableEq ι]
[Fintype ι']
[DecidableEq ι']
(e : ι ≃ ι')
(m : (ι → M) →ₘₗ[R] N)
:
Alternatization commutes with reindexing the arguments along an equivalence.