Finite endpoint multigraphs with loops

Edges are labelled objects with two numbered half-edges. The endpoints may coincide, so loops are represented without quotienting or special cases. Degree and parity always count half-edge incidences; consequently a loop contributes two incidences at its vertex.

def Sabidussi.LoopMultigraph.EulerTour.vertexAt {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (i : T.Pos) : V

The vertex of the transition from the previous edge into edge i.

Equations

• T.vertexAt i = G.endAt (T.edge i) (T.depart i)

def Sabidussi.LoopMultigraph.EulerTour.arrivalAt {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (i : T.Pos) : V

The vertex at which edge i arrives.

Equations

• T.arrivalAt i = G.endAt (T.edge i) (T.depart i).rev

@[simp]

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

@[simp]

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

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

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

@[reducible, inline]

abbrev Sabidussi.LoopMultigraph.EulerTour.Occurrence {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (v : V) : Type

Occurrences of v in the cyclic transition word.

Equations

• T.Occurrence v = { i : T.Pos // T.vertexAt i = v }

@[implicit_reducible]

instance Sabidussi.LoopMultigraph.EulerTour.instFintypeOccurrence {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] {G : LoopMultigraph V E} (T : G.EulerTour) (v : V) : Fintype (T.Occurrence v)

Equations

• T.instFintypeOccurrence v = Subtype.fintype fun (i : T.Pos) => T.vertexAt i = v

def Sabidussi.LoopMultigraph.EulerTour.transitionHalfEdge {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) {v : V} (o : T.Occurrence v) : Fin 2 → HalfEdge E

The two edge ends paired at an occurrence of a transition vertex.

Side 0 is the departing end of the current edge; side 1 is the arriving end of the previous edge. The two numbered half-edges remain distinct even when the underlying edge is a loop.

Equations

• T.transitionHalfEdge o 0 = (T.edge ↑o, T.depart ↑o)
• T.transitionHalfEdge o 1 = (T.edge (T.prev ↑o), (T.depart (T.prev ↑o)).rev)

@[simp]

theorem Sabidussi.LoopMultigraph.EulerTour.vertex_transitionHalfEdge {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) {v : V} (o : T.Occurrence v) (s : Fin 2) : G.vertex (T.transitionHalfEdge o s) = v

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

A transition occurrence with a chosen side, mapped to the corresponding incident half-edge.

Equations

• T.occurrenceSideToHalfEdge v os = ⟨T.transitionHalfEdge os.1 os.2, ⋯⟩

def Sabidussi.LoopMultigraph.EulerTour.positionSideToHalfEdge {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) : T.Pos × Fin 2 → HalfEdge E

The underlying map from a position and transition side to an edge end.

Equations

• T.positionSideToHalfEdge (i, 0) = (T.edge i, T.depart i)
• T.positionSideToHalfEdge (i, 1) = (T.edge (T.prev i), (T.depart (T.prev i)).rev)

def Sabidussi.LoopMultigraph.EulerTour.halfEdgeToPositionSide {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (h : HalfEdge E) : T.Pos × Fin 2

The inverse map: a departure end belongs to its own position, and an arrival end belongs to side 1 of the next position.

Equations

• T.halfEdgeToPositionSide h = if h.2 = T.depart (T.edge.symm h.1) then (T.edge.symm h.1, 0) else (T.next (T.edge.symm h.1), 1)

theorem Sabidussi.LoopMultigraph.EulerTour.halfEdgeToPositionSide_positionSideToHalfEdge {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (p : T.Pos × Fin 2) : T.halfEdgeToPositionSide (T.positionSideToHalfEdge p) = p

theorem Sabidussi.LoopMultigraph.EulerTour.positionSideToHalfEdge_halfEdgeToPositionSide {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (h : HalfEdge E) : T.positionSideToHalfEdge (T.halfEdgeToPositionSide h) = h

def Sabidussi.LoopMultigraph.EulerTour.positionSideEquivHalfEdge {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) : T.Pos × Fin 2 ≃ HalfEdge E

Edge positions with a choice of transition side are exactly all edge ends.

Equations

• T.positionSideEquivHalfEdge = { toFun := T.positionSideToHalfEdge, invFun := T.halfEdgeToPositionSide, left_inv := ⋯, right_inv := ⋯ }

theorem Sabidussi.LoopMultigraph.EulerTour.vertex_positionSideToHalfEdge {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] {G : LoopMultigraph V E} (T : G.EulerTour) (p : T.Pos × Fin 2) : G.vertex (T.positionSideToHalfEdge p) = T.vertexAt p.1

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

The two sides of all occurrences of v are exactly the half-edges incident with v.

Equations

• T.occurrenceSideEquivHalfEdgesAt v = Equiv.prodSubtypeFstEquivSubtypeProd.symm.trans (T.positionSideEquivHalfEdge.subtypeEquiv ⋯)

theorem Sabidussi.LoopMultigraph.EulerTour.degree_eq_two_mul_card_occurrence {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] {G : LoopMultigraph V E} (T : G.EulerTour) (v : V) : G.degree v = 2 * Fintype.card (T.Occurrence v)

The degree at v is twice its number of occurrences in the transition word.

def Sabidussi.LoopMultigraph.edgeIncidence {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (v : V) (e : E) : F₂

The incidence indicator of an edge at a vertex, with both edge ends counted.

Equations

• G.edgeIncidence v e = (if G.endAt e 0 = v then 1 else 0) + if G.endAt e 1 = v then 1 else 0

def Sabidussi.LoopMultigraph.IsEvenEdgeSet {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) : Prop

An edge set is even when every vertex has even degree in the induced multigraph.

Equations

• G.IsEvenEdgeSet F = ∀ (v : V), ∑ e ∈ F, G.edgeIncidence v e = 0

structure Sabidussi.LoopMultigraph.Cycle {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) : Type u_4

A (multigraph) cycle is a nonempty inclusion-minimal even edge set.

This includes singleton loops and pairs of parallel non-loop edges.

• edges : Finset E

  The edges of the cycle.

• nonempty : self.edges.Nonempty

  A cycle is nonempty.

• even : G.IsEvenEdgeSet self.edges

  Every vertex has even degree in the cycle.

• minimal (D : Finset E) : D.Nonempty → D ⊆ self.edges → G.IsEvenEdgeSet D → D = self.edges

  The edge set is inclusion-minimal among nonempty even edge sets.

theorem Sabidussi.LoopMultigraph.singleton_loop_even {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (e : E) (hloop : G.endAt e 0 = G.endAt e 1) : G.IsEvenEdgeSet {e}

Both incidences of a loop cancel in characteristic two.

def Sabidussi.LoopMultigraph.loopCycle {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (e : E) (hloop : G.endAt e 0 = G.endAt e 1) : G.Cycle

A loop is a one-edge circuit in the minimal-even-set definition.

Equations

• G.loopCycle e hloop = { edges := {e}, nonempty := ⋯, even := ⋯, minimal := ⋯ }

theorem Sabidussi.LoopMultigraph.decompose_even_edge_set {V : Type u_3} {E : Type u_4} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LoopMultigraph V E) (F : Finset E) (hF : G.IsEvenEdgeSet F) : ∃ (L : List G.Cycle), ∀ (e : E), (List.filter (fun (C : G.Cycle) => decide (e ∈ C.edges)) L).length = if e ∈ F then 1 else 0

Every finite even edge set is an edge-disjoint union of multigraph cycles. The displayed equation records edge multiplicities and is stronger than mere equality of unions.

structure Sabidussi.LoopMultigraph.CircuitDecomposition {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LoopMultigraph V E) : Type u_6

A partition of all edge objects into circuits.

• circuits : List G.Cycle

  The list of circuits partitioning the edges.

• coveredOnce (e : E) : (List.filter (fun (C : G.Cycle) => decide (e ∈ C.edges)) self.circuits).length = 1

  Every edge object lies in exactly one circuit.

def Sabidussi.LoopMultigraph.CircuitDecomposition.Compatible {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] {G : LoopMultigraph V E} (S : G.CircuitDecomposition) (T : G.EulerTour) : Prop

A circuit decomposition is compatible with an Euler tour when no one circuit contains both edge objects of a transition.

Equations

• S.Compatible T = ∀ (i : T.Pos), ∀ C ∈ S.circuits, ¬(T.edge (T.prev i) ∈ C.edges ∧ T.edge i ∈ C.edges)

structure Sabidussi.LoopMultigraph.CompatibleFourColoring {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (T : G.EulerTour) : Type u_6

The four-colour certificate produced by the cyclic-word part of the proof.

• color : E → Color

  The colour assigned to each edge object.

• transition_ne (i : T.Pos) : self.color (T.edge (T.prev i)) ≠ self.color (T.edge i)

  Consecutive edges of the tour receive different colours.

• color_even (z : Color) : G.IsEvenEdgeSet {e : E | self.color e = z}

  Each colour class is an even edge set.

theorem Sabidussi.LoopMultigraph.CompatibleFourColoring.exists_compatible_circuit_decomposition {V : Type u_5} {E : Type u_6} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LoopMultigraph V E) {T : G.EulerTour} (K : G.CompatibleFourColoring T) : ∃ (S : G.CircuitDecomposition), S.Compatible T

Every compatible four-colouring yields a compatible circuit decomposition.