The fibre bijection

Closed-pattern fibres are pure; their sums reindex over the colouring data through the diagonal parametrization.

theorem RS.pairPure_of_pattern_closed {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (s : Finset W.Flag) (hfibre : colourFlags W c = s) (hclosed : ∀ g ∈ s, W.pairing g ∈ s) : PairPure c

Closed patterns force purity.

theorem RS.fibreSum_eq_dataSum {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (F : EdgeSubset W) : ∑ c : { c : MixedColouring k ℓ (edgeCount W + edgeCount W) // c.IsEven } with colourFlags W ↑c = F.flags, masterSummand f P e' W ↑c = ∑ ψ : F.EvenColouring k, ∑ φ : F.OddColouring ℓ, masterSummand f P e' W (colouringOf W F ψ φ)

The fibre sum reindexes over the colouring data.

noncomputable def RS.edgeIndexSet (W : ClosedFragment) (F : EdgeSubset W) : Finset (Fin (edgeCount W))

The edge set of an edge subset: representative slots whose flags participate.

Equations

• RS.edgeIndexSet W F = {i : Fin (RS.edgeCount W) | (RS.starFlagEnum W).symm (Fin.castAdd (RS.edgeCount W) i) ∈ F.flags}

theorem RS.koszulCrossings_colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : koszulCrossings (colouringOf W F ψ φ).firstHalf (colouringOf W F ψ φ).secondHalf = {p : Fin (edgeCount W) × Fin (edgeCount W) | p.1 < p.2 ∧ p.1 ∈ edgeIndexSet W F ∧ p.2 ∈ edgeIndexSet W F}.card

The crossings of a data colouring: both-participating pairs.