One-position basis vectors

The colour-model basis vectors at a single position are the unit-padded standard basis vectors: the single-layer computation of colourPowerEquiv 1 on padded pure tensors.

def RS.oneColourE (k ℓ : ℕ) (i : Fin k) : MixedColouring k ℓ 1

The one-position even colouring.

Equations

• RS.oneColourE k ℓ i x✝ = Sum.inl i

def RS.oneColourO (k ℓ : ℕ) (a : Fin (2 * ℓ)) : MixedColouring k ℓ 1

The one-position odd colouring.

Equations

• RS.oneColourO k ℓ a x✝ = Sum.inr a

theorem RS.oneColourE_isEven {k ℓ : ℕ} (i : Fin k) : (oneColourE k ℓ i).IsEven

An even one-position colouring is even.

theorem RS.oneColourO_not_isEven {k ℓ : ℕ} (a : Fin (2 * ℓ)) : ¬(oneColourO k ℓ a).IsEven

And an odd one is not — the grading at a single position.

theorem RS.oneColour_ext {k ℓ : ℕ} {c₁ c₂ : MixedColouring k ℓ 1} (h : c₁ 0 = c₂ 0) : c₁ = c₂

One-position colourings are determined at zero.

theorem RS.evenBasisVec_one {k ℓ : ℕ} (i : Fin k) : evenBasisVec ⟨oneColourE k ℓ i, ⋯⟩ = evenPair 1 (stdE k i)

The one-position even basis vector is the unit-padded standard even basis vector.

theorem RS.oddBasisVec_one {k ℓ : ℕ} (a : Fin (2 * ℓ)) : oddBasisVec ⟨oneColourO k ℓ a, ⋯⟩ = oddUnitPad (stdF ℓ a)

The one-position odd basis vector is the unit-padded standard odd basis vector.