Conjugation into the colouring model

Endomorphisms of the monoidal power conjugate through colourPowerEquiv into the colouring model; extending along one step is conjugation of the whisker through colourPowerStep. These are the carriers of the braiding-coordinate computation.

noncomputable def RS.toColour {k ℓ : ℕ} (n : ℕ) (g : superPow (stdSuperPair k ℓ) n ⟶ superPow (stdSuperPair k ℓ) n) : colourPower k ℓ n ⟶ colourPower k ℓ n

Conjugating a power endomorphism into the colouring model.

Equations

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

noncomputable def RS.colourExtend {k ℓ : ℕ} (n : ℕ) (T : colourPower k ℓ n ⟶ colourPower k ℓ n) : colourPower k ℓ (n + 1) ⟶ colourPower k ℓ (n + 1)

Extending a colour-model endomorphism by one position: conjugation of the whisker through the step equivalence.

Equations

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

theorem RS.toColour_comp {k ℓ : ℕ} (n : ℕ) (g₁ g₂ : superPow (stdSuperPair k ℓ) n ⟶ superPow (stdSuperPair k ℓ) n) : toColour n (CategoryTheory.CategoryStruct.comp g₁ g₂) = CategoryTheory.CategoryStruct.comp (toColour n g₁) (toColour n g₂)

Conjugation preserves composition.

theorem RS.toColour_id {k ℓ : ℕ} (n : ℕ) : toColour n (CategoryTheory.CategoryStruct.id (superPow (stdSuperPair k ℓ) n)) = CategoryTheory.CategoryStruct.id (colourPower k ℓ n)

Conjugation preserves the identity.