From a cyclic word back to a loop-capable endpoint multigraph

The letters are transition vertices and the gaps are labelled edge objects. Cyclic-word side zero denotes the preceding gap, while Euler-tour side zero denotes the current departing half-edge; the bridge therefore precomposes occurrence sides with Fin.rev.

def Sabidussi.LoopMultigraph.EulerTour.eulerWord {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) : CyclicWord.Word

The cyclic transition word read from an Euler tour.

Equations

• T.eulerWord = { n := T.n, letter := T.vertexAt }

@[simp]

theorem Sabidussi.LoopMultigraph.EulerTour.eulerWord_letter {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (i : T.Pos) : T.eulerWord.letter i = T.vertexAt i

@[simp]

theorem Sabidussi.LoopMultigraph.EulerTour.eulerWord_prev {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (i : T.Pos) : T.eulerWord.prev i = T.prev i

def Sabidussi.LoopMultigraph.EulerTour.wordOccurrenceSideEquivHalfEdgesAt {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (v : V) : T.eulerWord.Occurrence v × Fin 2 ≃ G.halfEdgesAt v

Occurrence sides with the cyclic-word convention are exactly the incident half-edges.

Equations

• T.wordOccurrenceSideEquivHalfEdgesAt v = ((Equiv.refl (T.eulerWord.Occurrence v)).prodCongr Sabidussi.LoopMultigraph.EulerTour.revFinTwoEquiv✝).trans (T.occurrenceSideEquivHalfEdgesAt v)

theorem Sabidussi.LoopMultigraph.EulerTour.incidentColor_eq_halfEdgeColor {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (x : T.eulerWord.Pos → Color) {v : V} (os : T.eulerWord.Occurrence v × Fin 2) : T.eulerWord.incidentColor x os.1 os.2 = x (T.edge.symm (↑((T.wordOccurrenceSideEquivHalfEdgesAt v) os)).1)

Under the preceding equivalence, the gap incident with a word-occurrence side is the edge underlying the corresponding half-edge.

def Sabidussi.LoopMultigraph.EulerTour.coloredOccurrenceSideEquivColoredHalfEdgesAt {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] {G : LoopMultigraph V E} (T : G.EulerTour) (C : T.eulerWord.Coloring) (v : V) (z : Color) : { os : T.eulerWord.Occurrence v × Fin 2 // T.eulerWord.incidentColor C.color os.1 os.2 = z } ≃ { h : G.halfEdgesAt v // C.color (T.edge.symm (↑h).1) = z }

The coloured occurrence sides of the word and the correspondingly coloured half-edges at a vertex are equinumerous.

Equations

• T.coloredOccurrenceSideEquivColoredHalfEdgesAt C v z = (T.wordOccurrenceSideEquivHalfEdgesAt v).subtypeEquiv ⋯

noncomputable def Sabidussi.LoopMultigraph.EulerTour.compatibleFourColoringOfWordColoring {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] {G : LoopMultigraph V E} (T : G.EulerTour) (C : T.eulerWord.Coloring) : G.CompatibleFourColoring T

A cyclic-word colouring gives the graph-theoretic compatible four-colouring certificate.

Equations

• T.compatibleFourColoringOfWordColoring C = { color := fun (e : E) => C.color (T.edge.symm e), transition_ne := ⋯, color_even := ⋯ }

theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] {G : LoopMultigraph V E} (T : G.EulerTour) (hmin : ∀ (v : V), 4 ≤ G.degree v) : ∃ (S : G.CircuitDecomposition), S.Compatible T

Sabidussi compatibility for finite endpoint multigraphs, including loops.