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.

@[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} [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

    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} [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)) :
      AlternatingMap.domCoprod.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 ι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} [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 ιbMᵢ} {i : ιa ιb} {j : ιa ιb} (hv : v i = v j) (hij : i j) :

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

      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} [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 ιbMᵢ) :
        (a.domCoprod b) v = (Finset.univ.sum fun (σ : Equiv.Perm.ModSumCongr ιa ιb) => AlternatingMap.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) = Finset.univ.sum fun (σ : Equiv.Perm.ModSumCongr ιa ιb) => AlternatingMap.domCoprod.summand a 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} [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₂.

        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} [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₂) :
          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} [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₂) :
          ((MultilinearMap.alternatization a)).domCoprod (MultilinearMap.alternatization b) = Finset.univ.sum fun (σa : Equiv.Perm ιa) => Finset.univ.sum fun (σb : Equiv.Perm ιb) => Equiv.Perm.sign σa Equiv.Perm.sign σb (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.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₂) :
          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} [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₂) :
          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.