The β-diagonal's colour data #
The colour-form entries at a partner slot, the colouring of a sum
index on either side, and the β-diagonal these produce.
The colour form entry at an odd colour and its partner equals minus the partner sign.
theorem
RS.colouringOf_castAdd
{k ℓ : ℕ}
(W : ClosedFragment)
(F : EdgeSubset W)
(ψ : F.EvenColouring k)
(φ : F.OddColouring ℓ)
(i : Fin (edgeCount W))
:
colouringOf W F ψ φ (Fin.castAdd (edgeCount W) i) = if h : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags then
Sum.inr (↑φ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩)
else Sum.inl (↑ψ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩)
The data colouring at a castAdd slot gives the representative colour (even or odd).
theorem
RS.colouringOf_natAdd
{k ℓ : ℕ}
(W : ClosedFragment)
(F : EdgeSubset W)
(ψ : F.EvenColouring k)
(φ : F.OddColouring ℓ)
(i : Fin (edgeCount W))
:
colouringOf W F ψ φ (Fin.natAdd (edgeCount W) i) = if h : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags then
Sum.inr (oddPartner ℓ (↑φ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩))
else Sum.inl (↑ψ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩)
The data colouring at a natAdd slot gives the partner colour (even repeat or odd partner).
theorem
RS.betaDiag_colouringOf
{k ℓ : ℕ}
(W : ClosedFragment)
(F : EdgeSubset W)
(ψ : F.EvenColouring k)
(φ : F.OddColouring ℓ)
:
betaDiag (edgeCount W) (colouringOf W F ψ φ) = (-1) ^ {p : Fin (edgeCount W) × Fin (edgeCount W) | p.1 < p.2 ∧ p.1 ∈ edgeIndexSet W F ∧ p.2 ∈ edgeIndexSet W F}.card * ∏ i : Fin (edgeCount W),
if h : (starFlagEnum W).symm (Fin.castAdd (edgeCount W) i) ∈ F.flags then
-↑(oddPartnerSign ℓ (↑φ ⟨(starFlagEnum W).symm (Fin.castAdd (edgeCount W) i), h⟩))
else 1
The diagonal cap pairing on the data colouring: the Koszul sign times the product of per-position form entries, each evaluated on the diagonal partner.