The diagonal cap pairing equals the colour pairing

The diagonal cap pairing betaDiag m c on a colouring c : MixedColouring k ℓ (m + m) equals the tensor-power pairing betaColour applied to the two halves of c.

Helper lemmas: peelColour and halves

Relating halves of c to halves of peeled firstHalf

Product splitting

Mixed pair lemmas

The dite-false branch: betaDiag vanishes

Sign identity

The main theorem

theorem RS.betaDiag_eq_betaColour {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + m)) : betaDiag m c = betaColour c.firstHalf c.secondHalf

The diagonal cap pairing equals the colour pairing: betaDiag m c = betaColour (firstHalf c) (secondHalf c).