# Documentation

Mathlib.LinearAlgebra.Alternating.DomCoprod

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

@[inline, reducible]
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
theorem Equiv.Perm.ModSumCongr.swap_smul_involutive {α : Type u_7} {β : Type u_8} [DecidableEq (α β)] (i : α β) (j : α β) :
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
• One or more equations did not get rendered due to their size.
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 σ
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 [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'.

Equations
• One or more equations did not get rendered due to their size.
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ᵢ) :
() v = (Finset.sum Finset.univ fun (σ : ) => ) 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₂) :
() = Finset.sum Finset.univ fun (σ : ) =>
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
• One or more equations did not get rendered due to their size.
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) =
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.domCoprod (MultilinearMap.alternatization a) (MultilinearMap.alternatization b) = Finset.sum Finset.univ fun (σa : ) => Finset.sum Finset.univ fun (σb : ) => Equiv.Perm.sign σa Equiv.Perm.sign σ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} [] [] [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 () = AlternatingMap.domCoprod (MultilinearMap.alternatization a) (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 () = ()

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