Grace/Cumulus/GraphTheory/DoubleCover/Projection.g17

Open in Workbench Download source

Imports

Expansion

Declarations

Source

1-- The expansion of a bridgeless graph is bridgeless, and an even double2-- cover of the expansion projects along the spokes to an even double cover3-- of the graph.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.Projection10import Expansion1112-- Section: Bridgelessness.1314-- A set with one element has a member that every member equals.15theorem cardinality.member_of_one (A : Set)16  requires finite : Finite(A)17  requires one : cardinality(A) = 118  shows ∃ a ∈ A, ∀ x ∈ A, x = a19proof20  have inhabited : A ≠ ∅21    intro empty22    rw [empty, cardinality.empty] at one23    contradiction24  obtain ⟨a, ha⟩ := Nonempty.of_ne_empty with inhabited25  have count := cardinality.remove_add_one with finite, ha26  have restFinite := Finite.difference at A, {a} with finite27  have zero : cardinality(A ∖ {a}) = 0 by arith28  have rest := cardinality.eq_empty_of_zero with restFinite, zero29  refine ⟨a, ha, _⟩30  intros x hx31  by_contra different32  have outside : x ∈ A ∖ {a} by simp [hx, different]33  rw rest at outside34  simp at outside3536-- A vertex of degree one has a single end (e, i), and e is then the one37-- edge leaving {v}: a bridge. So a bridgeless graph has no such vertex.38theorem Bridgeless.degrees (V E leftEnd rightEnd : Set)39  requires graph : Graph(V, E, leftEnd, rightEnd)40  requires finiteEdges : Finite(E)41  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)42  shows ∀ v ∈ V, degreeIn(leftEnd, rightEnd, E, v) ≠ 143proof44  intros v hv one45  unfold degreeIn at one46  have finiteEnds := incidentEnds.finite at leftEnd, rightEnd, E, v47    with finiteEdges48  obtain ⟨p, hp, only⟩ := cardinality.member_of_one with finiteEnds, one49  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp50  -- An edge leaving {v} has an end at v, so it is e; and e does leave {v},51  -- since its other end is not at v.52  have cut : crossing(leftEnd, rightEnd, E, {v}) = {e}53    ext f54    constructor55    . intro hf56      obtain ⟨inE, crosses⟩ := hf57      simp at crosses58      cases crosses with atLeft | atRight59      . have end : (f, 0) ∈ incidentEnds(leftEnd, rightEnd, E, v)60          simp [incidentEnds.pair, inE, atLeft]61        have same := only with (f, 0), end62        obtain ⟨rfl, _⟩ := orderedPair.injective with same63        simp64      . have end : (f, 1) ∈ incidentEnds(leftEnd, rightEnd, E, v)65          simp [incidentEnds.pair, inE, atRight]66        have same := only with (f, 1), end67        obtain ⟨rfl, _⟩ := orderedPair.injective with same68        simp69    . intro hf70      simp at hf71      rw hf72      refine ⟨he, _⟩73      have sides := (incidentEnds.pair.forward with hp).right74      rcases sides with ⟨rfl, atLeft⟩ | ⟨rfl, atRight⟩75      . have notRight : rightEnd(e) ≠ v76          intro atRight77          have end : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, v)78            simp [incidentEnds.pair, he, atRight]79          have same := only with (e, 1), end80          have oneZero := (orderedPair.injective with same).right81          contradiction82        simp [atLeft, notRight]83      . have notLeft : leftEnd(e) ≠ v84          intro atLeft85          have end : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, v)86            simp [incidentEnds.pair, he, atLeft]87          have same := only with (e, 0), end88          have oneZero := (orderedPair.injective with same).right89          contradiction90        simp [atRight, notLeft]91  have inV : {v} ⊆ V := singleton.subset_iff.backward with hv92  have bridge := bridgeless with {v}, inV93  rw [cut, cardinality.singleton] at bridge94  exact bridge with rfl9596-- The vertices all of whose ends lie in a set X of ends.97def enclosed (V E leftEnd rightEnd X : Set) : Set :=98  { v ∈ V | incidentEnds(leftEnd, rightEnd, E, v) ⊆ X }99100-- When X holds all or none of the ends at each vertex, an end of e lies in X101-- exactly when its vertex is enclosed.102theorem enclosed.left (V E leftEnd rightEnd X e : Set)103  requires graph : Graph(V, E, leftEnd, rightEnd)104  requires edge : e ∈ E105  requires whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),106    h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X107  shows (e, 0) ∈ X ↔ leftEnd(e) ∈ enclosed(V, E, leftEnd, rightEnd, X)108proof109  have inV := (Graph.ends with graph, e, edge).left110  have atLeft : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, leftEnd(e))111    simp [incidentEnds.pair, edge]112  constructor113  . intro inX114    exact ⟨inV, (whole with leftEnd(e), inV, (e, 0), atLeft, inX)⟩115  . intro inside116    exact inside.right with (e, 0), atLeft117118theorem enclosed.right (V E leftEnd rightEnd X e : Set)119  requires graph : Graph(V, E, leftEnd, rightEnd)120  requires edge : e ∈ E121  requires whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),122    h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X123  shows (e, 1) ∈ X ↔ rightEnd(e) ∈ enclosed(V, E, leftEnd, rightEnd, X)124proof125  have inV := (Graph.ends with graph, e, edge).right126  have atRight : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, rightEnd(e))127    simp [incidentEnds.pair, edge]128  constructor129  . intro inX130    exact ⟨inV, (whole with rightEnd(e), inV, (e, 1), atRight, inX)⟩131  . intro inside132    exact inside.right with (e, 1), atRight133134-- When no ring edge leaves X, the edges of the expansion leaving X are the135-- spokes of the edges leaving the enclosed vertices.136theorem enclosed.crossing (V E leftEnd rightEnd σ X : Set)137  requires graph : Graph(V, E, leftEnd, rightEnd)138  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)139  requires stable : ∀ h ∈ halfEdges(E), (h ∈ X ↔ σ(h) ∈ X)140  requires whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),141    h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X142  shows crossing(expandedLeft(E, σ), expandedRight(E, σ),143      expandedEdges(E), X) =144    {0} × crossing(leftEnd, rightEnd, E, enclosed(V, E, leftEnd, rightEnd, X))145proof146  have function := RotationSystem.function with rotation147  ext x148  constructor149  . intro hx150    obtain ⟨inExpanded, crosses⟩ := hx151    have split := expandedEdges.cases with inExpanded152    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩153    . rw [(expandedLeft.spoke with he),154        (expandedRight.spoke with function, he),155        (enclosed.left with graph, he, whole),156        (enclosed.right with graph, he, whole)] at crosses157      apply product.pair_membership.backward158      constructor159      . simp160      . exact ⟨he, crosses⟩161    . rw [(expandedLeft.ring with hh),162        (expandedRight.ring with function, hh)] at crosses163      have same := stable with h, hh164      exfalso165      tauto166  . intro hx167    obtain ⟨_, z, hz, e, he, rfl⟩ := product.membership.forward with hx168    simp at hz169    rw hz170    obtain ⟨inE, crosses⟩ := he171    refine ⟨(spokes.edge with inE), _⟩172    rw [(expandedLeft.spoke with inE),173      (expandedRight.spoke with function, inE),174      (enclosed.left with graph, inE, whole),175      (enclosed.right with graph, inE, whole)]176    exact crosses177178-- A cut of the expansion crossed by one edge is crossed by no ring edge, as179-- the ring edges form an even edge set; so it holds all or none of the ends180-- at each vertex, and pulling the ends of each vertex together gives a cut181-- of the graph crossed by one edge.182theorem expansion.bridgeless (V E leftEnd rightEnd σ : Set)183  requires graph : Graph(V, E, leftEnd, rightEnd)184  requires finiteVertices : Finite(V)185  requires finiteEdges : Finite(E)186  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)187  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)188  shows Bridgeless(halfEdges(E), expandedEdges(E),189    expandedLeft(E, σ), expandedRight(E, σ))190proof191  intros X subset one192  have function := RotationSystem.function with rotation193  have finiteRingCut : Finite(crossing(expandedLeft(E, σ),194      expandedRight(E, σ), rings(E), X)) :=195    crossing.finite with (rings.finite with finiteEdges)196  -- No ring edge leaves X: an even number of them do, and at most one.197  have evenCount := EvenEdgeSet.crossing_even198    with (halfEdges.finite with finiteEdges),199      (rings.even with finiteEdges, rotation.left), subset200  have ringsInside : rings(E) ⊆ expandedEdges(E)201    unfold expandedEdges202    exact union2.subset_right203  have ringCut :204      crossing(expandedLeft(E, σ), expandedRight(E, σ), rings(E), X) ⊆205      crossing(expandedLeft(E, σ), expandedRight(E, σ), expandedEdges(E), X) :=206    crossing.monotone with ringsInside207  have bound := cardinality.monotone208    with (crossing.finite with (expandedEdges.finite with finiteEdges)),209      ringCut210  rw one at bound211  obtain ⟨m, hm, double⟩ := evenCount212  have zero : cardinality(crossing(expandedLeft(E, σ), expandedRight(E, σ),213      rings(E), X)) = 0214    rw double at bound215    rw double216    arith217  have noRing := cardinality.eq_empty_of_zero with finiteRingCut, zero218  have stable : ∀ h ∈ halfEdges(E), (h ∈ X ↔ σ(h) ∈ X)219    intros h hh220    by_contra221    have crosses : (1, h) ∈ crossing(expandedLeft(E, σ),222        expandedRight(E, σ), rings(E), X)223      refine ⟨(rings.member with hh), _⟩224      rw [(expandedLeft.ring with hh), (expandedRight.ring with function, hh)]225      tauto226    rw noRing at crosses227    simp at crosses228  -- So X holds all the ends at a vertex or none: σ runs through them all.229  have whole : ∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),230      h ∈ X → ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v), k ∈ X231    intros v hv h hh inX k hk232    obtain ⟨n, hn, reach⟩ := rotation.right.right with v, hv, h, hh, k, hk233    have closed : ∀ x ∈ X, σ(x) ∈ X234      intros x hx235      exact (stable with x, (subset with x, hx)).forward with hx236    rw ← reach237    exact orbitStep.closed with closed, inX238  -- The enclosed vertices are then left by exactly one edge of the graph.239  have enclosedSubset : enclosed(V, E, leftEnd, rightEnd, X) ⊆ V240    intros v hv241    exact hv.left242  rw [(enclosed.crossing with graph, rotation, stable, whole),243    (cardinality.singleton_product244      with (crossing.finite with finiteEdges))] at one245  exact bridgeless with enclosed(V, E, leftEnd, rightEnd, X),246    enclosedSubset, one247248-- Section: Projection.249250-- The projection of an edge set of the expansion: the edges whose spokes it251-- holds.252def projected (E F : Set) : Set := { e ∈ E | (0, e) ∈ F }253254theorem projected.subset (E F : Set)255  shows projected(E, F) ⊆ E256proof257  intros e he258  exact he.left259260-- The edges of F leaving the ends at v are the spokes of the edges of the261-- projection leaving v: a ring edge has both ends at one vertex.262theorem projected.crossing (V E leftEnd rightEnd σ F v : Set)263  requires graph : Graph(V, E, leftEnd, rightEnd)264  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)265  requires edges : F ⊆ expandedEdges(E)266  requires vertex : v ∈ V267  shows crossing(expandedLeft(E, σ), expandedRight(E, σ), F,268      incidentEnds(leftEnd, rightEnd, E, v)) =269    {0} × crossing(leftEnd, rightEnd, projected(E, F), {v})270proof271  have function := RotationSystem.function with rotation272  ext x273  constructor274  . intro hx275    obtain ⟨inF, crosses⟩ := hx276    have split := expandedEdges.cases with (edges with x, inF)277    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩278    . rw [(expandedLeft.spoke with he), (expandedRight.spoke with function, he),279        (incidentEnds.left with he), (incidentEnds.right with he)] at crosses280      apply product.pair_membership.backward281      constructor282      . simp283      . have inProjection : e ∈ projected(E, F) := ⟨he, inF⟩284        refine ⟨inProjection, _⟩285        simp286    . rw [(expandedLeft.ring with hh),287        (expandedRight.ring with function, hh)] at crosses288      have same := RotationSystem.at_vertex with graph, rotation, vertex, hh289      exfalso290      tauto291  . intro hx292    obtain ⟨_, z, hz, e, he, rfl⟩ := product.membership.forward with hx293    simp at hz294    rw hz295    obtain ⟨inProjection, crosses⟩ := he296    obtain ⟨inE, inF⟩ := inProjection297    refine ⟨inF, _⟩298    rw [(expandedLeft.spoke with inE), (expandedRight.spoke with function, inE),299      (incidentEnds.left with inE), (incidentEnds.right with inE)]300    simp at crosses301    tauto302303-- The projection of an even edge set is even: the edges of the projection304-- leaving v are counted by the edges of F leaving the ends at v, an even305-- number.306theorem projected.even (V E leftEnd rightEnd σ F : Set)307  requires graph : Graph(V, E, leftEnd, rightEnd)308  requires finiteEdges : Finite(E)309  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)310  requires edges : F ⊆ expandedEdges(E)311  requires even : EvenEdgeSet(halfEdges(E), expandedLeft(E, σ),312    expandedRight(E, σ), F)313  shows EvenEdgeSet(V, leftEnd, rightEnd, projected(E, F))314proof315  have finiteProjected : Finite(projected(E, F)) :=316    Finite.subset with finiteEdges, projected.subset317  constructor318  . exact finiteProjected319  . intros v hv320    have finiteEnds := halfEdges.finite with finiteEdges321    have finitePoint : Finite({v}) := Finite.singleton322    have subset := incidentEnds.subset_halfEdges at leftEnd, rightEnd, E, v323    have evenCut := EvenEdgeSet.crossing_even with finiteEnds, even, subset324    rw [(projected.crossing with graph, rotation, edges, hv),325      (cardinality.singleton_product326        with (crossing.finite with finiteProjected)),327      (crossing.parity with finitePoint, finiteProjected)] at evenCut328    have inSingleton : v ∈ {v} by simp329    have weight := degreeWeights.value330      at {v}, leftEnd, rightEnd, projected(E, F), v331      with finiteProjected, inSingleton332    have natural :333        degreeWeights({v}, leftEnd, rightEnd, projected(E, F))(v) ∈ ℕ334      rw weight335      exact degreeIn.natural with finiteProjected336    rw [(natSum.singleton with natural), weight] at evenCut337    exact evenCut338339-- The projection of a family of edge sets, member by member.340def projectedFamily (E H I : Set) : Set :=341  { p ∈ I × 𝒫(E) | ∃ i ∈ I, p = (i, projected(E, H(i))) }342343theorem projectedFamily.function (E H I : Set)344  shows projectedFamily(E, H, I) : I → 𝒫(E)345proof346  constructor347  . intros p member348    exact member.left349  constructor350  . intros x y relatedY z relatedZ351    obtain ⟨_, a, _, shapeY⟩ := relatedY352    obtain ⟨_, b, _, shapeZ⟩ := relatedZ353    obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY354    obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ355    cc356  . intros i hi357    have inside : projected(E, H(i)) ∈ 𝒫(E) :=358      powerset.membership.backward with projected.subset359    refine ⟨projected(E, H(i)), inside, _⟩360    exact projectedFamily.membership.backward361      with ⟨(product.pair with hi, inside), i, hi, rfl⟩362363theorem projectedFamily.value (E H I i : Set)364  requires index : i ∈ I365  shows projectedFamily(E, H, I)(i) = projected(E, H(i))366proof367  have inside : projected(E, H(i)) ∈ 𝒫(E) :=368    powerset.membership.backward with projected.subset369  have related : relates(projectedFamily(E, H, I), i, projected(E, H(i))) :=370    projectedFamily.membership.backward371      with ⟨(product.pair with index, inside), i, index, rfl⟩372  exact FunctionBetween.apply_value373    with projectedFamily.function, index, related374375-- The members of the projected family holding e are those holding its spoke.376theorem projected.holding (E H I e : Set)377  requires edge : e ∈ E378  shows holding(projectedFamily(E, H, I), I, e) = holding(H, I, (0, e))379proof380  ext i381  by_cases hi : i ∈ I382  . have value := projectedFamily.value at E, H, I, i with hi383    simp [holding, projected, value, hi, edge]384  . simp [holding, hi]385386-- An even double cover of the expansion projects to one of the graph: each387-- member projects to an even edge set, and an edge is held as often as its388-- spoke.389theorem projected.double_cover (V E leftEnd rightEnd σ H I : Set)390  requires graph : Graph(V, E, leftEnd, rightEnd)391  requires finiteEdges : Finite(E)392  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)393  requires cover : EvenDoubleCover(halfEdges(E), expandedEdges(E),394    expandedLeft(E, σ), expandedRight(E, σ), H, I)395  shows EvenDoubleCover(V, E, leftEnd, rightEnd, projectedFamily(E, H, I), I)396proof397  obtain ⟨finiteIndex, family, evens, twice⟩ := cover398  refine ⟨finiteIndex, projectedFamily.function, _, _⟩399  . intros i hi400    rw projectedFamily.value with hi401    have edges : H(i) ⊆ expandedEdges(E) :=402      powerset.membership.forward403        with (FunctionBetween.apply_closed with family, hi)404    exact projected.even405      with graph, finiteEdges, rotation, edges, (evens with i, hi)406  . intros e he407    have spoke := twice with (0, e), (spokes.edge with he)408    unfold multiplicity at spoke409    unfold multiplicity410    rw projected.holding with he411    exact spoke412