Grace/Cumulus/GraphTheory/DoubleCover/Covers.g17

Open in Workbench Download source

Imports

Multigraph.Trees

Declarations

Source

1-- Double covers of a multigraph: an indexed family of even edge sets holding2-- every edge exactly twice. Two-element labels on the edges with even local3-- multiplicity give one.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.DoubleCover.Covers10import Multigraph.Trees1112-- Cubic and loopless: every vertex meets three edge ends, no edge is a loop.13predicate Cubic (V E leftEnd rightEnd : Set) :=14  (∀ v ∈ V, degreeIn(leftEnd, rightEnd, E, v) = 3) ∧15  (∀ e ∈ E, leftEnd(e) ≠ rightEnd(e))1617-- The indices of the family H whose member holds e, and their number.18def holding (H I e : Set) : Set := { i ∈ I | e ∈ H(i) }19def multiplicity (H I e : Set) : Set := cardinality(holding(H, I, e))2021predicate EvenDoubleCover (V E leftEnd rightEnd H I : Set) :=22  Finite(I) ∧ FunctionBetween(H, I, 𝒫(E)) ∧23  (∀ i ∈ I, EvenEdgeSet(V, leftEnd, rightEnd, H(i))) ∧24  (∀ e ∈ E, multiplicity(H, I, e) = 2)2526theorem holding.subset (H I e : Set)27  shows holding(H, I, e) ⊆ I28proof29  intros i hi30  exact hi.left3132-- Two-element labels: P(e) ⊆ L has two elements, and at every vertex each33-- label s is carried by an even number of incident ends. The family34-- H(s) = {e | s ∈ P(e)} is then an even double cover.35def labelClass (E P s : Set) : Set := { e ∈ E | s ∈ P(e) }36def labelledEnds (leftEnd rightEnd E P v s : Set) : Set :=37  { p ∈ incidentEnds(leftEnd, rightEnd, E, v) | s ∈ P(fst(p)) }3839theorem labelClass.subset (E P s : Set)40  shows labelClass(E, P, s) ⊆ E41proof42  intros e he43  exact he.left4445defgraph labelFamily (E P L : Set) (s ∈ L) : 𝒫(E) := labelClass(E, P, s)46proof47  exact powerset.membership_iff.backward with labelClass.subset4849-- The ends of the class of s at v are the ends at v labelled s.50theorem labelClass.incidentEnds (leftEnd rightEnd E P v s : Set)51  shows incidentEnds(leftEnd, rightEnd, labelClass(E, P, s), v) =52    labelledEnds(leftEnd, rightEnd, E, P, v, s)53proof54  ext p55  constructor56  . intro hp57    obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp58    have ends := incidentEnds.pair.forward with hp59    refine ⟨(incidentEnds.pair.backward with ⟨he.left, ends.right⟩), ?_⟩60    rw fst.pair61    exact he.right62  . intro hp63    obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp.left64    have ends := incidentEnds.pair.forward with hp.left65    have label := hp.right66    rw fst.pair at label67    exact incidentEnds.pair.backward with ⟨⟨he, label⟩, ends.right⟩6869-- The labels holding e are exactly its pair P(e).70theorem labelFamily.holding (E P L e : Set)71  requires labels : P : E → 𝒫(L)72  requires edge : e ∈ E73  shows holding(labelFamily(E, P, L), L, e) = P(e)74proof75  have inside : P(e) ⊆ L := powerset.membership_iff.forward76    with (FunctionBetween.apply_closed with labels, edge)77  ext i78  constructor79  . intro hi80    have parts := holding.membership.forward with hi81    rw labelFamily.value with parts.left at parts82    exact (labelClass.membership.forward with parts.right).right83  . intro hi84    have inL := inside with i, hi85    refine ⟨inL, ?_⟩86    rw labelFamily.value with inL87    exact ⟨edge, hi⟩8889theorem labels.double_cover (V E leftEnd rightEnd P L : Set)90  requires graph : Graph(V, E, leftEnd, rightEnd)91  requires finiteEdges : Finite(E)92  requires finiteLabels : Finite(L)93  requires labels : FunctionBetween(P, E, 𝒫(L)) ∧94    (∀ e ∈ E, cardinality(P(e)) = 2)95  requires balanced : ∀ v ∈ V, ∀ s ∈ L,96    EvenSet(labelledEnds(leftEnd, rightEnd, E, P, v, s))97  shows EvenDoubleCover(V, E, leftEnd, rightEnd, labelFamily(E, P, L), L)98proof99  refine ⟨finiteLabels, labelFamily.function, ?_, ?_⟩100  . -- Each class is even: its ends at v are the ends labelled s there.101    intros s hs102    rw labelFamily.value with hs103    constructor104    . exact Finite.subset with finiteEdges, labelClass.subset105    . intros v hv106      unfold degreeIn107      rw labelClass.incidentEnds108      exact balanced with v, hv, s, hs109  . -- Each edge is held by its two labels.110    intros e he111    unfold multiplicity112    rw labelFamily.holding with labels.left, he113    exact labels.right with e, he114