The shuffle sum of a wedge with a 2-form, on a pair family

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Analysis.Normed.Module.Alternating).

The wedge α ∧ β of a 2k-form with a 2-form, evaluated on 2k + 2 vectors, is a signed sum over the shuffle classes Equiv.Perm.ModSumCongr (Fin (2k)) (Fin 2) (wedge_apply). When the vectors come in k + 1 pairs on which β is ±1 within a pair and 0 across pairs (IsPairFamily), only the classes sending the two β-slots into one pair survive, and each such class has a representative made of two disjoint transpositions — of sign +1 — that moves that pair into the β-slots and leaves a family of k pairs behind:

• slotPair, slotMem, slotOf — the bookkeeping of pairs on Fin (2k) ⊕ Fin 2 (inl p is in pair p / 2, member p % 2; the two inr slots form the last pair);
• pairRep j — the two-transposition representative for pair j (the identity for the last pair); pairRep_inl, pairRep_inr, ★ sign_pairRep;
• modSumCongr_mk_eq_of_inr, exists_inr_eq_of_mk_eq — two permutations are in one shuffle class iff they send the inr slots to the same places (Mathlib's mem_sumCongrHom_range_of_perm_mapsTo_inl);
• classTerm, classTerm_mk'', slotPair_eq_of_classTerm_ne_zero, mk_eq_pairRep_of_classTerm_ne_zero, classTerm_pairRep_weighted, classTerm_pairRep;
• ★★ wedge_mul_apply_weightedPairs — the shuffle sum on a weighted pair family (IsWeightedPairFamily: β is ± c j on pair j and 0 across pairs): (α ∧ β) u = ∑ⱼ c j · α (u ∘ pairRep j ∘ inl); ★★ wedge_mul_apply_pairs is the case of all weights 1 (IsPairFamily).

No sign is ever computed beyond sign (swap · ·) = -1 twice: that is the whole point of the two-transposition representative, and it is what makes the count of the top power of the standard symplectic form (Instances/ProjectiveSpaceFubiniStudyVolume.lean) an induction with no combinatorics left in it.

Honest scope

⚠️ Real-valued forms with the codomains paired by multiplication only. ⚠️ Nothing is said about α ∧ β off pair families.

Provenance and references. The top-power plan (M6(b)); Alternating/Wedge.lean (wedge_apply), Alternating/WedgeCLM.lean (liftTensor_summand_mk''); Mathlib/LinearAlgebra/Alternating/DomCoprod.lean; Mathlib/GroupTheory/Perm/Finite.lean; the completed-work ledger.

def ContinuousAlternatingMap.slotPair {k : ℕ} : Fin (2 * k) ⊕ Fin 2 → Fin (k + 1)

The pair a slot of Fin (2k) ⊕ Fin 2 belongs to: inl p is in pair p / 2, the two inr slots form the last pair.

Equations

• ContinuousAlternatingMap.slotPair (Sum.inl p) = ⟨↑p / 2, ⋯⟩
• ContinuousAlternatingMap.slotPair (Sum.inr val) = Fin.last k

def ContinuousAlternatingMap.slotMem {k : ℕ} : Fin (2 * k) ⊕ Fin 2 → Fin 2

Which member of its pair a slot is.

Equations

• ContinuousAlternatingMap.slotMem (Sum.inl p) = ⟨↑p % 2, ⋯⟩
• ContinuousAlternatingMap.slotMem (Sum.inr val) = val

theorem ContinuousAlternatingMap.slotPair_inl {k : ℕ} (p : Fin (2 * k)) : slotPair (Sum.inl p) = ⟨↑p / 2, ⋯⟩

slotPair on an inl slot: pair p / 2.

theorem ContinuousAlternatingMap.slotPair_inr {k : ℕ} (b : Fin 2) : slotPair (Sum.inr b) = Fin.last k

slotPair on an inr slot: the last pair.

theorem ContinuousAlternatingMap.slotMem_inl {k : ℕ} (p : Fin (2 * k)) : slotMem (Sum.inl p) = ⟨↑p % 2, ⋯⟩

slotMem on an inl slot: member p % 2.

theorem ContinuousAlternatingMap.slotMem_inr {k : ℕ} (b : Fin 2) : slotMem (Sum.inr b) = b

slotMem on an inr slot: the slot's own index.

def ContinuousAlternatingMap.slotOf {k : ℕ} (j : Fin (k + 1)) (m : Fin 2) : Fin (2 * k) ⊕ Fin 2

The slot of member m of pair j.

Equations

• ContinuousAlternatingMap.slotOf j m = if h : ↑j < k then Sum.inl ⟨2 * ↑j + ↑m, ⋯⟩ else Sum.inr m

theorem ContinuousAlternatingMap.slotOf_def {k : ℕ} (j : Fin (k + 1)) (m : Fin 2) : slotOf j m = if h : ↑j < k then Sum.inl ⟨2 * ↑j + ↑m, ⋯⟩ else Sum.inr m

slotOf, unfolded: the definitional equation.

theorem ContinuousAlternatingMap.slotPair_slotOf {k : ℕ} (j : Fin (k + 1)) (m : Fin 2) : slotPair (slotOf j m) = j

theorem ContinuousAlternatingMap.slotMem_slotOf {k : ℕ} (j : Fin (k + 1)) (m : Fin 2) : slotMem (slotOf j m) = m

theorem ContinuousAlternatingMap.slotOf_slotPair_slotMem {k : ℕ} (x : Fin (2 * k) ⊕ Fin 2) : slotOf (slotPair x) (slotMem x) = x

theorem ContinuousAlternatingMap.slot_ext {k : ℕ} {x y : Fin (2 * k) ⊕ Fin 2} (h₁ : slotPair x = slotPair y) (h₂ : slotMem x = slotMem y) : x = y

def ContinuousAlternatingMap.pairRep {k : ℕ} (j : Fin (k + 1)) : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)

