Colourings of the whole subset

RS21 colours every edge of the Eulerian subset: φ : H → [2ℓ]. The edges of H with an end at an unlabelled vertex are the ones the vertex product sees; the edges with both ends labelled are seen only by the boundary vectors. Both kinds are coloured, and the colouring is one object.

This file is that object, and its restriction to the edges the vertex product sees. The restriction is a map between colouring types, stated here so that the split the flag model makes is a theorem about EdgeOddColouring rather than a definition in its own right.

def RS.EdgeSubset.EdgeOddColouring {α : Type} {W : Fragment α} (F : EdgeSubset W) (ℓ : ℕ) : Type

RS21's odd colouring: a colour on every edge of the subset, constant on the two flags of an edge.

Equations

• F.EdgeOddColouring ℓ = { φ : ↥F.flags → Fin (2 * ℓ) // ∀ (f : ↥F.flags), φ ⟨W.pairing ↑f, ⋯⟩ = φ f }

@[instance_reducible]

noncomputable instance RS.EdgeSubset.EdgeOddColouring.instFintype {α : Type} {W : Fragment α} (F : EdgeSubset W) (ℓ : ℕ) : Fintype (F.EdgeOddColouring ℓ)

Edge odd colourings are finite in number.

Equations

• RS.EdgeSubset.EdgeOddColouring.instFintype F ℓ = id inferInstance

noncomputable def RS.EdgeSubset.EdgeOddColouring.core {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} (φ : F.EdgeOddColouring ℓ) : F.CoreOddColouring ℓ

The colouring restricted to the edges with an end at a vertex — the ones the vertex product reads.

Equations

• φ.core = ⟨fun (f : ↥F.coreFlags) => ↑φ ⟨↑f, ⋯⟩, ⋯⟩

theorem RS.EdgeSubset.EdgeOddColouring.pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {ℓ : ℕ} (φ : F.EdgeOddColouring ℓ) (f : ↥F.flags) : ↑φ ⟨W.pairing ↑f, ⋯⟩ = ↑φ f

The colour of an edge is the colour of either of its flags.

def RS.EdgeSubset.edgeOddBoundaryMatch {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (st : GenBoundaryState k ℓ α) (φ : F.EdgeOddColouring ℓ) : Prop

The boundary constraint φ ∼ χ₁: at a used label the colouring agrees with the state.

Equations

• F.edgeOddBoundaryMatch st φ = ∀ (i : α) (c : Fin (2 * ℓ)), st i = Sum.inr c → ∀ (hmem : W.boundaryFlag i ∈ F.flags), ↑φ ⟨W.boundaryFlag i, hmem⟩ = c

The colour a used flag is pinned to

On the support of the state every used label is odd, so a boundary flag of the subset has a colour, and φ ∼ χ₁ pins the colouring to it. Naming that colour is what lets a core colouring be extended back over the through-edges.

noncomputable def RS.EdgeSubset.usedColour {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (χ : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags χ) {f : W.Flag} (hb : f ∈ F.boundaryFlags) : Fin (2 * ℓ)

The odd colour the state carries at a boundary flag of the subset.

Equations

• F.usedColour χ hbnd hb = Classical.choose ⋯

theorem RS.EdgeSubset.usedColour_spec {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (χ : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags χ) {f : W.Flag} (hb : f ∈ F.boundaryFlags) : χ (F.boundaryLabel hb) = Sum.inr (F.usedColour χ hbnd hb)

The named colour is the state's.

theorem RS.EdgeSubset.edgeOddColouring_eq_usedColour {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) {φ : F.EdgeOddColouring ℓ} (hφ : F.edgeOddBoundaryMatch χ φ) {f : W.Flag} (hb : f ∈ F.boundaryFlags) : ↑φ ⟨f, ⋯⟩ = F.usedColour χ hbnd hb

A matching colouring takes the named colour at every used flag.

The restriction is injective on matching colourings

Every flag of the subset either has an end at a vertex — and is then read by the restriction — or has both ends labelled, and is then pinned by φ ∼ χ₁. So two matching colourings with the same restriction agree.

theorem RS.EdgeSubset.mem_boundaryFlags_of_not_coreFlags {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.flags) (hc : f ∉ F.coreFlags) : f ∈ F.boundaryFlags

A flag the restriction forgets is a boundary flag.

theorem RS.EdgeSubset.edgeOddColouring_ext {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) {φ₁ φ₂ : F.EdgeOddColouring ℓ} (h₁ : F.edgeOddBoundaryMatch χ φ₁) (h₂ : F.edgeOddBoundaryMatch χ φ₂) (hcore : φ₁.core = φ₂.core) : φ₁ = φ₂

Two matching colourings with the same restriction are equal.

Extending a core colouring over the through-edges

A core colouring is extended by giving each through-edge the colour the state already carries at its two labelled ends. That is well defined exactly because those two ends agree, which is what φ ∼ χ₁ forces of any colouring of the whole subset.

theorem RS.EdgeSubset.not_coreFlags_pairing {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.flags) (hc : f ∉ F.coreFlags) : W.pairing f ∉ F.coreFlags

The flags the restriction forgets are closed under the pairing.

def RS.EdgeSubset.ThroughAgree {α : Type} {W : Fragment α} {k ℓ : ℕ} (F : EdgeSubset W) (χ : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags χ) : Prop

The agreement condition: at a through-edge the state's two legs carry one colour.

Equations

• F.ThroughAgree χ hbnd = ∀ (f : W.Flag) (hb : f ∈ F.boundaryFlags) (hbp : W.pairing f ∈ F.boundaryFlags), F.usedColour χ hbnd hbp = F.usedColour χ hbnd hb

theorem RS.EdgeSubset.throughAgree_congr {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ χ' : GenBoundaryState k ℓ α} (hcc : χ = χ') (hbnd : genBoundarySubsetMatches W F.flags χ) (hbnd' : genBoundarySubsetMatches W F.flags χ') : F.ThroughAgree χ hbnd ↔ F.ThroughAgree χ' hbnd'

Agreement reads only the state.

theorem RS.EdgeSubset.usedColour_congr {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ χ' : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hbnd' : genBoundarySubsetMatches W F.flags χ') {f : W.Flag} (hb : f ∈ F.boundaryFlags) (heq : χ (F.boundaryLabel hb) = χ' (F.boundaryLabel hb)) : F.usedColour χ hbnd hb = F.usedColour χ' hbnd' hb

The named colour reads only the state's value at the label.

theorem RS.EdgeSubset.throughAgree_of_eq_on_through {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ χ' : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hbnd' : genBoundarySubsetMatches W F.flags χ') (heq : ∀ (f : W.Flag) (hb : f ∈ F.boundaryFlags), W.pairing f ∈ F.boundaryFlags → χ (F.boundaryLabel hb) = χ' (F.boundaryLabel hb)) (hag : F.ThroughAgree χ hbnd) : F.ThroughAgree χ' hbnd'

Agreement reads only the through-edges' labels. Two states that agree there agree on the condition.

theorem RS.EdgeSubset.throughAgree_of_edgeOddBoundaryMatch {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) {φ : F.EdgeOddColouring ℓ} (hφ : F.edgeOddBoundaryMatch χ φ) : F.ThroughAgree χ hbnd

Only agreeing states are coloured at all. A colouring of the whole subset carries one colour on each edge, and φ ∼ χ₁ pins it at both labelled ends of a through-edge; so a state whose two legs there disagree admits no colouring.

noncomputable def RS.EdgeSubset.extendFun {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (φ' : F.CoreOddColouring ℓ) : ↥F.flags → Fin (2 * ℓ)

The extension's value: the core colouring where it is defined, and the state's own colour on a through-edge.

Equations

• RS.EdgeSubset.extendFun hbnd φ' f = if hc : ↑f ∈ F.coreFlags then ↑φ' ⟨↑f, hc⟩ else F.usedColour χ hbnd ⋯

theorem RS.EdgeSubset.extendFun_pairing {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hag : F.ThroughAgree χ hbnd) (φ' : F.CoreOddColouring ℓ) (f : ↥F.flags) : extendFun hbnd φ' ⟨W.pairing ↑f, ⋯⟩ = extendFun hbnd φ' f

The extension is constant on the two flags of an edge.

noncomputable def RS.EdgeSubset.CoreOddColouring.extend {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hag : F.ThroughAgree χ hbnd) (φ' : F.CoreOddColouring ℓ) : F.EdgeOddColouring ℓ

Extend a core colouring over the through-edges.

Equations

• RS.EdgeSubset.CoreOddColouring.extend hbnd hag φ' = ⟨RS.EdgeSubset.extendFun hbnd φ', ⋯⟩

theorem RS.EdgeSubset.CoreOddColouring.core_extend {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hag : F.ThroughAgree χ hbnd) (φ' : F.CoreOddColouring ℓ) : (extend hbnd hag φ').core = φ'

The extension restricts to what it extended.

theorem RS.EdgeSubset.coreOddBoundaryMatch_core {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} {φ : F.EdgeOddColouring ℓ} (hφ : F.edgeOddBoundaryMatch χ φ) : F.coreOddBoundaryMatch χ φ.core

A matching colouring restricts to a matching core colouring.

The round trip

The extension of a matching core colouring matches, and extending a matching colouring's restriction returns it. With injectivity this makes the restriction a bijection between the matching colourings of the whole subset and those of its core.

theorem RS.EdgeSubset.edgeOddBoundaryMatch_extend {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hag : F.ThroughAgree χ hbnd) {φ' : F.CoreOddColouring ℓ} (hφ' : F.coreOddBoundaryMatch χ φ') : F.edgeOddBoundaryMatch χ (CoreOddColouring.extend hbnd hag φ')

The extension matches the state.

theorem RS.EdgeSubset.extend_core {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hag : F.ThroughAgree χ hbnd) {φ : F.EdgeOddColouring ℓ} (hφ : F.edgeOddBoundaryMatch χ φ) : CoreOddColouring.extend hbnd hag φ.core = φ

Extending a matching colouring's restriction returns it.

The sum over colourings of the whole subset

The restriction being a bijection on the matching colourings, a sum over RS21's colourings of all of H is a sum over the flag model's colourings of its core. This is the theorem the flag model's split rests on; nothing above it assumes the split.

theorem RS.EdgeSubset.sum_edgeOddColouring {α : Type} {W : Fragment α} {k ℓ : ℕ} {F : EdgeSubset W} {χ : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W F.flags χ) (hag : F.ThroughAgree χ hbnd) (G : F.CoreOddColouring ℓ → ℂ) : (∑ φ : F.EdgeOddColouring ℓ, if F.edgeOddBoundaryMatch χ φ then G φ.core else 0) = ∑ φ' : F.CoreOddColouring ℓ, if F.coreOddBoundaryMatch χ φ' then G φ' else 0

The colouring sum over the whole subset is the sum over its core.