Grace/Cumulus/GraphTheory/DoubleCover/Expansion.g17

Open in Workbench Download source

Imports

RotationSystems

Declarations

Source

1-- The cubic expansion of a multigraph along a rotation system: the vertices2-- are the edge ends, the spoke of an edge joins its two ends, and the ring3-- edges at a vertex run around the cycle of its ends. The expansion is a4-- graph, and it is cubic and loopless when every degree is at least two.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.DoubleCover.Expansion11import RotationSystems1213-- Section: The expanded graph.1415-- The expanded graph has the ends as vertices. The spoke (0, e) of an edge16-- e joins its ends (e, 0) and (e, 1); the ring edge (1, h) of an end h joins17-- h to σ(h), so the ring edges at a vertex run around the cycle of its ends.18def spokes (E : Set) : Set := {0} × E19def rings (E : Set) : Set := {1} × halfEdges(E)20def expandedEdges (E : Set) : Set := spokes(E) ∪ rings(E)21def expandedLeft (E σ : Set) : Set :=22  { p ∈ expandedEdges(E) × halfEdges(E) |23    ∃ e ∈ E, p = ((0, e), (e, 0)) ∨24      (∃ h ∈ halfEdges(E), p = ((1, h), h)) }25def expandedRight (E σ : Set) : Set :=26  { p ∈ expandedEdges(E) × halfEdges(E) |27    ∃ e ∈ E, p = ((0, e), (e, 1)) ∨28      (∃ h ∈ halfEdges(E), p = ((1, h), σ(h))) }2930theorem spokes.member (E e : Set)31  requires edge : e ∈ E32  shows (0, e) ∈ spokes(E)33proof34  unfold spokes35  simp [product.pair_membership, edge]3637theorem rings.member (E h : Set)38  requires end : h ∈ halfEdges(E)39  shows (1, h) ∈ rings(E)40proof41  unfold rings42  simp [product.pair_membership, end]4344theorem spokes.edge (E e : Set)45  requires edge : e ∈ E46  shows (0, e) ∈ expandedEdges(E)47proof48  unfold expandedEdges49  simp [(spokes.member with edge)]5051theorem rings.edge (E h : Set)52  requires end : h ∈ halfEdges(E)53  shows (1, h) ∈ expandedEdges(E)54proof55  unfold expandedEdges56  simp [(rings.member with end)]5758-- An edge of the expansion is a spoke or a ring edge.59theorem expandedEdges.cases (E x : Set)60  requires member : x ∈ expandedEdges(E)61  shows (∃ e ∈ E, x = (0, e)) ∨ (∃ h ∈ halfEdges(E), x = (1, h))62proof63  unfold expandedEdges at member64  have split := union2.membership.forward with member65  cases split with spoke | ring66  . unfold spokes at spoke67    obtain ⟨_, z, hz, e, he, rfl⟩ := product.membership.forward with spoke68    simp at hz69    left70    refine ⟨e, he, _⟩71    rw hz72  . unfold rings at ring73    obtain ⟨_, z, hz, h, hh, rfl⟩ := product.membership.forward with ring74    simp at hz75    right76    refine ⟨h, hh, _⟩77    rw hz7879-- Spokes and ring edges are told apart by their first coordinate.80theorem expandedEdges.apart (E : Set)81  shows Disjoint(spokes(E), rings(E))82proof83  have heads : Disjoint({0}, {1})84    apply Disjoint.iff.backward85    intros x hx86    simp at hx87    rw hx88    simp89  unfold spokes90  unfold rings91  exact product.disjoint_of_left with heads9293-- The expansion of a finite graph is finite.94theorem spokes.finite (E : Set)95  requires finiteEdges : Finite(E)96  shows Finite(spokes(E))97proof98  unfold spokes99  exact Finite.product with Finite.singleton, finiteEdges100101theorem rings.finite (E : Set)102  requires finiteEdges : Finite(E)103  shows Finite(rings(E))104proof105  unfold rings106  have finiteEnds := halfEdges.finite with finiteEdges107  exact Finite.product with Finite.singleton, finiteEnds108109theorem expandedEdges.finite (E : Set)110  requires finiteEdges : Finite(E)111  shows Finite(expandedEdges(E))112proof113  unfold expandedEdges114  exact Finite.union with (spokes.finite with finiteEdges),115    (rings.finite with finiteEdges)116117-- The end maps, read off their graphs: a spoke (0, e) runs from (e, 0) to118-- (e, 1), a ring edge (1, h) from h to σ(h).119theorem expandedLeft.of_relates (E σ x y : Set)120  requires related : relates(expandedLeft(E, σ), x, y)121  shows (∃ e ∈ E, x = (0, e) ∧ y = (e, 0)) ∨122    (∃ h ∈ halfEdges(E), x = (1, h) ∧ y = h)123proof124  obtain ⟨_, e, he, shape⟩ := related125  rcases shape with spoke | ⟨h, hh, ring⟩126  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with spoke127    left128    exact ⟨e, he, rfl, rfl⟩129  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with ring130    right131    exact ⟨h, hh, rfl, rfl⟩132133theorem expandedRight.of_relates (E σ x y : Set)134  requires related : relates(expandedRight(E, σ), x, y)135  shows (∃ e ∈ E, x = (0, e) ∧ y = (e, 1)) ∨136    (∃ h ∈ halfEdges(E), x = (1, h) ∧ y = σ(h))137proof138  obtain ⟨_, e, he, shape⟩ := related139  rcases shape with spoke | ⟨h, hh, ring⟩140  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with spoke141    left142    exact ⟨e, he, rfl, rfl⟩143  . obtain ⟨rfl, rfl⟩ := orderedPair.injective with ring144    right145    exact ⟨h, hh, rfl, rfl⟩146147theorem expandedLeft.spoke_relates (E σ e : Set)148  requires edge : e ∈ E149  shows relates(expandedLeft(E, σ), (0, e), (e, 0))150proof151  apply expandedLeft.membership.backward152  refine ⟨(product.pair with (spokes.edge with edge),153      (halfEdges.left with edge)), e, edge, _⟩154  left155  rfl156157theorem expandedRight.spoke_relates (E σ e : Set)158  requires edge : e ∈ E159  shows relates(expandedRight(E, σ), (0, e), (e, 1))160proof161  apply expandedRight.membership.backward162  refine ⟨(product.pair with (spokes.edge with edge),163      (halfEdges.right with edge)), e, edge, _⟩164  left165  rfl166167theorem expandedLeft.ring_relates (E σ h : Set)168  requires end : h ∈ halfEdges(E)169  shows relates(expandedLeft(E, σ), (1, h), h)170proof171  obtain ⟨e, he, _, _, _⟩ := halfEdges.shape with end172  apply expandedLeft.membership.backward173  refine ⟨(product.pair with (rings.edge with end), end), e, he, _⟩174  right175  exact ⟨h, end, rfl⟩176177theorem expandedRight.ring_relates (E σ h : Set)178  requires function : σ : halfEdges(E) → halfEdges(E)179  requires end : h ∈ halfEdges(E)180  shows relates(expandedRight(E, σ), (1, h), σ(h))181proof182  obtain ⟨e, he, _, _, _⟩ := halfEdges.shape with end183  have image := FunctionBetween.apply_closed with function, end184  apply expandedRight.membership.backward185  refine ⟨(product.pair with (rings.edge with end), image), e, he, _⟩186  right187  exact ⟨h, end, rfl⟩188189theorem expandedLeft.function (E σ : Set)190  shows expandedLeft(E, σ) : expandedEdges(E) → halfEdges(E)191proof192  constructor193  . intros p member194    exact member.left195  constructor196  . intros x y relatedY z relatedZ197    have shapeY := expandedLeft.of_relates with relatedY198    have shapeZ := expandedLeft.of_relates with relatedZ199    rcases shapeY with ⟨e, he, rfl, rfl⟩ | ⟨h, hh, rfl, rfl⟩200    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩201      . obtain ⟨_, rfl⟩ := orderedPair.injective with same202        rfl203      . obtain ⟨zeroOne, _⟩ := orderedPair.injective with same204        contradiction205    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩206      . obtain ⟨oneZero, _⟩ := orderedPair.injective with same207        contradiction208      . obtain ⟨_, rfl⟩ := orderedPair.injective with same209        rfl210  . intros x member211    have split := expandedEdges.cases with member212    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩213    . exact ⟨(e, 0), (halfEdges.left with he),214        (expandedLeft.spoke_relates with he)⟩215    . exact ⟨h, hh, (expandedLeft.ring_relates with hh)⟩216217theorem expandedRight.function (E σ : Set)218  requires function : σ : halfEdges(E) → halfEdges(E)219  shows expandedRight(E, σ) : expandedEdges(E) → halfEdges(E)220proof221  constructor222  . intros p member223    exact member.left224  constructor225  . intros x y relatedY z relatedZ226    have shapeY := expandedRight.of_relates with relatedY227    have shapeZ := expandedRight.of_relates with relatedZ228    rcases shapeY with ⟨e, he, rfl, rfl⟩ | ⟨h, hh, rfl, rfl⟩229    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩230      . obtain ⟨_, rfl⟩ := orderedPair.injective with same231        rfl232      . obtain ⟨zeroOne, _⟩ := orderedPair.injective with same233        contradiction234    . rcases shapeZ with ⟨f, hf, same, rfl⟩ | ⟨k, hk, same, rfl⟩235      . obtain ⟨oneZero, _⟩ := orderedPair.injective with same236        contradiction237      . obtain ⟨_, rfl⟩ := orderedPair.injective with same238        rfl239  . intros x member240    have split := expandedEdges.cases with member241    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩242    . exact ⟨(e, 1), (halfEdges.right with he),243        (expandedRight.spoke_relates with he)⟩244    . exact ⟨σ(h), (FunctionBetween.apply_closed with function, hh),245        (expandedRight.ring_relates with function, hh)⟩246247theorem expansion.graph (V E leftEnd rightEnd σ : Set)248  requires graph : Graph(V, E, leftEnd, rightEnd)249  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)250  shows Graph(halfEdges(E), expandedEdges(E),251    expandedLeft(E, σ), expandedRight(E, σ))252proof253  have function := RotationSystem.function with rotation254  exact ⟨expandedLeft.function, (expandedRight.function with function)⟩255256-- The values of the end maps.257theorem expandedLeft.spoke (E σ e : Set)258  requires edge : e ∈ E259  shows expandedLeft(E, σ)((0, e)) = (e, 0)260proof261  exact FunctionBetween.apply_value with expandedLeft.function,262    (spokes.edge with edge), (expandedLeft.spoke_relates with edge)263264theorem expandedRight.spoke (E σ e : Set)265  requires function : σ : halfEdges(E) → halfEdges(E)266  requires edge : e ∈ E267  shows expandedRight(E, σ)((0, e)) = (e, 1)268proof269  exact FunctionBetween.apply_value with (expandedRight.function with function),270    (spokes.edge with edge), (expandedRight.spoke_relates with edge)271272theorem expandedLeft.ring (E σ h : Set)273  requires end : h ∈ halfEdges(E)274  shows expandedLeft(E, σ)((1, h)) = h275proof276  exact FunctionBetween.apply_value with expandedLeft.function,277    (rings.edge with end), (expandedLeft.ring_relates with end)278279theorem expandedRight.ring (E σ h : Set)280  requires function : σ : halfEdges(E) → halfEdges(E)281  requires end : h ∈ halfEdges(E)282  shows expandedRight(E, σ)((1, h)) = σ(h)283proof284  exact FunctionBetween.apply_value with (expandedRight.function with function),285    (rings.edge with end), (expandedRight.ring_relates with function, end)286287-- Section: The ends of the expansion.288289-- The spoke end at h = (e, i) is side i of the spoke of e.290theorem spokes.ends (E σ e i : Set)291  requires function : σ : halfEdges(E) → halfEdges(E)292  requires edge : e ∈ E293  requires side : i ∈ 2294  shows incidentEnds(expandedLeft(E, σ), expandedRight(E, σ), spokes(E),295    (e, i)) = {((0, e), i)}296proof297  ext p298  constructor299  . intro hp300    obtain ⟨x, hx, j, hj, rfl⟩ := incidentEnds.shape with hp301    have ending := (incidentEnds.pair.forward with hp).right302    unfold spokes at hx303    obtain ⟨_, z, hz, f, hf, rfl⟩ := product.membership.forward with hx304    simp at hz305    rw hz at ending306    rw hz307    rw [(expandedLeft.spoke with hf), (expandedRight.spoke with function, hf)]308      at ending309    rcases ending with ⟨rfl, same⟩ | ⟨rfl, same⟩310    . obtain ⟨rfl, rfl⟩ := orderedPair.injective with same311      simp312    . obtain ⟨rfl, rfl⟩ := orderedPair.injective with same313      simp314  . intro hp315    simp at hp316    rw hp317    have spoke := spokes.member with edge318    have sides := membership.two.forward with side319    rcases sides with rfl | rfl320    . simp [incidentEnds.pair, spoke,321        (expandedLeft.spoke at E, σ, e with edge)]322    . simp [incidentEnds.pair, spoke, (expandedRight.spoke with function, edge)]323324-- The ring ends at h = (e, i): the left end of its own ring edge and the325-- right end of the ring edge of the end σ carries to h.326theorem rings.ends (E σ e i : Set)327  requires bijective : BijectiveBetween(σ, halfEdges(E), halfEdges(E))328  requires edge : e ∈ E329  requires side : i ∈ 2330  shows incidentEnds(expandedLeft(E, σ), expandedRight(E, σ), rings(E),331      (e, i)) =332    {((1, (e, i)), 0),333      ((1, converse(σ, halfEdges(E), halfEdges(E))((e, i))), 1)}334proof335  have function := Injective.function with (Bijective.injective with bijective)336  have end : (e, i) ∈ halfEdges(E) :=337    halfEdges.pair.backward with ⟨edge, side⟩338  have inverse := converse.function_of_bijective with bijective339  have preimage := FunctionBetween.apply_closed with inverse, end340  have back := Bijective.apply_inverse with bijective, end341  ext p342  constructor343  . intro hp344    obtain ⟨x, hx, j, hj, rfl⟩ := incidentEnds.shape with hp345    have ending := (incidentEnds.pair.forward with hp).right346    unfold rings at hx347    obtain ⟨_, z, hz, k, hk, rfl⟩ := product.membership.forward with hx348    simp at hz349    rw hz at ending350    rw hz351    rw [(expandedLeft.ring with hk), (expandedRight.ring with function, hk)]352      at ending353    rcases ending with ⟨rfl, rfl⟩ | ⟨rfl, same⟩354    . simp355    . have forward := Bijective.inverse_apply with bijective, hk356      rw same at forward357      rw ← forward358      simp359  . intro hp360    simp at hp361    rcases hp with rfl | rfl362    . simp [incidentEnds.pair, (rings.member with end),363        (expandedLeft.ring at E, σ, (e, i) with end)]364    . simp [incidentEnds.pair, (rings.member with preimage),365        (expandedRight.ring with function, preimage), back]366367-- Each end meets one spoke and two ring edges.368theorem spokes.degree (E σ e i : Set)369  requires function : σ : halfEdges(E) → halfEdges(E)370  requires edge : e ∈ E371  requires side : i ∈ 2372  shows degreeIn(expandedLeft(E, σ), expandedRight(E, σ), spokes(E),373    (e, i)) = 1374proof375  unfold degreeIn376  rw spokes.ends with function, edge, side377  exact cardinality.singleton378379theorem rings.degree (E σ e i : Set)380  requires bijective : BijectiveBetween(σ, halfEdges(E), halfEdges(E))381  requires edge : e ∈ E382  requires side : i ∈ 2383  shows degreeIn(expandedLeft(E, σ), expandedRight(E, σ), rings(E),384    (e, i)) = 2385proof386  have fresh : ((1, converse(σ, halfEdges(E), halfEdges(E))((e, i))), 1) ∉387      {((1, (e, i)), 0)}388    intro same389    simp at same390  unfold degreeIn391  rw [(rings.ends with bijective, edge, side), pair.eq_union2,392    (cardinality.union_disjoint with Finite.singleton, Finite.singleton,393      (Disjoint.singleton_of_fresh with fresh)),394    cardinality.singleton, cardinality.singleton]395  compute396397-- The ring edges form an even edge set of the expansion.398theorem rings.even (E σ : Set)399  requires finiteEdges : Finite(E)400  requires bijective : BijectiveBetween(σ, halfEdges(E), halfEdges(E))401  shows EvenEdgeSet(halfEdges(E), expandedLeft(E, σ), expandedRight(E, σ),402    rings(E))403proof404  constructor405  . exact rings.finite with finiteEdges406  . intros h hh407    obtain ⟨e, he, i, hi, rfl⟩ := halfEdges.shape with hh408    rw rings.degree with bijective, he, hi409    exact Even.two410411-- With every degree at least two the expansion is cubic and loopless: each412-- end meets its spoke and two ring edges, a spoke joins the two distinct413-- ends of its edge, and a ring edge joins an end to a different end.414theorem expansion.cubic (V E leftEnd rightEnd σ : Set)415  requires graph : Graph(V, E, leftEnd, rightEnd)416  requires finiteEdges : Finite(E)417  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)418  requires degrees : ∀ v ∈ V, 2 ≤ degreeIn(leftEnd, rightEnd, E, v)419  shows Cubic(halfEdges(E), expandedEdges(E),420    expandedLeft(E, σ), expandedRight(E, σ))421proof422  have function := RotationSystem.function with rotation423  constructor424  . intros h hh425    obtain ⟨e, he, i, hi, rfl⟩ := halfEdges.shape with hh426    unfold expandedEdges427    rw [(degreeIn.union_disjoint with (spokes.finite with finiteEdges),428        (rings.finite with finiteEdges), expandedEdges.apart),429      (spokes.degree with function, he, hi),430      (rings.degree with rotation.left, he, hi)]431    compute432  . intros x hx433    have split := expandedEdges.cases with hx434    rcases split with ⟨e, he, rfl⟩ | ⟨h, hh, rfl⟩435    . rw [(expandedLeft.spoke with he), (expandedRight.spoke with function, he)]436      intro same437      have sides := (orderedPair.injective with same).right438      contradiction439    . rw [(expandedLeft.ring with hh), (expandedRight.ring with function, hh)]440      have moves := RotationSystem.moves441        with graph, finiteEdges, rotation, degrees, hh442      cc443