The two-transposition representative of the shuffle class that sends pair j into the two inr slots (the identity when j is the last pair).

Equations

• ContinuousAlternatingMap.pairRep j = if h : ↑j < k then Equiv.swap (Sum.inl ⟨2 * ↑j, ⋯⟩) (Sum.inr 0) * Equiv.swap (Sum.inl ⟨2 * ↑j + 1, ⋯⟩) (Sum.inr 1) else 1

theorem ContinuousAlternatingMap.pairRep_inr {k : ℕ} (j : Fin (k + 1)) (m : Fin 2) : (pairRep j) (Sum.inr m) = slotOf j m

theorem ContinuousAlternatingMap.pairRep_inl {k : ℕ} (j : Fin (k + 1)) (p : Fin (2 * k)) : (pairRep j) (Sum.inl p) = if slotPair (Sum.inl p) = j then Sum.inr (slotMem (Sum.inl p)) else Sum.inl p

theorem ContinuousAlternatingMap.sign_pairRep {k : ℕ} (j : Fin (k + 1)) : Equiv.Perm.sign (pairRep j) = 1

theorem ContinuousAlternatingMap.modSumCongr_mk_eq_of_inr {k : ℕ} {σ₁ σ₂ : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)} (h : ∀ (m : Fin 2), ∃ (m' : Fin 2), σ₁ (Sum.inr m) = σ₂ (Sum.inr m')) : Quotient.mk'' σ₁ = Quotient.mk'' σ₂

Two permutations whose images of the inr slots agree lie in the same shuffle class.

theorem ContinuousAlternatingMap.exists_inr_eq_of_mk_eq {k : ℕ} {σ ρ : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)} (h : Quotient.mk'' σ = Quotient.mk'' ρ) (m : Fin 2) : ∃ (m' : Fin 2), σ (Sum.inr m) = ρ (Sum.inr m')

In one shuffle class, the images of the inr slots agree.

def ContinuousAlternatingMap.pairSign (a b : Fin 2) : ℝ

The sign of a pairing: 1 for (member 0, member 1), -1 the other way round, 0 otherwise.

Equations

• ContinuousAlternatingMap.pairSign a b = if a = 0 ∧ b = 1 then 1 else if a = 1 ∧ b = 0 then -1 else 0

def ContinuousAlternatingMap.IsPairFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (β : E [⋀^Fin 2]→L[ℝ] ℝ) (u : Fin (2 * k) ⊕ Fin 2 → E) : Prop

A family of 2k + 2 vectors is a pair family for the 2-form β when β pairs the two members of each pair to ±1 and kills everything else.

Equations

• One or more equations did not get rendered due to their size.

def ContinuousAlternatingMap.IsWeightedPairFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (β : E [⋀^Fin 2]→L[ℝ] ℝ) (c : Fin (k + 1) → ℝ) (u : Fin (2 * k) ⊕ Fin 2 → E) : Prop

A family of 2k + 2 vectors is a weighted pair family for the 2-form β, with weights c, when β pairs the two members of pair j to ± c j and kills everything else.

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousAlternatingMap.IsPairFamily.isWeightedPairFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsPairFamily u) : β.IsWeightedPairFamily (fun (x : Fin (k + 1)) => 1) u

A pair family is a weighted pair family with all weights 1.

noncomputable def ContinuousAlternatingMap.classTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ) (β : E [⋀^Fin 2]→L[ℝ] ℝ) (u : Fin (2 * k) ⊕ Fin 2 → E) (q : Equiv.Perm.ModSumCongr (Fin (2 * k)) (Fin 2)) : ℝ

