Sector intertwining for the standard model

The even and odd sector trace functionals for the standard model stdSuperPair k ℓ, and their character formulas: the intertwining that carries the abstract superPermAction kernel containment of KoszulAction.lean to concrete characters.

Main definitions

• evenSectorTr k ℓ n — the partial trace on the all-even colour block of (superPow (stdSuperPair k ℓ) n).even
• oddSectorTr k ℓ n — the partial trace on the all-odd colour block (in the even component when n is even)

Main results

• evenSectorTr_perm — the character formula: evenSectorTr k ℓ n (modelPermMap σ).evenMap = cycleProd (const k) σ
• oddSectorTr_perm — the signed character formula: oddSectorTr k ℓ n (modelPermMap σ).evenMap = sign(σ) · cycleProd (const (2ℓ)) σ (for even n)

The transport to an abstract package

The transport from stdSuperPair k ℓ to strandImage f P (for an abstract Deligne package with strandImage ≅ stdSuperPair k ℓ) requires conjugating evenSectorTr / oddSectorTr by the induced LinearEquiv on (superPow V n).even. Concretely: given a super iso pair (e, e') with e' ∘ e = id and e ∘ e' = id, the functoriality of superPow (tensorHom iterated) gives superPowIso : superPow (stdSuperPair k ℓ) n ≅ superPow (strandImage f P) n and evenSectorTr k ℓ n ∘ (conjugate by superPowIso.even) = evenSectorTr' f P n intertwines modelPermMap with evenPermRep. The kernel containment superPermAction f P n x = 0 → evenSectorTr' (evenPermRep f P n x) = 0 follows from superPermAction_zero_imp_evenPermRep_zero in KoszulAction.lean.

All-even colourings

def RS.allEvenEmb (k ℓ n : ℕ) (f : Fin n → Fin k) : MixedColouring k ℓ n

The all-even colouring: every position gets an even colour.

Equations

• RS.allEvenEmb k ℓ n f i = Sum.inl (f i)

theorem RS.allEvenEmb_isEven (k ℓ n : ℕ) (f : Fin n → Fin k) : (allEvenEmb k ℓ n f).IsEven

All-even colourings have empty odd support, hence even parity.

theorem RS.allEvenEmb_comp (k ℓ n : ℕ) (f : Fin n → Fin k) (σ : Equiv.Perm (Fin n)) : allEvenEmb k ℓ n f ∘ ⇑σ = allEvenEmb k ℓ n (f ∘ ⇑σ)

Composing an all-even colouring with a permutation.

theorem RS.allEvenEmb_injective (k ℓ n : ℕ) : Function.Injective (allEvenEmb k ℓ n)

The all-even embedding is injective.

theorem RS.oddInversions_allEvenEmb (k ℓ n : ℕ) (σ : Equiv.Perm (Fin n)) (f : Fin n → Fin k) : oddInversions σ (allEvenEmb k ℓ n f) = 0

oddInversions vanishes on all-even colourings: no position is odd-coloured, so the inversion filter is empty.

Colour-model basis vectors

noncomputable def RS.evenBasis (k ℓ n : ℕ) (c : { c : MixedColouring k ℓ n // c.IsEven }) : (superPow (stdSuperPair k ℓ) n).even

A basis vector of the even colour model at an even colouring.

Equations

• RS.evenBasis k ℓ n c = (RS.colourPowerEquiv k ℓ n).evenEquiv.symm (have this := Pi.single c 1; this)

The even sector trace

noncomputable def RS.evenSectorTr (k ℓ n : ℕ) : Module.End ℂ (superPow (stdSuperPair k ℓ) n).even →ₗ[ℂ] ℂ

The even sector trace functional: the partial trace of an endomorphism of (superPow (stdSuperPair k ℓ) n).even restricted to the all-even colour block.

Equations

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

Fixed-point count

theorem RS.fixedCount_eq_cycleProd (n m : ℕ) (σ : Equiv.Perm (Fin n)) : (∑ f : Fin n → Fin m, if f ∘ ⇑σ = f then 1 else 0) = cycleProd (fun (x : ℕ) => ↑m) σ

The sum over if f ∘ σ = f then 1 else 0 equals cycleProd (const m).

The even character formula

theorem RS.evenSectorTr_perm (k ℓ n : ℕ) (σ : Equiv.Perm (Fin n)) : (evenSectorTr k ℓ n) (modelPermMap σ).evenMap = cycleProd (fun (x : ℕ) => ↑k) σ

Even character formula: the even sector trace of modelPermMap σ equals cycleProd (fun _ => k) σ.

All-odd colourings (even-n case)

def RS.allOddEmb (k ℓ n : ℕ) (g : Fin n → Fin (2 * ℓ)) : MixedColouring k ℓ n

The all-odd colouring: every position gets an odd colour.

Equations

• RS.allOddEmb k ℓ n g i = Sum.inr (g i)

theorem RS.allOddEmb_oddSet_card (k ℓ n : ℕ) (g : Fin n → Fin (2 * ℓ)) : (allOddEmb k ℓ n g).oddSet.card = n

An all-odd colouring has oddSet = univ.

theorem RS.allOddEmb_isEven_iff (k ℓ n : ℕ) (g : Fin n → Fin (2 * ℓ)) : (allOddEmb k ℓ n g).IsEven ↔ Even n

All-odd colourings are even-parity iff n is even.

theorem RS.allOddEmb_isEven (k ℓ n : ℕ) (hn : Even n) (g : Fin n → Fin (2 * ℓ)) : (allOddEmb k ℓ n g).IsEven

For even n, all-odd colourings are even-parity.

theorem RS.allOddEmb_comp (k ℓ n : ℕ) (g : Fin n → Fin (2 * ℓ)) (σ : Equiv.Perm (Fin n)) : allOddEmb k ℓ n g ∘ ⇑σ = allOddEmb k ℓ n (g ∘ ⇑σ)

Composing an all-odd colouring with a permutation.

theorem RS.allOddEmb_injective (k ℓ n : ℕ) : Function.Injective (allOddEmb k ℓ n)

The all-odd embedding is injective.

Sign equals (-1)^inversions

theorem RS.neg_one_pow_oddInversions_allOdd {ℓ k n : ℕ} (σ : Equiv.Perm (Fin (n + 1))) (g : Fin (n + 1) → Fin (2 * ℓ)) : (-1) ^ oddInversions σ (allOddEmb k ℓ (n + 1) g) = ↑↑(Equiv.Perm.sign σ)

(-1)^oddInversions σ c = sign σ when c is all-odd, at positive arity.

theorem RS.neg_one_pow_oddInversions_allOdd' {ℓ k : ℕ} (n : ℕ) (σ : Equiv.Perm (Fin n)) (g : Fin n → Fin (2 * ℓ)) : (-1) ^ oddInversions σ (allOddEmb k ℓ n g) = ↑↑(Equiv.Perm.sign σ)

The sign-inversion identity at all arities.

The odd sector trace (even-n case)

noncomputable def RS.oddSectorTr (k ℓ n : ℕ) (hn : Even n) : Module.End ℂ (superPow (stdSuperPair k ℓ) n).even →ₗ[ℂ] ℂ

The odd sector trace functional (for even n): the partial trace on the all-odd colour block of (superPow (stdSuperPair k ℓ) n).even.

Equations

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

theorem RS.oddSectorTr_perm (k ℓ n : ℕ) (hn : Even n) (σ : Equiv.Perm (Fin n)) : (oddSectorTr k ℓ n hn) (modelPermMap σ).evenMap = ↑↑(Equiv.Perm.sign σ) * cycleProd (fun (x : ℕ) => ↑(2 * ℓ)) σ

Odd character formula (even-n case): the odd sector trace of modelPermMap σ equals sign(σ) · cycleProd (const (2ℓ)) σ.