Evaluating a colour tensor

The function tensor on a pure tensor is the pointwise product, and the colouring of a product index splits into its two factors — the computation rules the standard super model's coordinates use.

theorem RS.funTensorFun_tmul {ι κ : Type} [Fintype ι] [Fintype κ] (f : ι → ℂ) (g : κ → ℂ) (p : ι × κ) : (funTensorFun ι κ) (f ⊗ₜ[ℂ] g) p = f p.1 * g p.2

The function tensor on a pure tensor is the pointwise product.

theorem RS.colouringSplit_symm_castSucc {k ℓ d : ℕ} (c₀ : MixedColouring k ℓ d) (x : Fin k ⊕ Fin (2 * ℓ)) (i : Fin d) : (colouringSplit k ℓ d).symm (c₀, x) i.castSucc = c₀ i

Rejoining, at an early slot.

theorem RS.colouringSplit_symm_last {k ℓ d : ℕ} (c₀ : MixedColouring k ℓ d) (x : Fin k ⊕ Fin (2 * ℓ)) : (colouringSplit k ℓ d).symm (c₀, x) (Fin.last d) = x

At the last slot.

theorem RS.evenSplitEquiv_symm_inl {k ℓ d : ℕ} (c₀ : { c : MixedColouring k ℓ d // c.IsEven }) (a : Fin k) : ↑((evenSplitEquiv k ℓ d).symm (Sum.inl (c₀, a))) = (colouringSplit k ℓ d).symm (↑c₀, Sum.inl a)

The inverse even split on an even-tail/even-colour pair.

theorem RS.evenSplitEquiv_symm_inr {k ℓ d : ℕ} (c₀ : { c : MixedColouring k ℓ d // ¬c.IsEven }) (b : Fin (2 * ℓ)) : ↑((evenSplitEquiv k ℓ d).symm (Sum.inr (c₀, b))) = (colouringSplit k ℓ d).symm (↑c₀, Sum.inr b)

The inverse even split on an odd-tail/odd-colour pair.

theorem RS.oddSplitEquiv_symm_inl {k ℓ d : ℕ} (c₀ : { c : MixedColouring k ℓ d // ¬c.IsEven }) (a : Fin k) : ↑((oddSplitEquiv k ℓ d).symm (Sum.inl (c₀, a))) = (colouringSplit k ℓ d).symm (↑c₀, Sum.inl a)

The inverse odd split on an odd-tail/even-colour pair.

theorem RS.oddSplitEquiv_symm_inr {k ℓ d : ℕ} (c₀ : { c : MixedColouring k ℓ d // c.IsEven }) (b : Fin (2 * ℓ)) : ↑((oddSplitEquiv k ℓ d).symm (Sum.inr (c₀, b))) = (colouringSplit k ℓ d).symm (↑c₀, Sum.inr b)

The inverse odd split on an even-tail/odd-colour pair.