Grace/Cumulus/GraphTheory/Flows/Lifting.g17

Open in Workbench Download source

Imports

Contraction

Declarations

Source

1-- Lifting even sets and even covers from the contraction of an edge e: an2-- even set of the contraction lifts with or without e, and when e lies in a3-- cut of two edges an even cover of the contraction lifts to one of the4-- graph.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.GraphTheory.Flows.Lifting11import Contraction1213-- An even set of the contraction lifts to the graph, with or without e: the14-- two ends of e have degrees of equal parity in it.15theorem contraction.lift_even (V E leftEnd rightEnd e F : Set)16  requires graph : Graph(V, E, leftEnd, rightEnd)17  requires finiteVertices : Finite(V)18  requires edge : e ∈ E19  requires even : EvenEdgeSet(contractionPartition(V, leftEnd, rightEnd, e),20    contractedLeft(V, E, leftEnd, rightEnd, e),21    contractedRight(V, E, leftEnd, rightEnd, e), F)22  requires edges : F ⊆ E ∖ {e}23  shows EvenEdgeSet(V, leftEnd, rightEnd, F) ∨24    EvenEdgeSet(V, leftEnd, rightEnd, F ∪ {e})25proof26  obtain ⟨finite, degrees⟩ := even27  obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, e, edge28  have partition := contractionPartition.partition with graph, edge29  have endClass : {leftEnd(e), rightEnd(e)} ∈30      contractionPartition(V, leftEnd, rightEnd, e)31    rw ← contraction.class_end with graph, edge32    exact (classOf.member with partition, leftIn).left33  -- Away from the ends of e a vertex is its own class, with its own degree.34  have away : ∀ v ∈ V, v ≠ leftEnd(e) → v ≠ rightEnd(e) →35      Even(degreeIn(leftEnd, rightEnd, F, v))36    intros v hv left right37    have single := contraction.class_apart with graph, edge, hv, left, right38    have class : {v} ∈ contractionPartition(V, leftEnd, rightEnd, e)39      rw ← single40      exact (classOf.member with partition, hv).left41    rw ← degreeIn.contraction_singleton with graph, edge, edges, class42    exact degrees with {v}, class43  by_cases loop : leftEnd(e) = rightEnd(e)44  . -- A loop merges nothing, so F itself is even.45    left46    refine ⟨finite, _⟩47    intros v hv48    by_cases atEnd : v = leftEnd(e)49    . rw [← loop, pair.self] at endClass50      rw atEnd51      rw ← degreeIn.contraction_singleton with graph, edge, edges, endClass52      exact degrees with {leftEnd(e)}, endClass53    . have atRight : v ≠ rightEnd(e) by cc54      exact away with v, hv, atEnd, atRight55  . -- The class of the two ends has the sum of their degrees, so the two56    -- degrees have the same parity.57    have sum := degreeIn.contraction_pair58      with graph, edge, finite, edges, loop59    have evenSum := degrees with {leftEnd(e), rightEnd(e)}, endClass60    rw sum at evenSum61    have parity := (Even.add_iff at degreeIn(leftEnd, rightEnd, F, leftEnd(e)),62      degreeIn(leftEnd, rightEnd, F, rightEnd(e))).forward with evenSum63    by_cases evenLeft : Even(degreeIn(leftEnd, rightEnd, F, leftEnd(e)))64    . left65      have evenRight := parity.forward with evenLeft66      refine ⟨finite, _⟩67      intros v hv68      by_cases atLeft : v = leftEnd(e)69      . rw atLeft70        exact evenLeft71      . by_cases atRight : v = rightEnd(e)72        . rw atRight73          exact evenRight74        . exact away with v, hv, atLeft, atRight75    . -- Both degrees are odd, and e adds one end at each of them.76      right77      have oddLeft := (Odd.iff_not_even78        at degreeIn(leftEnd, rightEnd, F, leftEnd(e))).backward with evenLeft79      have notRight : ¬Even(degreeIn(leftEnd, rightEnd, F, rightEnd(e)))80        intro evenRight81        exact evenLeft with (parity.backward with evenRight)82      have oddRight := (Odd.iff_not_even83        at degreeIn(leftEnd, rightEnd, F, rightEnd(e))).backward with notRight84      have absent : ¬e ∈ F85        intro inF86        have other := edges with e, inF87        simp at other88      have apart : Disjoint(F, {e}) by simp [Disjoint.iff, absent]89      refine ⟨(Finite.union with finite, Finite.singleton), _⟩90      intros v hv91      rw degreeIn.union_disjoint with finite, Finite.singleton, apart92      by_cases atLeft : v = leftEnd(e)93      . rw [atLeft, (degreeIn.end_left with loop, rfl), Even.add_one_iff]94        exact oddLeft95      . by_cases atRight : v = rightEnd(e)96        . rw [atRight, (degreeIn.end_right with loop, rfl), Even.add_one_iff]97          exact oddRight98        . have leftAway : leftEnd(e) ≠ v by cc99          have rightAway : rightEnd(e) ≠ v by cc100          have zero : degreeIn(leftEnd, rightEnd, F, v) + 0 =101              degreeIn(leftEnd, rightEnd, F, v) by ring102          rw [(degreeIn.absent with leftAway, rightAway), zero]103          exact away with v, hv, atLeft, atRight104105-- The lift of an even set F of the contraction: F itself when that is even106-- in the graph, and otherwise F with e.107def liftedSet (V leftEnd rightEnd e F : Set) : Set :=108  F ∪ { x ∈ {e} | ¬EvenEdgeSet(V, leftEnd, rightEnd, F) }109110theorem liftedSet.cases (V leftEnd rightEnd e F : Set)111  shows (EvenEdgeSet(V, leftEnd, rightEnd, F) ∧112      liftedSet(V, leftEnd, rightEnd, e, F) = F) ∨113    (¬EvenEdgeSet(V, leftEnd, rightEnd, F) ∧114      liftedSet(V, leftEnd, rightEnd, e, F) = F ∪ {e})115proof116  unfold liftedSet117  by_cases even : EvenEdgeSet(V, leftEnd, rightEnd, F)118  . left119    refine ⟨even, _⟩120    have none : liftedSet.family(V, leftEnd, rightEnd, e, F) = ∅121      ext x122      simp [liftedSet.family, even]123    rw [none, union2.right_empty]124  . right125    refine ⟨even, _⟩126    have all : liftedSet.family(V, leftEnd, rightEnd, e, F) = {e}127      ext x128      simp [liftedSet.family, even]129    rw all130131theorem liftedSet.even (V E leftEnd rightEnd e F : Set)132  requires graph : Graph(V, E, leftEnd, rightEnd)133  requires finiteVertices : Finite(V)134  requires edge : e ∈ E135  requires even : EvenEdgeSet(contractionPartition(V, leftEnd, rightEnd, e),136    contractedLeft(V, E, leftEnd, rightEnd, e),137    contractedRight(V, E, leftEnd, rightEnd, e), F)138  requires edges : F ⊆ E ∖ {e}139  shows EvenEdgeSet(V, leftEnd, rightEnd, liftedSet(V, leftEnd, rightEnd, e, F))140    ∧ F ⊆ liftedSet(V, leftEnd, rightEnd, e, F)141    ∧ liftedSet(V, leftEnd, rightEnd, e, F) ⊆ E142proof143  have lifted := contraction.lift_even144    with graph, finiteVertices, edge, even, edges145  have cases := liftedSet.cases at V, leftEnd, rightEnd, e, F146  have edgesE : F ⊆ E := Subset.transitive with edges, difference.subset_left147  rcases cases with ⟨evenF, same⟩ | ⟨oddF, same⟩148  . rw same149    exact ⟨evenF, Subset.reflexive, edgesE⟩150  . rw same151    have evenUnion : EvenEdgeSet(V, leftEnd, rightEnd, F ∪ {e})152      rcases lifted with evenF | evenUnion153      . exfalso154        exact oddF with evenF155      . exact evenUnion156    have inE : {e} ⊆ E := singleton.subset_iff.backward with edge157    refine ⟨evenUnion, union2.subset_left, _⟩158    exact Subset.union2_iff.backward with ⟨edgesE, inE⟩159160-- When e lies in a cut {e, f} of the graph, every lifted even set holding f161-- holds e, so a cover of the contraction lifts to a cover of the graph.162theorem contraction.lift_cover (V E leftEnd rightEnd e f X F : Set)163  requires graph : Graph(V, E, leftEnd, rightEnd)164  requires finiteVertices : Finite(V)165  requires finiteEdges : Finite(E)166  requires cut : X ⊆ V ∧ crossing(leftEnd, rightEnd, E, X) = {e, f} ∧167    e ≠ f168  requires cover : EvenCover(contractionPartition(V, leftEnd, rightEnd, e),169    E ∖ {e}, contractedLeft(V, E, leftEnd, rightEnd, e),170    contractedRight(V, E, leftEnd, rightEnd, e), F)171  shows ∃ G, EvenCover(V, E, leftEnd, rightEnd, G)172proof173  obtain ⟨bound, cutEdges, distinct⟩ := cut174  obtain ⟨function, even, covers⟩ := cover175  have endsE := Graph.ends with graph176  have cutInE := crossing.subset at leftEnd, rightEnd, E, X177  have eInCut : e ∈ crossing(leftEnd, rightEnd, E, X)178    rw cutEdges179    exact pair.left180  have fInCut : f ∈ crossing(leftEnd, rightEnd, E, X)181    rw cutEdges182    exact pair.right183  have eInE := cutInE with e, eInCut184  have fNotE : ¬f ∈ {e}185    intro same186    rw singleton.membership at same187    cc188  have fOther : f ∈ E ∖ {e} :=189    difference.membership.backward with (cutInE with f, fInCut), fNotE190  -- Every coordinate lifts to an even set of the graph inside E.191  have lifts : ∀ i ∈ 3,192      EvenEdgeSet(V, leftEnd, rightEnd,193        liftedSet(V, leftEnd, rightEnd, e, F(i)))194      ∧ F(i) ⊆ liftedSet(V, leftEnd, rightEnd, e, F(i))195      ∧ liftedSet(V, leftEnd, rightEnd, e, F(i)) ⊆ E196    intros i hi197    have edgesI : F(i) ⊆ E ∖ {e} := powerset.membership_iff.forward198      with (FunctionBetween.apply_closed with function, hi)199    exact liftedSet.even200      with graph, finiteVertices, eInE, (even with i, hi), edgesI201  have zero : 0 ∈ 3 by simp [membership.three]202  have one : 1 ∈ 3 by simp [membership.three]203  have two : 2 ∈ 3 by simp [membership.three]204  have mem0 : liftedSet(V, leftEnd, rightEnd, e, F(0)) ∈ 𝒫(E) :=205    powerset.membership_iff.backward with (lifts with 0, zero).right.right206  have mem1 : liftedSet(V, leftEnd, rightEnd, e, F(1)) ∈ 𝒫(E) :=207    powerset.membership_iff.backward with (lifts with 1, one).right.right208  have mem2 : liftedSet(V, leftEnd, rightEnd, e, F(2)) ∈ 𝒫(E) :=209    powerset.membership_iff.backward with (lifts with 2, two).right.right210  have values := tripleMap.value with mem0, mem1, mem2211  have valueAt : ∀ i ∈ 3,212      tripleMap(𝒫(E), liftedSet(V, leftEnd, rightEnd, e, F(0)),213      liftedSet(V, leftEnd, rightEnd, e, F(1)),214      liftedSet(V, leftEnd, rightEnd, e, F(2)))(i) =215      liftedSet(V, leftEnd, rightEnd, e, F(i))216    intros i hi217    have cases := membership.three.forward with hi218    rcases cases with rfl | rfl | rfl219    . exact values.left220    . exact values.right.left221    . exact values.right.right222  witness tripleMap(𝒫(E), liftedSet(V, leftEnd, rightEnd, e, F(0)),223    liftedSet(V, leftEnd, rightEnd, e, F(1)),224    liftedSet(V, leftEnd, rightEnd, e, F(2)))225  refine ⟨(tripleMap.function with mem0, mem1, mem2), _, _⟩226  . intros i hi227    have value := valueAt with i, hi228    rw value229    exact (lifts with i, hi).left230  . intros g hg231    by_cases same : g = e232    . -- The lifted set holding f is even and meets the cut {e, f} in f, so233      -- it holds e as well.234      obtain ⟨i, hi, inF⟩ := covers with f, fOther235      obtain ⟨evenI, growI, inI⟩ := lifts with i, hi236      have value := valueAt with i, hi237      refine ⟨i, hi, _⟩238      rw [value, same]239      have both := EvenEdgeSet.two_cut240        with finiteVertices, evenI, bound, inI, endsE, cutEdges, distinct241      exact both.backward with (growI with f, inF)242    . have gNotE : ¬g ∈ {e}243        intro inE244        rw singleton.membership at inE245        exact same with inE246      obtain ⟨i, hi, inF⟩ :=247        covers with g, (difference.membership.backward with hg, gNotE)248      have value := valueAt with i, hi249      refine ⟨i, hi, _⟩250      rw value251      exact (lifts with i, hi).right.left with g, inF252