Padding a mixed model with unused colours

Extension by zero preserves the colouring sum: embedded colourings have the original vertex values, and every other colouring has a zero vertex factor. Equality of superdimensions then preserves the free-circle factor as well.

def RS.MixedColourEmbedding.evenColouring {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {α : Type} {W : Fragment α} (F : EdgeSubset W) : F.EvenColouring k ↪ F.EvenColouring K

The induced embedding of even edge colourings.

Equations

• e.evenColouring F = { toFun := fun (ψ : F.EvenColouring k) => ⟨fun (a : { f : W.Flag // f ∉ F.flags }) => e.even (↑ψ a), ⋯⟩, inj' := ⋯ }

def RS.MixedColourEmbedding.oddColouring {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {α : Type} {W : Fragment α} (F : EdgeSubset W) : F.OddColouring ℓ ↪ F.OddColouring L

The induced embedding of odd edge colourings.

Equations

• e.oddColouring F = { toFun := fun (φ : F.OddColouring ℓ) => ⟨fun (a : ↥F.flags) => e.odd (↑φ a), ⋯⟩, inj' := ⋯ }

theorem RS.MixedColourEmbedding.evenColoursAt_map {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {α : Type} {W : Fragment α} (F : EdgeSubset W) (ψ : F.EvenColouring k) (v : W.Vertex) : F.evenColoursAt ((e.evenColouring F) ψ) v = Multiset.map (⇑e.even) (F.evenColoursAt ψ v)

Taking the even multiset commutes with embedding colours.

theorem RS.MixedColourEmbedding.oddListAt_map {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {α : Type} {W : Fragment α} (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W.Vertex) : F.oddListAt o ((e.oddColouring F) φ) v = List.map (⇑e.odd) (F.oddListAt o φ v)

Taking the odd list commutes with embedding colours because the odd embedding preserves symplectic partners.

theorem RS.MixedColourEmbedding.oddSignAt_map {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {α : Type} {W : Fragment α} (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (φ : F.OddColouring ℓ) (v : W.Vertex) : F.oddSignAt o ((e.oddColouring F) φ) v = F.oddSignAt o φ v

The odd vertex sign is preserved by embedding colours.

theorem RS.MixedColourEmbedding.mixedSummand_extendColours {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {W : ClosedFragment} (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (h : MixedFunctional k ℓ) : F.mixedSummand (h.extendColours e) o = F.mixedSummand h o

Extension by zero preserves each closed Eulerian colouring sum. Colourings using any additional colour have a zero factor.

theorem RS.MixedColourEmbedding.mixedValue_extendColours {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) {W : ClosedFragment} (F : EdgeSubset W) (h : MixedFunctional k ℓ) : F.mixedValue (h.extendColours e) = F.mixedValue h

The chosen Eulerian value is preserved by extension by zero.

theorem RS.MixedColourEmbedding.mixedPartition_extendColours {k ℓ K L : ℕ} (e : MixedColourEmbedding k ℓ K L) (h : MixedFunctional k ℓ) (hbalance : ↑K - 2 * ↑L = ↑k - 2 * ↑ℓ) (W : ClosedFragment) : mixedPartition (h.extendColours e) W = mixedPartition h W

Extension by zero preserves the full partition function when the source and target have the same superdimension.

noncomputable def RS.MixedFunctional.padColours {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (hk : k ≤ K) (hℓ : ℓ ≤ L) : MixedFunctional K L

Pad a functional with unused even colours and unused symplectic pairs of odd colours.

Equations

• h.padColours hk hℓ = h.extendColours (RS.MixedColourEmbedding.ofLE hk hℓ)

theorem RS.MixedFunctional.padColours_represents {k ℓ K L : ℕ} (h : MixedFunctional k ℓ) (hk : k ≤ K) (hℓ : ℓ ≤ L) (hbalance : ↑K - 2 * ↑L = ↑k - 2 * ↑ℓ) {f : ClosedFragment → ℂ} (hrep : h.Represents f) : (h.padColours hk hℓ).Represents f

Padding with equal numbers of unused even and odd colours preserves the represented parameter, including free circles.