Coordinates of model vectors

The coordinate reading of a power vector at a colouring (zero on odd parity), the cast rule, the conjugation transfer, and the basis expansion: the vocabulary in which the final computation evaluates.

noncomputable def RS.coordOf {k ℓ n : ℕ} (v : (superPow (stdSuperPair k ℓ) n).even) (c : MixedColouring k ℓ n) : ℂ

The coordinate of a model vector at a colouring.

Equations

• RS.coordOf v c = if hc : c.IsEven then (RS.colourPowerEquiv k ℓ n).evenEquiv v ⟨c, hc⟩ else 0

theorem RS.coordOf_odd {k ℓ n : ℕ} (v : (superPow (stdSuperPair k ℓ) n).even) (c : MixedColouring k ℓ n) (hc : ¬c.IsEven) : coordOf v c = 0

Coordinates vanish on odd parity.

theorem RS.coordOf_cast {k ℓ n₁ n₂ : ℕ} (h : n₁ = n₂) (v : (superPow (stdSuperPair k ℓ) n₁).even) (c : MixedColouring k ℓ n₂) : coordOf ((CategoryTheory.eqToHom ⋯).evenMap v) c = coordOf v (c ∘ ⇑(finCongr h))

The cast rule: coordinates of a recast vector read the recast colouring.

theorem RS.toColour_apply {k ℓ n : ℕ} (g : superPow (stdSuperPair k ℓ) n ⟶ superPow (stdSuperPair k ℓ) n) (v : (superPow (stdSuperPair k ℓ) n).even) : (toColour n g).evenMap ((colourPowerEquiv k ℓ n).evenEquiv v) = (colourPowerEquiv k ℓ n).evenEquiv (g.evenMap v)

The conjugation transfer: colour-model conjugates act on coordinate functions.

theorem RS.coord_expansion {k ℓ n : ℕ} (v : (superPow (stdSuperPair k ℓ) n).even) : v = ∑ c : { c : MixedColouring k ℓ n // c.IsEven }, (colourPowerEquiv k ℓ n).evenEquiv v c • (colourPowerEquiv k ℓ n).evenEquiv.symm (Pi.single c 1)

The basis expansion of a model vector by its coordinates.