Grace/Cumulus/GraphTheory/Flows/Splits.g17

Open in Workbench Download source

Imports

Lifting · Multigraph.Subgraph

Declarations

Source

1-- Even sets and even covers across a split, a vertex set crossed by no edge:2-- an even set of one side is even in the whole graph, covers of the two3-- sides join, and a cover found with the end functions restricted to a side4-- is a cover for the original ends.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.Splits11import Lifting12import Multigraph.Subgraph1314-- An even set of one side of a split is even in the whole graph: no edge of15-- it has an end outside the side.16theorem EvenEdgeSet.of_side (V X leftEnd rightEnd F : Set)17  requires even : EvenEdgeSet(X, leftEnd, rightEnd, F)18  requires ends : ∀ e ∈ F, leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X19  shows EvenEdgeSet(V, leftEnd, rightEnd, F)20proof21  obtain ⟨finite, degrees⟩ := even22  refine ⟨finite, _⟩23  intros v hv24  by_cases inX : v ∈ X25  . exact degrees with v, inX26  . -- No edge of F has an end at v.27    have none : incidentEnds(leftEnd, rightEnd, F, v) = ∅28      ext p29      constructor30      . intro hp31        obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp32        obtain ⟨leftX, rightX⟩ := ends with e, he33        have sides := (incidentEnds.pair.forward with hp).right34        exfalso35        rcases sides with ⟨_, atLeft⟩ | ⟨_, atRight⟩36        . rw atLeft at leftX37          exact inX with leftX38        . rw atRight at rightX39          exact inX with rightX40      . intro hp41        simp at hp42    unfold degreeIn43    rw [none, cardinality.empty]44    exact Even.zero4546-- A vertex set left by no edge splits the graph; covers of the two sides join.47theorem EvenCover.join (V E leftEnd rightEnd X F G : Set)48  requires graph : Graph(V, E, leftEnd, rightEnd)49  requires split : X ⊆ V ∧ crossing(leftEnd, rightEnd, E, X) = ∅50  requires first : EvenCover(X, inside(leftEnd, rightEnd, E, X), leftEnd,51    rightEnd, F)52  requires second : EvenCover(V ∖ X, inside(leftEnd, rightEnd, E, V ∖ X),53    leftEnd, rightEnd, G)54  shows ∃ H, EvenCover(V, E, leftEnd, rightEnd, H)55proof56  obtain ⟨subset, none⟩ := split57  obtain ⟨functionF, evenF, coversF⟩ := first58  obtain ⟨functionG, evenG, coversG⟩ := second59  have endsE := Graph.ends with graph60  -- The insides of the two sides are disjoint, and since no edge crosses61  -- between the sides, together they hold every edge.62  have apart : Disjoint(inside(leftEnd, rightEnd, E, X),63      inside(leftEnd, rightEnd, E, V ∖ X))64    rw Disjoint.iff65    intros e he inY66    have outside := difference.membership.forward with inY.right.left67    exact outside.right with he.right.left68  have sides : ∀ e ∈ E, e ∈ inside(leftEnd, rightEnd, E, X) ∨69      e ∈ inside(leftEnd, rightEnd, E, V ∖ X)70    intros e he71    obtain ⟨leftV, rightV⟩ := endsE with e, he72    have notCross : ¬e ∈ crossing(leftEnd, rightEnd, E, X)73      rw none74      simp75    by_cases leftX : leftEnd(e) ∈ X76    . left77      refine ⟨he, leftX, _⟩78      by_contra rightX79      apply notCross80      refine ⟨he, _⟩81      left82      exact ⟨leftX, rightX⟩83    . right84      have rightX : ¬rightEnd(e) ∈ X85        intro rightX86        apply notCross87        refine ⟨he, _⟩88        right89        exact ⟨rightX, leftX⟩90      exact ⟨he, (difference.membership.backward with leftV, leftX),91        (difference.membership.backward with rightV, rightX)⟩92  -- Coordinate by coordinate, the union of the two sides' even sets is an93  -- even set of the whole graph.94  have union : ∀ i ∈ 3, F(i) ∪ G(i) ∈ 𝒫(E) ∧95      EvenEdgeSet(V, leftEnd, rightEnd, F(i) ∪ G(i))96    intros i hi97    have subF : F(i) ⊆ inside(leftEnd, rightEnd, E, X) :=98      powerset.membership_iff.forward99        with (FunctionBetween.apply_closed with functionF, hi)100    have subG : G(i) ⊆ inside(leftEnd, rightEnd, E, V ∖ X) :=101      powerset.membership_iff.forward102        with (FunctionBetween.apply_closed with functionG, hi)103    have evenFi := EvenEdgeSet.of_side at V, X, leftEnd, rightEnd, F(i)104      with (evenF with i, hi),105        (ends_in.subset with (inside.ends at leftEnd, rightEnd, E, X), subF)106    have evenGi := EvenEdgeSet.of_side at V, V ∖ X, leftEnd, rightEnd, G(i)107      with (evenG with i, hi),108        (ends_in.subset with (inside.ends at leftEnd, rightEnd, E, V ∖ X),109          subG)110    have apartI : Disjoint(F(i), G(i)) :=111      Disjoint.of_subset_right112        with (Disjoint.of_subset_left with apart, subF), subG113    refine ⟨powerset.membership_iff.backward with (Subset.union2_iff.backward114      with ⟨(Subset.transitive with subF, inside.subset),115        (Subset.transitive with subG, inside.subset)⟩),116      (EvenEdgeSet.union_disjoint with evenFi, evenGi, apartI)⟩117  have zero : 0 ∈ 3 by simp [membership.three]118  have one : 1 ∈ 3 by simp [membership.three]119  have two : 2 ∈ 3 by simp [membership.three]120  obtain ⟨mem0, even0⟩ := union with 0, zero121  obtain ⟨mem1, even1⟩ := union with 1, one122  obtain ⟨mem2, even2⟩ := union with 2, two123  have values := tripleMap.value with mem0, mem1, mem2124  have valueAt : ∀ i ∈ 3,125      tripleMap(𝒫(E), F(0) ∪ G(0), F(1) ∪ G(1), F(2) ∪ G(2))(i) =126        F(i) ∪ G(i)127    intros i hi128    have cases := membership.three.forward with hi129    rcases cases with rfl | rfl | rfl130    . exact values.left131    . exact values.right.left132    . exact values.right.right133  witness tripleMap(𝒫(E), F(0) ∪ G(0), F(1) ∪ G(1), F(2) ∪ G(2))134  refine ⟨(tripleMap.function with mem0, mem1, mem2), _, _⟩135  . intros i hi136    have value := valueAt with i, hi137    rw value138    exact (union with i, hi).right139  . intros e he140    have cases := sides with e, he141    rcases cases with inX | inY142    . obtain ⟨i, hi, inF⟩ := coversF with e, inX143      have value := valueAt with i, hi144      refine ⟨i, hi, _⟩145      rw value146      simp [inF]147    . obtain ⟨i, hi, inG⟩ := coversG with e, inY148      have value := valueAt with i, hi149      refine ⟨i, hi, _⟩150      rw value151      simp [inG]152153-- An even cover found with the restricted ends is one for the original154-- ends, since a degree reads only the ends of edges of the set.155theorem EvenCover.of_restricted (W V E leftEnd rightEnd D F : Set)156  requires graph : Graph(W, E, leftEnd, rightEnd)157  requires edges : D ⊆ E158  requires cover : EvenCover(V, D, restrict(leftEnd, D), restrict(rightEnd, D),159    F)160  shows EvenCover(V, D, leftEnd, rightEnd, F)161proof162  obtain ⟨function, even, covers⟩ := cover163  refine ⟨function, _, covers⟩164  intros i hi165  have subset : F(i) ⊆ D := powerset.membership_iff.forward166    with (FunctionBetween.apply_closed with function, hi)167  obtain ⟨finite, degrees⟩ := even with i, hi168  refine ⟨finite, _⟩169  intros v hv170  have same := degreeIn.restricted at W, E, D, F(i), leftEnd, rightEnd, v171    with graph, edges, subset172  rw ← same173  exact degrees with v, hv174