Star coordinate symmetry

The star vector is permutation-invariant, the inverse transport intertwines permutations, and hence the star coordinate at a permuted colouring is the odd-inversion sign times the original.

theorem RS.starVec_perm {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (d : ℕ) (σ : Equiv.Perm (Fin d)) : (P.ω.map (bundleMapClass f σ)).evenMap (starVec f P d) = starVec f P d

The star vector is permutation-invariant.

theorem RS.stdFromOmega_perm {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (he'e : CategoryTheory.CategoryStruct.comp e e' = CategoryTheory.CategoryStruct.id (stdSuperPair k ℓ)) (d : ℕ) (σ : Equiv.Perm (Fin d)) : CategoryTheory.CategoryStruct.comp (stdFromOmega f P e' d) (modelPermMap σ) = CategoryTheory.CategoryStruct.comp (P.ω.map (bundleMapClass f σ)) (stdFromOmega f P e' d)

The inverse transport intertwines permutations.

theorem RS.starCoord_eq_coordOf {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (d : ℕ) (c : MixedColouring k ℓ d) : starCoord f P e' d c = coordOf ((stdFromOmega f P e' d).evenMap (starVec f P d)) c

The star coordinate is a model coordinate.

theorem RS.starCoord_perm {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (he'e : CategoryTheory.CategoryStruct.comp e e' = CategoryTheory.CategoryStruct.id (stdSuperPair k ℓ)) (d : ℕ) (σ : Equiv.Perm (Fin d)) (c : MixedColouring k ℓ d) : starCoord f P e' d (c ∘ ⇑σ) = (-1) ^ oddInversions σ c * starCoord f P e' d c

The star coordinate symmetry: permuting the colouring multiplies by the odd-inversion sign.