Exterior product of alternating maps

In this file we define AlternatingMap.domCoprod to be the exterior product of two alternating maps, taking values in the tensor product of the codomains of the original maps.

@[reducible, inline]

abbrev Equiv.Perm.ModSumCongr (α : Type u_7) (β : Type u_8) : Type (max u_7 u_8)

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

def AlternatingMap.domCoprod.summand {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) : MultilinearMap R' (fun (x : ιa ⊕ ιb) => Mᵢ) (TensorProduct R' N₁ N₂)

summand used in AlternatingMap.domCoprod

theorem AlternatingMap.domCoprod.summand_mk'' {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ⊕ ιb)) : summand a b (Quotient.mk'' σ) = Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ ((↑a).domCoprod ↑b)

theorem AlternatingMap.domCoprod.summand_add_swap_smul_eq_zero {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) : (summand a b σ) v + (summand a b (Equiv.swap i j • σ)) v = 0

Swapping elements in σ with equal values in v results in an addition that cancels

theorem AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb} (hv : v i = v j) (hij : i ≠ j) : Equiv.swap i j • σ = σ → (summand a b σ) v = 0

Swapping elements in σ with equal values in v result in zero if the swap has no effect on the quotient.

def AlternatingMap.domCoprod {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] TensorProduct R' N₁ N₂

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'.

@[simp]

theorem AlternatingMap.domCoprod_apply {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (v : ιa ⊕ ιb → Mᵢ) : (a.domCoprod b) v = (∑ σ : Equiv.Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ) v

theorem AlternatingMap.domCoprod_coe {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : ↑(a.domCoprod b) = ∑ σ : Equiv.Perm.ModSumCongr ιa ιb, domCoprod.summand a b σ

def AlternatingMap.domCoprod' {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] : TensorProduct R' (Mᵢ [⋀^ιa]→ₗ[R'] N₁) (Mᵢ [⋀^ιb]→ₗ[R'] N₂) →ₗ[R'] Mᵢ [⋀^ιa ⊕ ιb]→ₗ[R'] TensorProduct R' N₁ N₂

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

@[simp]

theorem AlternatingMap.domCoprod'_apply {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : domCoprod' (a ⊗ₜ[R'] b) = a.domCoprod b

theorem MultilinearMap.domCoprod_alternization_coe {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : MultilinearMap R' (fun (x : ιa) => Mᵢ) N₁) (b : MultilinearMap R' (fun (x : ιb) => Mᵢ) N₂) : (↑(alternatization a)).domCoprod ↑(alternatization b) = ∑ σa : Equiv.Perm ιa, ∑ σb : Equiv.Perm ιb, Equiv.Perm.sign σa • Equiv.Perm.sign σb • (domDomCongr σa a).domCoprod (domDomCongr σb b)

A helper lemma for MultilinearMap.domCoprod_alternization.

theorem MultilinearMap.domCoprod_alternization {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : MultilinearMap R' (fun (x : ιa) => Mᵢ) N₁) (b : MultilinearMap R' (fun (x : ιb) => Mᵢ) N₂) : alternatization (a.domCoprod b) = (alternatization a).domCoprod (alternatization b)

Computing the MultilinearMap.alternatization of the MultilinearMap.domCoprod is the same as computing the AlternatingMap.domCoprod of the MultilinearMap.alternatizations.

theorem MultilinearMap.domCoprod_alternization_eq {ιa : Type u_1} {ιb : Type u_2} [Fintype ιa] [Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [CommSemiring R'] [AddCommGroup N₁] [Module R' N₁] [AddCommGroup N₂] [Module R' N₂] [AddCommMonoid Mᵢ] [Module R' Mᵢ] [DecidableEq ιa] [DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) : alternatization ((↑a).domCoprod ↑b) = ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b

Taking the MultilinearMap.alternatization of the MultilinearMap.domCoprod of two AlternatingMaps gives a scaled version of the AlternatingMap.coprod of those maps.