The tensor-power pairing in colouring coordinates

The accompanying paper's pinned pairing (§5.1):

β_d(v₁⊗⋯⊗v_d, w₁⊗⋯⊗w_d)
  = (−1)^{Σ_{i<j} |v_j||w_i|} ∏ᵢ b(vᵢ, wᵢ).

On colouring basis vectors this is a sign times a product of single-position form entries: 1 on matching even colours, the symplectic entry on odd colours, 0 on mixed positions.

def RS.colourFormEntry (k ℓ : ℕ) : Fin k ⊕ Fin (2 * ℓ) → Fin k ⊕ Fin (2 * ℓ) → ℂ

The single-position form entry: Kronecker on even colours, the symplectic matrix on odd colours, zero on mixed.

Equations

• RS.colourFormEntry k ℓ (Sum.inl i) (Sum.inl j) = if i = j then 1 else 0
• RS.colourFormEntry k ℓ (Sum.inr a) (Sum.inr b) = if ↑a + ℓ = ↑b then 1 else if ↑b + ℓ = ↑a then -1 else 0
• RS.colourFormEntry k ℓ (Sum.inl val) (Sum.inr val_1) = 0
• RS.colourFormEntry k ℓ (Sum.inr val) (Sum.inl val_1) = 0

def RS.koszulCrossings {k ℓ d : ℕ} (c c' : MixedColouring k ℓ d) : ℕ

The Koszul crossing count of a colouring pair: pairs of positions i < j with the second argument odd at i and the first odd at j.

Equations

• RS.koszulCrossings c c' = {p : Fin d × Fin d | p.1 < p.2 ∧ (c p.2).isRight = true ∧ (c' p.1).isRight = true}.card

noncomputable def RS.betaColour {k ℓ d : ℕ} (c c' : MixedColouring k ℓ d) : ℂ

The pinned tensor-power pairing on colouring basis vectors.

Equations

• RS.betaColour c c' = (-1) ^ RS.koszulCrossings c c' * ∏ i : Fin d, RS.colourFormEntry k ℓ (c i) (c' i)

theorem RS.betaColour_eq_zero_of_mixed {k ℓ d : ℕ} {c c' : MixedColouring k ℓ d} (i : Fin d) (h : (c i).isRight ≠ (c' i).isRight) : betaColour c c' = 0

Mixed positions kill the pairing.