Adjacent braidings on monoidal powers

The braiding of two adjacent factors of a monoidal power: the top case conjugates the braiding through one associator, and lower positions whisker the smaller power's braiding. On the colouring model the intended action is the Koszul-signed position swap, defined here; the identification is the coordinate workhorse of the extraction.

noncomputable def RS.topBraid (V : SuperVect) (m : ℕ) : superPow V (m + 2) ⟶ superPow V (m + 2)

The top adjacent braiding on a monoidal power: braid the last two factors through the associator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RS.powBraid (V : SuperVect) (n i : ℕ) : i + 2 ≤ n → (superPow V n ⟶ superPow V n)

The adjacent braiding at position i: swap the factors at zero-based positions i and i + 1.

Equations

• RS.powBraid V 0 x✝¹ x✝ = absurd x✝ ⋯
• RS.powBraid V 1 x✝¹ x✝ = absurd x✝ ⋯
• RS.powBraid V n.succ.succ x✝¹ x✝ = if hi : x✝¹ = n then RS.topBraid V n else CategoryTheory.MonoidalCategoryStruct.whiskerRight (RS.powBraid V (n + 1) x✝¹ ⋯) V

theorem RS.MixedColouring.oddSet_comp_card {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (σ : Equiv.Perm (Fin d)) : (oddSet (c ∘ ⇑σ)).card = c.oddSet.card

Reindexing a colouring along a permutation preserves the odd count.

theorem RS.MixedColouring.IsEven.comp {k ℓ d : ℕ} {c : MixedColouring k ℓ d} (hc : c.IsEven) (σ : Equiv.Perm (Fin d)) : IsEven (c ∘ ⇑σ)

Reindexing preserves evenness.

theorem RS.MixedColouring.not_isEven_comp {k ℓ d : ℕ} {c : MixedColouring k ℓ d} (hc : ¬c.IsEven) (σ : Equiv.Perm (Fin d)) : ¬IsEven (c ∘ ⇑σ)

Reindexing preserves oddness.

def RS.adjSign {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (a b : Fin d) : ℂ

The Koszul sign of swapping two positions of a colouring: −1 when both are odd.

Equations

• RS.adjSign c a b = if (c a).isRight = true ∧ (c b).isRight = true then -1 else 1

noncomputable def RS.colourSwap (k ℓ n i : ℕ) : i + 2 ≤ n → (colourPower k ℓ n ⟶ colourPower k ℓ n)

The Koszul-signed adjacent position swap on the colouring model.

Equations

• One or more equations did not get rendered due to their size.