Grace/Cumulus/GraphTheory/DoubleCover/CycleCover.g17

Open in Workbench Download source

Imports

Cycles · Set.Choice

Declarations

Source

1-- The cycle double cover of an even double cover: replacing each even set2-- by the cycles of a chosen decomposition gives a family of cycles holding3-- every edge exactly twice.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.CycleCover10import Cycles11import Set.Choice1213predicate CycleDoubleCover (V E leftEnd rightEnd H I : Set) :=14  Finite(I) ∧ FunctionBetween(H, I, 𝒫(E)) ∧15  (∀ i ∈ I, Cycle(V, leftEnd, rightEnd, H(i))) ∧16  (∀ e ∈ E, multiplicity(H, I, e) = 2)1718-- Replacing each even set of a double cover by its cycles gives a cycle19-- double cover, indexed by the pairs (i, C) with C a cycle of the chosen20-- decomposition of H(i). An edge is held by exactly one cycle of each even21-- set holding it, so the indices holding it correspond to those of the22-- original cover.2324-- The edges of an even double cover are finitely many: every edge lies in25-- one of the finitely many even sets of the cover.26theorem EvenDoubleCover.finite_edges (V E leftEnd rightEnd H I : Set)27  requires cover : EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)28  shows Finite(E)29proof30  obtain ⟨finiteI, family, evens, twice⟩ := cover31  have finiteImage :=32    Finite.function_image with family, finiteI, Subset.reflexive33  have members : ∀ S ∈ functionImage(H, I, 𝒫(E)), Finite(S)34    intros S hS35    obtain ⟨_, i, hi, rfl⟩ := hS36    exact (evens with i, hi).left37  have finiteUnion := Finite.big_union with finiteImage, members38  have inside : E ⊆ ⋃(functionImage(H, I, 𝒫(E)))39    intros e he40    have count := twice with e, he41    have inhabited : holding(H, I, e) ≠ ∅42      intro empty43      unfold multiplicity at count44      rw [empty, cardinality.empty] at count45      arith46    obtain ⟨i, hi⟩ := Nonempty.of_ne_empty with inhabited47    have parts := holding.membership.forward with hi48    have image : H(i) ∈ functionImage(H, I, 𝒫(E)) :=49      ⟨(FunctionBetween.apply_closed with family, parts.left), i, parts.left,50        rfl⟩51    exact union.membership.backward with ⟨H(i), image, parts.right⟩52  exact Finite.subset with finiteUnion, inside5354-- The decompositions of an edge set into cycles, and a chosen one.55def cycleDecompositions (V leftEnd rightEnd F : Set) : Set :=56  { D ∈ 𝒫(𝒫(F)) | Finite(D) ∧57    (∀ C ∈ D, Cycle(V, leftEnd, rightEnd, C)) ∧58    (∀ C ∈ D, ∀ B ∈ D, C ≠ B → Disjoint(C, B)) ∧ ⋃(D) = F }5960def chosenCycles (V leftEnd rightEnd F : Set) : Set :=61  choose(cycleDecompositions(V, leftEnd, rightEnd, F))6263theorem chosenCycles.decomposes (V leftEnd rightEnd F : Set)64  requires finiteVertices : Finite(V)65  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V66  requires even : EvenEdgeSet(V, leftEnd, rightEnd, F)67  shows chosenCycles(V, leftEnd, rightEnd, F) ∈68    cycleDecompositions(V, leftEnd, rightEnd, F)69proof70  obtain ⟨D, finiteD, cycles, apart, covers⟩ :=71    EvenEdgeSet.cycle_decomposition with finiteVertices, ends, even72  have inside : D ∈ 𝒫(𝒫(F))73    apply powerset.membership_iff.backward74    intros C hC75    apply powerset.membership_iff.backward76    rw ← covers77    exact union.subset_of_member with hC78  have member : D ∈ cycleDecompositions(V, leftEnd, rightEnd, F) :=79    ⟨inside, finiteD, cycles, apart, covers⟩80  have inhabited : Nonempty(cycleDecompositions(V, leftEnd, rightEnd, F)) :=81    ⟨D, member⟩82  unfold chosenCycles83  exact choose.member with inhabited8485-- In an even double cover every H(i) has its chosen decomposition.86theorem chosenCycles.of_cover (V E leftEnd rightEnd H I i : Set)87  requires graph : Graph(V, E, leftEnd, rightEnd)88  requires finiteVertices : Finite(V)89  requires cover : EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)90  requires index : i ∈ I91  shows chosenCycles(V, leftEnd, rightEnd, H(i)) ∈92    cycleDecompositions(V, leftEnd, rightEnd, H(i))93proof94  have ends := Graph.ends with graph95  have edges : H(i) ⊆ E := powerset.membership_iff.forward96    with (FunctionBetween.apply_closed with cover.right.left, index)97  exact chosenCycles.decomposes with finiteVertices,98    (ends_in.subset with ends, edges), (cover.right.right.left with i, index)99100-- The pairs (i, C) with C a cycle of the chosen decomposition of H(i), and101-- the family sending (i, C) to C.102def cycleIndex (V E leftEnd rightEnd H I : Set) : Set :=103  { p ∈ I × 𝒫(E) |104    snd(p) ∈ chosenCycles(V, leftEnd, rightEnd, H(fst(p))) }105106theorem cycleIndex.second (V E leftEnd rightEnd H I p : Set)107  requires member : p ∈ cycleIndex(V, E, leftEnd, rightEnd, H, I)108  shows snd(p) ∈ 𝒫(E)109proof110  obtain ⟨_, i, hi, C, hC, rfl⟩ := product.membership.forward111    with member.left112  rw snd.pair113  exact hC114115defgraph cycleFamily (V E leftEnd rightEnd H I : Set)116  (p ∈ cycleIndex(V, E, leftEnd, rightEnd, H, I)) : 𝒫(E) := snd(p)117proof118  exact cycleIndex.second with member119120-- An index holding e is a pair (i, C) with i holding e and C a cycle of121-- the chosen decomposition of H(i) through e.122theorem cycleIndex.holding (V E leftEnd rightEnd H I e p : Set)123  requires graph : Graph(V, E, leftEnd, rightEnd)124  requires finiteVertices : Finite(V)125  requires cover : EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)126  requires member : p ∈ holding(cycleFamily(V, E, leftEnd, rightEnd, H, I),127    cycleIndex(V, E, leftEnd, rightEnd, H, I), e)128  shows ∃ i ∈ I, ∃ C ∈ chosenCycles(V, leftEnd, rightEnd, H(i)),129    p = (i, C) ∧ e ∈ C ∧ e ∈ H(i)130proof131  have inIndex := member.left132  have holds := member.right133  rw cycleFamily.value with inIndex at holds134  obtain ⟨_, i, hi, C, hC, shape⟩ := product.membership.forward135    with inIndex.left136  have inChosen := inIndex.right137  rw [shape, snd.pair, fst.pair] at inChosen138  rw [shape, snd.pair] at holds139  obtain ⟨_, _, _, _, covers⟩ :=140    chosenCycles.of_cover with graph, finiteVertices, cover, hi141  have inH : e ∈ H(i)142    rw ← covers143    exact union.membership.backward with ⟨C, inChosen, holds⟩144  exact ⟨i, hi, C, inChosen, shape, holds, inH⟩145146-- The first projection is a bijection from the indices (i, C) holding e to147-- the indices i holding e: the cycle C of H(i) through e is unique.148def cycleProjection (V E leftEnd rightEnd H I e : Set) : Set :=149  { r ∈ holding(cycleFamily(V, E, leftEnd, rightEnd, H, I),150      cycleIndex(V, E, leftEnd, rightEnd, H, I), e) × holding(H, I, e) |151    snd(r) = fst(fst(r)) }152153theorem cycleProjection.bijective (V E leftEnd rightEnd H I e : Set)154  requires graph : Graph(V, E, leftEnd, rightEnd)155  requires finiteVertices : Finite(V)156  requires cover : EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)157  shows BijectiveBetween(cycleProjection(V, E, leftEnd, rightEnd, H, I, e),158    holding(cycleFamily(V, E, leftEnd, rightEnd, H, I),159      cycleIndex(V, E, leftEnd, rightEnd, H, I), e),160    holding(H, I, e))161proof162  have family := cover.right.left163  have function : FunctionBetween(cycleProjection(V, E, leftEnd, rightEnd,164      H, I, e), holding(cycleFamily(V, E, leftEnd, rightEnd, H, I),165      cycleIndex(V, E, leftEnd, rightEnd, H, I), e), holding(H, I, e))166    constructor167    . intros r hr168      exact hr.left169    . constructor170      . intros x y xy z xz171        have valueY := xy.right172        have valueZ := xz.right173        simp [fst.pair, snd.pair] at valueY, valueZ174        cc175      . intros p hp176        obtain ⟨i, hi, C, hC, shape, holds, inH⟩ :=177          cycleIndex.holding with graph, finiteVertices, cover, hp178        have target : i ∈ holding(H, I, e) := ⟨hi, inH⟩179        refine ⟨i, target, ?_⟩180        apply cycleProjection.membership.backward181        refine ⟨(product.pair with hp, target), ?_⟩182        rw shape183        simp [fst.pair, snd.pair]184  constructor185  . refine ⟨function, ?_⟩186    -- Two indices with the same first coordinate i are cycles of the187    -- decomposition of H(i) both through e, hence equal.188    intros x hx y hy z hz xz yz189    obtain ⟨i, hi, C, hC, shapeX, holdsX, _⟩ :=190      cycleIndex.holding with graph, finiteVertices, cover, hx191    obtain ⟨j, hj, B, hB, shapeY, holdsY, _⟩ :=192      cycleIndex.holding with graph, finiteVertices, cover, hy193    have valueX := xz.right194    have valueY := yz.right195    simp [fst.pair, snd.pair] at valueX, valueY196    have same : i = j by cc197    rw ← same at hB198    obtain ⟨_, _, _, apart, _⟩ :=199      chosenCycles.of_cover with graph, finiteVertices, cover, hi200    have equal : C = B201      by_contra different202      have disjoint := apart with C, hC, B, hB, different203      rw Disjoint.iff at disjoint204      exact disjoint with e, holdsX, holdsY205    rw [shapeX, shapeY, same, equal]206  . refine ⟨function, ?_⟩207    -- An index i holding e: e lies in some cycle C of H(i), and (i, C)208    -- holds e.209    intros i hi210    have inI := hi.left211    have inH := hi.right212    obtain ⟨inPowerset, _, _, _, covers⟩ :=213      chosenCycles.of_cover with graph, finiteVertices, cover, inI214    have inUnion : e ∈ ⋃(chosenCycles(V, leftEnd, rightEnd, H(i)))215      rw covers216      exact inH217    obtain ⟨C, hC, holds⟩ := union.membership.forward with inUnion218    have cyclesIn : chosenCycles(V, leftEnd, rightEnd, H(i)) ⊆ 𝒫(H(i)) :=219      powerset.membership_iff.forward with inPowerset220    have edges : H(i) ⊆ E := powerset.membership_iff.forward221      with (FunctionBetween.apply_closed with family, inI)222    have inside : C ⊆ E := Subset.transitive223      with (powerset.membership_iff.forward with (cyclesIn with C, hC)), edges224    have inIndex : (i, C) ∈ cycleIndex(V, E, leftEnd, rightEnd, H, I)225      refine ⟨(product.pair with inI,226        (powerset.membership_iff.backward with inside)), ?_⟩227      rw [snd.pair, fst.pair]228      exact hC229    have inHolding : (i, C) ∈ holding(cycleFamily(V, E, leftEnd, rightEnd,230        H, I), cycleIndex(V, E, leftEnd, rightEnd, H, I), e)231      refine ⟨inIndex, ?_⟩232      rw [(cycleFamily.value with inIndex), snd.pair]233      exact holds234    refine ⟨(i, C), inHolding, ?_⟩235    apply cycleProjection.membership.backward236    refine ⟨(product.pair with inHolding, hi), ?_⟩237    simp [fst.pair, snd.pair]238239theorem EvenDoubleCover.to_cycles (V E leftEnd rightEnd H I : Set)240  requires graph : Graph(V, E, leftEnd, rightEnd)241  requires finiteVertices : Finite(V)242  requires cover : EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)243  shows ∃ K, ∃ J, CycleDoubleCover(V, E, leftEnd, rightEnd, K, J)244proof245  have finiteE := EvenDoubleCover.finite_edges with cover246  obtain ⟨finiteI, family, evens, twice⟩ := cover247  have indexSubset : cycleIndex(V, E, leftEnd, rightEnd, H, I) ⊆ I × 𝒫(E)248    intros p hp249    exact hp.left250  have finiteIndex := Finite.subset251    with (Finite.product with finiteI, (Finite.powerset with finiteE)),252      indexSubset253  witness cycleFamily(V, E, leftEnd, rightEnd, H, I)254  witness cycleIndex(V, E, leftEnd, rightEnd, H, I)255  refine ⟨finiteIndex, cycleFamily.function, ?_, ?_⟩256  . -- Each index (i, C) names a cycle C of H(i).257    intros p hp258    rw cycleFamily.value with hp259    obtain ⟨_, i, hi, C, hC, shape⟩ := product.membership.forward260      with hp.left261    have inChosen := hp.right262    rw [shape, snd.pair, fst.pair] at inChosen263    rw [shape, snd.pair]264    obtain ⟨_, _, cycles, _, _⟩ :=265      chosenCycles.of_cover with graph, finiteVertices, cover, hi266    exact cycles with C, inChosen267  . -- The indices holding e correspond to the two indices of the cover268    -- holding e.269    intros e he270    have count := twice with e, he271    unfold multiplicity at count272    unfold multiplicity273    rw ← count274    have bijective :=275      cycleProjection.bijective at V, E, leftEnd, rightEnd, H, I, e276        with graph, finiteVertices, cover277    have finiteSource : Finite(holding(cycleFamily(V, E, leftEnd, rightEnd,278        H, I), cycleIndex(V, E, leftEnd, rightEnd, H, I), e)) :=279      Finite.subset with finiteIndex, holding.subset280    exact cardinality.bijective with finiteSource, bijective281