The Eulerian reindex

The master summand, the flag pattern of a colouring, and the fibrewise partition of the master colour sum over flag patterns.

noncomputable def RS.masterSummand {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) : ℂ

The master summand of a colouring.

Equations

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

theorem RS.parameter_masterSummand {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (hform : SuperVect.Hom.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := 1 } { arity := 1 }) (CategoryTheory.CategoryStruct.comp (P.ω.map (ε_ { arity := 1 } { arity := 1 })) (CategoryTheory.Functor.OplaxMonoidal.η P.ω))) (SuperVect.tensorHom e e) = stdForm k ℓ) : f.val W = circleVal f ^ W.circles * ∑ c : { c : MixedColouring k ℓ (edgeCount W + edgeCount W) // c.IsEven }, masterSummand f P e' W ↑c

The master colour sum, in summand form.

noncomputable def RS.colourFlags {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) : Finset W.Flag

The flag pattern of a colouring: the flags at odd slots.

Equations

• RS.colourFlags W c = Finset.image (fun (s : Fin (RS.edgeCount W + RS.edgeCount W)) => (RS.starFlagEnum W).symm s) c.oddSet

theorem RS.masterSum_partition {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) : ∑ c : { c : MixedColouring k ℓ (edgeCount W + edgeCount W) // c.IsEven }, masterSummand f P e' W ↑c = ∑ s : Finset W.Flag, ∑ c : { c : MixedColouring k ℓ (edgeCount W + edgeCount W) // c.IsEven } with colourFlags W ↑c = s, masterSummand f P e' W ↑c

The pattern partition of the master sum.

def RS.PairPure {k ℓ m : ℕ} (c : MixedColouring k ℓ (m + m)) : Prop

Parity purity: cap-paired slots share parity.

Equations

• RS.PairPure c = ∀ (i : Fin m), (c (Fin.castAdd m i)).isRight = (c (Fin.natAdd m i)).isRight

theorem RS.colourFlags_pairing_mem {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hpure : PairPure c) (g : W.Flag) : g ∈ colourFlags W c → W.pairing g ∈ colourFlags W c

Pure patterns are pairing-closed.