S_d-invariance of the pinned pairing (Lemma 5.1(b))

The pinned tensor-power pairing betaColour is invariant under simultaneous permutation of both colourings' positions.

The key combinatorial fact: with matching parities the crossing count koszulCrossings c c' depends only on c.oddSet.card, via the identity 2 * crossings = n * (n - 1) (upper/lower triangle of the off-diagonal). Since permutations preserve oddSet.card, the crossing count — hence the Koszul sign — is invariant.

The formalization does not consume this lemma: it obtains the same S_d-invariance one level upstream, geometrically, from RS.vertexStarClass_perm, where all legs of a vertex star meet the same vertex and a permutation bundle map is absorbed before the fibre functor is applied. The lemma is kept because it is a numbered lemma of the paper.

def RS.MixedColouring.perm {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (π : Equiv.Perm (Fin d)) : MixedColouring k ℓ d

Permuting a colouring by a permutation of positions.

Equations

• c.perm π i = c (π i)

@[simp]

theorem RS.MixedColouring.perm_apply {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (π : Equiv.Perm (Fin d)) (i : Fin d) : c.perm π i = c (π i)

Permuting a colouring's positions.

theorem RS.MixedColouring.oddSet_perm {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (π : Equiv.Perm (Fin d)) : (c.perm π).oddSet = Finset.map (Equiv.symm π).toEmbedding c.oddSet

The odd support of a permuted colouring is the image of the original odd support under π⁻¹.

theorem RS.MixedColouring.oddSet_card_perm {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (π : Equiv.Perm (Fin d)) : (c.perm π).oddSet.card = c.oddSet.card

Permuting does not change how many positions are odd.

theorem RS.prod_colourFormEntry_perm {k ℓ d : ℕ} (c c' : MixedColouring k ℓ d) (π : Equiv.Perm (Fin d)) : ∏ i : Fin d, colourFormEntry k ℓ (c.perm π i) (c'.perm π i) = ∏ i : Fin d, colourFormEntry k ℓ (c i) (c' i)

The product of position form entries is permutation-invariant.

Koszul crossing invariance

theorem RS.betaColour_perm {k ℓ d : ℕ} (π : Equiv.Perm (Fin d)) (c c' : MixedColouring k ℓ d) (hpar : ∀ (i : Fin d), (c i).isRight = (c' i).isRight) : betaColour (c.perm π) (c'.perm π) = betaColour c c'

Lemma 5.1(b): the pinned pairing is S_d-invariant on the support (matching parities).

theorem RS.betaColour_perm' {k ℓ d : ℕ} (π : Equiv.Perm (Fin d)) (c c' : MixedColouring k ℓ d) : betaColour (c.perm π) (c'.perm π) = betaColour c c'

Lemma 5.1(b), unconditional: the pinned pairing is S_d-invariant. Off the support both sides vanish.