Basis vectors split over the merge

Coordinate basis vectors of a merged power decompose as merges of half-basis pairs: even halves through the even pair, odd halves through the odd pair. The coordinate product rules of both parities identify the coordinates; injectivity does the rest.

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

The even coordinate basis vector at a colouring.

Equations

• RS.evenBasisVec c = (RS.colourPowerEquiv k ℓ n).evenEquiv.symm (Pi.single c 1)

noncomputable def RS.oddBasisVec {k ℓ n : ℕ} (c : { c : MixedColouring k ℓ n // ¬c.IsEven }) : (superPow (stdSuperPair k ℓ) n).odd

The odd coordinate basis vector at a colouring.

Equations

• RS.oddBasisVec c = (RS.colourPowerEquiv k ℓ n).oddEquiv.symm (Pi.single c 1)

theorem RS.MixedColouring.ext_halves {k ℓ a b : ℕ} {c₁ c₂ : MixedColouring k ℓ (a + b)} (h1 : c₁.firstHalf = c₂.firstHalf) (h2 : c₁.secondHalf = c₂.secondHalf) : c₁ = c₂

Colourings are determined by their halves.

theorem RS.evenBasisVec_split {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) (hc : c.IsEven) : evenBasisVec ⟨c, hc⟩ = if h : c.firstHalf.IsEven then (powMerge (stdSuperPair k ℓ) a b).evenMap (evenPair (evenBasisVec ⟨c.firstHalf, h⟩) (evenBasisVec ⟨c.secondHalf, ⋯⟩)) else (powMerge (stdSuperPair k ℓ) a b).evenMap (0, oddBasisVec ⟨c.firstHalf, h⟩ ⊗ₜ[ℂ] oddBasisVec ⟨c.secondHalf, ⋯⟩)

Basis vectors split over the merge.