Ordinary circuits in endpoint multigraphs

This file relates the binary minimal even edge set notion used by the colouring proof to the usual graph-theoretic notion of a circuit. Connectivity below is phrased directly in terms of chains of incident labelled edges; in particular it does not mention parity or minimality. Loops and parallel edges need no exceptional representation.

@[simp]

theorem Sabidussi.LoopMultigraph.mem_edgeSupport_iff {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) {F : Finset E} {v : V} : v ∈ G.edgeSupport F ↔ ∃ e ∈ F, ∃ (i : Fin 2), G.endAt e i = v

theorem Sabidussi.LoopMultigraph.degreeIn_cast {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) (v : V) : ↑(G.degreeIn F v) = ∑ e ∈ F, G.edgeIncidence v e

theorem Sabidussi.LoopMultigraph.isEvenEdgeSet_iff_even_degree {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) : G.IsEvenEdgeSet F ↔ ∀ (v : V), Even (G.degreeIn F v)

theorem Sabidussi.LoopMultigraph.degreeIn_pos_iff_mem_edgeSupport {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) (v : V) : 0 < G.degreeIn F v ↔ v ∈ G.edgeSupport F

theorem Sabidussi.LoopMultigraph.sum_degreeIn {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) : ∑ v : V, G.degreeIn F v = 2 * F.card

The degree-sum formula, valid without excluding loops: each labelled edge has exactly two numbered ends.

theorem Sabidussi.LoopMultigraph.Cycle.edgeConnected {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (C : G.Cycle) : G.EdgeConnected C.edges

Inclusion-minimal even edge sets are connected in the ordinary edge-chain sense.

noncomputable def Sabidussi.LoopMultigraph.incidenceMatrix {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) : Matrix (↥(G.edgeSupport F)) (↥F) F₂

The vertex-edge incidence matrix of an edge set, with rows restricted to its support.

Equations

• G.incidenceMatrix F v e = G.edgeIncidence ↑v ↑e

noncomputable def Sabidussi.LoopMultigraph.incidenceMap {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) : (↥F → F₂) →ₗ[F₂] ↥(G.edgeSupport F) → F₂

The incidence matrix as a linear map over F₂.

Equations

• G.incidenceMap F = (G.incidenceMatrix F).mulVecLin

@[simp]

theorem Sabidussi.LoopMultigraph.incidenceMap_apply {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (F : Finset E) (x : ↥F → F₂) (v : ↥(G.edgeSupport F)) : (G.incidenceMap F) x v = ∑ e : ↥F, G.edgeIncidence ↑v ↑e * x e

theorem Sabidussi.LoopMultigraph.Cycle.degree_eq_two {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (C : G.Cycle) {v : V} (hv : v ∈ G.edgeSupport C.edges) : G.degreeIn C.edges v = 2

Every supported vertex of a binary cycle has ordinary degree exactly two.

def Sabidussi.LoopMultigraph.Cycle.toOrdinaryCircuit {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (C : G.Cycle) : G.OrdinaryCircuit

Regard a minimal nonempty binary-even edge set as an ordinary connected 2-regular circuit.

Equations

• Sabidussi.LoopMultigraph.Cycle.toOrdinaryCircuit G C = { edges := C.edges, nonempty := ⋯, connected := ⋯, twoRegular := ⋯ }

@[simp]

theorem Sabidussi.LoopMultigraph.Cycle.toOrdinaryCircuit_edges {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (C : G.Cycle) : (toOrdinaryCircuit G C).edges = C.edges

theorem Sabidussi.LoopMultigraph.OrdinaryCircuit.even {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] (G : LoopMultigraph V E) (C : G.OrdinaryCircuit) : G.IsEvenEdgeSet C.edges

An ordinary circuit is an even edge set (including the singleton-loop case).

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

The existing minimal-even-set decomposition can therefore be read as a decomposition into ordinary connected 2-regular circuits.

def Sabidussi.LoopMultigraph.CircuitDecomposition.toOrdinary {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LoopMultigraph V E) (S : G.CircuitDecomposition) : G.OrdinaryCircuitDecomposition

Transport a decomposition from the minimal-even representation to ordinary circuits.

Equations

• Sabidussi.LoopMultigraph.CircuitDecomposition.toOrdinary G S = { circuits := List.map (Sabidussi.LoopMultigraph.Cycle.toOrdinaryCircuit G) S.circuits, coveredOnce := ⋯ }

theorem Sabidussi.LoopMultigraph.CircuitDecomposition.compatible_toOrdinary {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq E] (G : LoopMultigraph V E) {T : G.EulerTour} {S : G.CircuitDecomposition} (h : S.Compatible T) : (toOrdinary G S).Compatible T

theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary {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.OrdinaryCircuitDecomposition), S.Compatible T

Sabidussi compatibility with the conclusion expressed using ordinary connected 2-regular circuits rather than minimal binary-even edge sets.