One shuffle-class term of the real-valued wedge.

Equations

• α.classTerm β u q = (ContinuousLinearMap.mul ℝ ℝ).liftTensor ((AlternatingMap.domCoprod.summand α.toAlternatingMap β.toAlternatingMap q) u)

theorem ContinuousAlternatingMap.classTerm_mk'' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ) (β : E [⋀^Fin 2]→L[ℝ] ℝ) (u : Fin (2 * k) ⊕ Fin 2 → E) (σ : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)) : α.classTerm β u (Quotient.mk'' σ) = ↑(Equiv.Perm.sign σ) • ((α fun (i : Fin (2 * k)) => u (σ (Sum.inl i))) * β fun (i : Fin 2) => u (σ (Sum.inr i)))

theorem ContinuousAlternatingMap.wedge_mul_apply_eq_sum_classTerm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ) (β : E [⋀^Fin 2]→L[ℝ] ℝ) (u : Fin (2 * k) ⊕ Fin 2 → E) : (wedge (ContinuousLinearMap.mul ℝ ℝ) α β) u = ∑ q : Equiv.Perm.ModSumCongr (Fin (2 * k)) (Fin 2), α.classTerm β u q

theorem ContinuousAlternatingMap.beta_inr_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} (β : E [⋀^Fin 2]→L[ℝ] ℝ) (u : Fin (2 * k) ⊕ Fin 2 → E) (σ : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)) : (β fun (i : Fin 2) => u (σ (Sum.inr i))) = β ![u (σ (Sum.inr 0)), u (σ (Sum.inr 1))]

theorem ContinuousAlternatingMap.slotPair_eq_of_classTerm_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {c : Fin (k + 1) → ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsWeightedPairFamily c u) (σ : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)) (h : α.classTerm β u (Quotient.mk'' σ) ≠ 0) : slotPair (σ (Sum.inr 0)) = slotPair (σ (Sum.inr 1))

A class term vanishes unless the two inr slots land in one pair.

theorem ContinuousAlternatingMap.mk_eq_pairRep_of_classTerm_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {c : Fin (k + 1) → ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsWeightedPairFamily c u) (σ : Equiv.Perm (Fin (2 * k) ⊕ Fin 2)) (h : α.classTerm β u (Quotient.mk'' σ) ≠ 0) : Quotient.mk'' σ = Quotient.mk'' (pairRep (slotPair (σ (Sum.inr 0))))

A non-vanishing class is the class of the two-transposition representative of its pair.

theorem ContinuousAlternatingMap.classTerm_pairRep_weighted {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {c : Fin (k + 1) → ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsWeightedPairFamily c u) (j : Fin (k + 1)) : α.classTerm β u (Quotient.mk'' (pairRep j)) = c j * α fun (i : Fin (2 * k)) => u ((pairRep j) (Sum.inl i))

The class term of the representative of pair j, on a weighted pair family: the weight of pair j times the 2k-form on the family with pair j moved into the β-slots.

theorem ContinuousAlternatingMap.classTerm_pairRep {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsPairFamily u) (j : Fin (k + 1)) : α.classTerm β u (Quotient.mk'' (pairRep j)) = α fun (i : Fin (2 * k)) => u ((pairRep j) (Sum.inl i))

The class term of the representative of pair j.

theorem ContinuousAlternatingMap.wedge_mul_apply_weightedPairs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {c : Fin (k + 1) → ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsWeightedPairFamily c u) : (wedge (ContinuousLinearMap.mul ℝ ℝ) α β) u = ∑ j : Fin (k + 1), c j * α fun (i : Fin (2 * k)) => u ((pairRep j) (Sum.inl i))

★★ The shuffle sum on a weighted pair family. The wedge of a 2k-form with a 2-form, on a weighted pair family, is the sum over the pairs of that pair's weight times the 2k-form on the family with the pair moved into the 2-form's slots.

theorem ContinuousAlternatingMap.wedge_mul_apply_pairs {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {k : ℕ} {α : E [⋀^Fin (2 * k)]→L[ℝ] ℝ} {β : E [⋀^Fin 2]→L[ℝ] ℝ} {u : Fin (2 * k) ⊕ Fin 2 → E} (hu : β.IsPairFamily u) : (wedge (ContinuousLinearMap.mul ℝ ℝ) α β) u = ∑ j : Fin (k + 1), α fun (i : Fin (2 * k)) => u ((pairRep j) (Sum.inl i))

★★ The shuffle sum on a pair family. The wedge of a 2k-form with a 2-form, on a pair family, is the sum over the pairs of the 2k-form on the family with that pair moved into the 2-form's slots.