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]
noncomputable 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 β

Equations
Instances For
noncomputable 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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : ) :
MultilinearMap R' (fun (x : ιa ιb) => Mᵢ) (TensorProduct R' N₁ N₂)

summand used in AlternatingMap.domCoprod

Equations
Instances For
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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ιb)) :
= 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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : ) {v : ιa ιbMᵢ} {i : ιa ιb} {j : ιa ιb} (hv : v i = v j) (hij : i j) :

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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : ) {v : ιa ιbMᵢ} {i : ιa ιb} {j : ιa ιb} (hv : v i = v j) (hij : i j) :
σ = σ v = 0

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

noncomputable 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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (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 [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 finSumFinEquiv and LinearMap.mul'.

Equations
• a.domCoprod b = { toFun := fun (v : ιa ιbMᵢ) => (∑ σ : , ) v, map_add' := , map_smul' := , map_eq_zero_of_eq' := }
Instances For
@[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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (v : ιa ιbMᵢ) :
(a.domCoprod b) v = (∑ σ : , ) 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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
(a.domCoprod b) = σ : ,
noncomputable 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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] :
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₂.

Equations
Instances For
@[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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
AlternatingMap.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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : MultilinearMap R' (fun (x : ιa) => Mᵢ) N₁) (b : MultilinearMap R' (fun (x : ιb) => Mᵢ) N₂) :
(↑(MultilinearMap.alternatization a)).domCoprod (MultilinearMap.alternatization b) = σa : , σb : , Equiv.Perm.sign σa Equiv.Perm.sign σb .domCoprod

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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : MultilinearMap R' (fun (x : ιa) => Mᵢ) N₁) (b : MultilinearMap R' (fun (x : ιb) => Mᵢ) N₂) :
MultilinearMap.alternatization (a.domCoprod b) = (MultilinearMap.alternatization a).domCoprod (MultilinearMap.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} [] [] [Module R' N₁] [] [Module R' N₂] [] [Module R' Mᵢ] [] [] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) :
MultilinearMap.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.