Flipping an odd colouring

Reversing the odd colouring at a chosen edge is an involution of the colourings, so summing a value over the colourings is invariant under it — the reindexing the circuit-sign computation uses.

noncomputable def RS.EdgeSubset.OddColouring.flip {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (T : Finset W.Flag) (hT : ∀ g ∈ T, W.pairing g ∈ T) (φ : F.OddColouring ℓ) : F.OddColouring ℓ

Flip an odd colouring on a pairing-closed set of flags: apply oddPartner to every colour indexed by a flag in T, leave the rest unchanged.

Equations

• RS.EdgeSubset.OddColouring.flip F T hT φ = ⟨fun (f : ↥F.flags) => if ↑f ∈ T then RS.oddPartner ℓ (↑φ f) else ↑φ f, ⋯⟩

theorem RS.EdgeSubset.OddColouring.flip_flip {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (T : Finset W.Flag) (hT : ∀ g ∈ T, W.pairing g ∈ T) (φ : F.OddColouring ℓ) : flip F T hT (flip F T hT φ) = φ

Flipping twice is the identity.

noncomputable def RS.EdgeSubset.OddColouring.flipEquiv {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (T : Finset W.Flag) (hT : ∀ g ∈ T, W.pairing g ∈ T) : F.OddColouring ℓ ≃ F.OddColouring ℓ

The flip as a self-equivalence on odd colourings.

Equations

• RS.EdgeSubset.OddColouring.flipEquiv F T hT = { toFun := RS.EdgeSubset.OddColouring.flip F T hT, invFun := RS.EdgeSubset.OddColouring.flip F T hT, left_inv := ⋯, right_inv := ⋯ }

theorem RS.EdgeSubset.OddColouring.sum_flip {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (T : Finset W.Flag) (hT : ∀ g ∈ T, W.pairing g ∈ T) (g : F.OddColouring ℓ → ℂ) : ∑ φ : F.OddColouring ℓ, g (flip F T hT φ) = ∑ φ : F.OddColouring ℓ, g φ

Summing over flipped colourings equals summing over the originals.

theorem RS.EdgeSubset.OddColouring.flip_val_mem {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (T : Finset W.Flag) (hT : ∀ g ∈ T, W.pairing g ∈ T) (φ : F.OddColouring ℓ) (f : ↥F.flags) (h : ↑f ∈ T) : ↑(flip F T hT φ) f = oddPartner ℓ (↑φ f)

The value of flip at a flag in T.

theorem RS.EdgeSubset.OddColouring.flip_val_not_mem {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} (T : Finset W.Flag) (hT : ∀ g ∈ T, W.pairing g ∈ T) (φ : F.OddColouring ℓ) (f : ↥F.flags) (h : ↑f ∉ T) : ↑(flip F T hT φ) f = ↑φ f

The value of flip at a flag not in T.