Grace/Cumulus/GraphTheory/DoubleCover/RotationSystems.g17

Open in Workbench Download source

Imports

Cycles · Multigraph.Cuts · Nat.CyclicShift

Declarations

Source

1-- Rotation systems: a permutation of the edge ends carrying each end to2-- another end at the same vertex, whose orbit through an end is all the ends3-- there. Every finite multigraph has one, by a cyclic permutation of the4-- ends at each vertex.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.RotationSystems11import Cycles12import Multigraph.Cuts13import Nat.CyclicShift1415-- Section: Rotation systems.1617-- The ends of the edges: (e, 0) is the left end of e and (e, 1) its right18-- end. The ends at a vertex v are incidentEnds(leftEnd, rightEnd, E, v).19def halfEdges (E : Set) : Set := E × 22021-- The n-th iterate of σ at h.22def orbitStep (σ h : Set, n : Nat) → Set23  | σ, h, zero => h24  | σ, h, succ(m) => σ(orbitStep(σ, h, m))2526-- A rotation system: a permutation of the ends carrying each end to another27-- end at the same vertex, whose orbit through an end is all the ends there.28predicate RotationSystem (V E leftEnd rightEnd σ : Set) :=29  BijectiveBetween(σ, halfEdges(E), halfEdges(E)) ∧30  (∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),31    σ(h) ∈ incidentEnds(leftEnd, rightEnd, E, v)) ∧32  (∀ v ∈ V, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),33    ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v),34    ∃ n ∈ ℕ, orbitStep(σ, h, n) = k)3536-- Iterates compose: the (m + k)-th iterate is the k-th iterate of the m-th.37theorem orbitStep.add (σ h : Set, m k : Nat)38  shows orbitStep(σ, h, m + k) = orbitStep(σ, orbitStep(σ, h, m), k)39proof40  induction k41  | zero => rw [add.right_unit, orbitStep]42  | succ(j) using ih => rw [add.succ_right, orbitStep, orbitStep, ih]4344-- The orbit of a point of a set closed under σ stays in the set.45theorem orbitStep.closed (σ h X : Set, n : Nat)46  requires closed : ∀ x ∈ X, σ(x) ∈ X47  requires start : h ∈ X48  shows orbitStep(σ, h, n) ∈ X49proof50  induction n51  | zero => rwa orbitStep52  | succ(m) using ih =>53    rw orbitStep54    exact closed with orbitStep(σ, h, m), ih5556-- A fixed point of σ has a one-point orbit.57theorem orbitStep.fixed (σ h : Set, n : Nat)58  requires fixed : σ(h) = h59  shows orbitStep(σ, h, n) = h60proof61  induction n62  | zero => rw orbitStep63  | succ(m) using ih => rw [orbitStep, ih, fixed]6465-- Two maps agreeing on a set closed under one of them have the same orbits66-- through its points.67theorem orbitStep.agree (σ τ h X : Set, n : Nat)68  requires same : ∀ x ∈ X, τ(x) = σ(x)69  requires closed : ∀ x ∈ X, σ(x) ∈ X70  requires start : h ∈ X71  shows orbitStep(τ, h, n) = orbitStep(σ, h, n)72proof73  induction n74  | zero => rw [orbitStep, orbitStep]75  | succ(m) using ih =>76    have reached := orbitStep.closed at σ, h, X, m with closed, start77    rw [orbitStep, orbitStep, ih]78    exact same with orbitStep(σ, h, m), reached7980theorem halfEdges.pair (E e i : Set)81  shows (e, i) ∈ halfEdges(E) ↔ e ∈ E ∧ i ∈ 282proof83  unfold halfEdges84  exact product.pair_membership8586theorem halfEdges.shape (E h : Set)87  requires end : h ∈ halfEdges(E)88  shows ∃ e ∈ E, ∃ i ∈ 2, h = (e, i)89proof90  unfold halfEdges at end91  exact (product.membership.forward with end).right9293-- The two ends of an edge.94theorem halfEdges.left (E e : Set)95  requires edge : e ∈ E96  shows (e, 0) ∈ halfEdges(E)97proof98  have zero : 0 ∈ 2 by typecheck99  exact halfEdges.pair.backward with ⟨edge, zero⟩100101theorem halfEdges.right (E e : Set)102  requires edge : e ∈ E103  shows (e, 1) ∈ halfEdges(E)104proof105  have one : 1 ∈ 2 by typecheck106  exact halfEdges.pair.backward with ⟨edge, one⟩107108theorem halfEdges.finite (E : Set)109  requires finiteEdges : Finite(E)110  shows Finite(halfEdges(E))111proof112  unfold halfEdges113  exact Finite.product with finiteEdges, Finite.natural114115theorem incidentEnds.subset_halfEdges (leftEnd rightEnd E v : Set)116  shows incidentEnds(leftEnd, rightEnd, E, v) ⊆ halfEdges(E)117proof118  unfold halfEdges119  exact incidentEnds.subset_product120121-- The left end of e lies at leftEnd(e), the right end at rightEnd(e).122theorem incidentEnds.left (leftEnd rightEnd E v e : Set)123  requires edge : e ∈ E124  shows (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, v) ↔ leftEnd(e) = v125proof126  simp [incidentEnds.pair, edge]127128theorem incidentEnds.right (leftEnd rightEnd E v e : Set)129  requires edge : e ∈ E130  shows (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, v) ↔ rightEnd(e) = v131proof132  simp [incidentEnds.pair, edge]133134-- Every end lies at a vertex of the graph, and at one vertex only.135theorem halfEdges.vertex (V E leftEnd rightEnd h : Set)136  requires graph : Graph(V, E, leftEnd, rightEnd)137  requires end : h ∈ halfEdges(E)138  shows ∃ v ∈ V, h ∈ incidentEnds(leftEnd, rightEnd, E, v)139proof140  obtain ⟨e, he, i, hi, rfl⟩ := halfEdges.shape with end141  have ends := Graph.ends with graph, e, he142  have sides := membership.two.forward with hi143  rcases sides with rfl | rfl144  . refine ⟨leftEnd(e), ends.left, _⟩145    simp [incidentEnds.pair, he]146  . refine ⟨rightEnd(e), ends.right, _⟩147    simp [incidentEnds.pair, he]148149theorem incidentEnds.same_vertex (leftEnd rightEnd E v w p : Set)150  requires atV : p ∈ incidentEnds(leftEnd, rightEnd, E, v)151  requires atW : p ∈ incidentEnds(leftEnd, rightEnd, E, w)152  shows v = w153proof154  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with atV155  have sides := (incidentEnds.pair.forward with atV).right156  rcases sides with ⟨rfl, hv⟩ | ⟨rfl, hv⟩157  . rw (incidentEnds.left with he) at atW158    cc159  . rw (incidentEnds.right with he) at atW160    cc161162theorem RotationSystem.function (V E leftEnd rightEnd σ : Set)163  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)164  shows σ : halfEdges(E) → halfEdges(E)165proof166  exact rotation.left.left.left167168-- σ carries the ends at v to ends at v, and no other end to one.169theorem RotationSystem.at_vertex (V E leftEnd rightEnd σ v h : Set)170  requires graph : Graph(V, E, leftEnd, rightEnd)171  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)172  requires vertex : v ∈ V173  requires end : h ∈ halfEdges(E)174  shows h ∈ incidentEnds(leftEnd, rightEnd, E, v) ↔175    σ(h) ∈ incidentEnds(leftEnd, rightEnd, E, v)176proof177  constructor178  . intro atV179    exact rotation.right.left with v, vertex, h, atV180  . intro imageAtV181    obtain ⟨w, hw, atW⟩ := halfEdges.vertex with graph, end182    have imageAtW := rotation.right.left with w, hw, h, atW183    rw (incidentEnds.same_vertex with imageAtV, imageAtW)184    exact atW185186-- With at least two ends at every vertex, σ fixes no end: the orbit of a187-- fixed end is a single point, but it must reach the other end at its vertex.188theorem RotationSystem.moves (V E leftEnd rightEnd σ h : Set)189  requires graph : Graph(V, E, leftEnd, rightEnd)190  requires finiteEdges : Finite(E)191  requires rotation : RotationSystem(V, E, leftEnd, rightEnd, σ)192  requires degrees : ∀ v ∈ V, 2 ≤ degreeIn(leftEnd, rightEnd, E, v)193  requires end : h ∈ halfEdges(E)194  shows σ(h) ≠ h195proof196  intro fixed197  obtain ⟨v, hv, atV⟩ := halfEdges.vertex with graph, end198  have finiteEnds := incidentEnds.finite at leftEnd, rightEnd, E, v199    with finiteEdges200  have another : incidentEnds(leftEnd, rightEnd, E, v) ∖ {h} ≠ ∅201    intro empty202    have count := cardinality.remove_add_one with finiteEnds, atV203    have bound := degrees with v, hv204    unfold degreeIn at bound205    rw [empty, cardinality.empty] at count206    arith207  obtain ⟨k, hk⟩ := Nonempty.of_ne_empty with another208  obtain ⟨atVk, different⟩ := hk209  obtain ⟨n, hn, reaches⟩ :=210    rotation.right.right with v, hv, h, atV, k, atVk211  rw orbitStep.fixed with fixed at reaches212  simp [reaches] at different213214-- Section: Existence of rotation systems.215216-- The orbit of i under the cyclic shift of n counts up while it stays in n.217theorem rotation.orbit_below (n : Nat, i k : Nat)218  requires inside : i + k ∈ n219  shows orbitStep(rotation(n), i, k) = i + k220proof221  induction k222  | zero =>223    intro inside224    rw [orbitStep, add.right_unit]225  | succ(j) using ih =>226    intro inside227    rw add.succ_right at inside228    have earlier : i + j ∈ n229      have below := Less.of_membership with inside230      have lower : i + j < n by arith231      exact membership.of_Less with lower232    rw [orbitStep, (ih with earlier), add.succ_right]233    exact rotation.step with earlier, inside234235-- Every member of n is reached from every other: climb from i to n − 1,236-- wrap to 0, and climb to j.237theorem rotation.orbit (n : Nat, i j : Set)238  requires hi : i ∈ n239  requires hj : j ∈ n240  shows ∃ m ∈ ℕ, orbitStep(rotation(n), i, m) = j241proof242  have iNat := natural.member at n with hi243  have jNat := natural.member at n with hj244  have below := Less.of_membership with hi245  obtain ⟨d, dNat, split⟩ := Less.exists_add_one with below246  have top : succ(i + d) = n247    rw split248    ring249  have topIn : i + d ∈ n250    have lower : i + d < n by arith251    exact membership.of_Less with lower252  have toZero : orbitStep(rotation(n), i, succ(d)) = 0253    rw [orbitStep, (rotation.orbit_below with topIn)]254    exact rotation.wrap with topIn, top255  have fromZero : orbitStep(rotation(n), 0, j) = j256    have start : 0 + j ∈ n257      rw add.left_unit258      exact hj259    rw rotation.orbit_below with start260    exact add.left_unit261  refine ⟨succ(d) + j, _, _⟩262  . typecheck263  . rw [orbitStep.add, toZero, fromZero]264265-- Conjugating the shift by an enumeration f : A → n: the orbit of a under266-- f⁻¹ ∘ ρ ∘ f is the orbit of f(a) under ρ, carried back by f⁻¹.267def conjugated (f ρ A n : Set) : Set :=268  compose(converse(f, A, n), compose(ρ, f, A, n, n), A, n, A)269270theorem conjugated.bijective (f ρ A n : Set)271  requires enumeration : BijectiveBetween(f, A, n)272  requires shift : BijectiveBetween(ρ, n, n)273  shows BijectiveBetween(conjugated(f, ρ, A, n), A, A)274proof275  unfold conjugated276  exact compose.bijective with (compose.bijective with enumeration, shift),277    (converse.bijective with enumeration)278279theorem conjugated.apply (f ρ A n a : Set)280  requires enumeration : BijectiveBetween(f, A, n)281  requires shift : BijectiveBetween(ρ, n, n)282  requires member : a ∈ A283  shows conjugated(f, ρ, A, n)(a) = converse(f, A, n)(ρ(f(a)))284proof285  have fFunction :=286    Injective.function with (Bijective.injective with enumeration)287  have ρFunction := Injective.function with (Bijective.injective with shift)288  have inner := Injective.function289    with (Bijective.injective with (compose.bijective with enumeration, shift))290  have inverse := converse.function_of_bijective with enumeration291  unfold conjugated292  rw [(compose.apply with inner, inverse, member),293    (compose.apply with fFunction, ρFunction, member)]294295theorem conjugated.orbit (f ρ A n a : Set, m : Nat)296  requires enumeration : BijectiveBetween(f, A, n)297  requires shift : BijectiveBetween(ρ, n, n)298  requires member : a ∈ A299  shows orbitStep(conjugated(f, ρ, A, n), a, m) =300    converse(f, A, n)(orbitStep(ρ, f(a), m))301proof302  induction m303  | zero =>304    rw [orbitStep, orbitStep]305    symm306    exact Bijective.inverse_apply with enumeration, member307  | succ(k) using ih =>308    have fFunction :=309      Injective.function with (Bijective.injective with enumeration)310    have ρFunction := Injective.function with (Bijective.injective with shift)311    have closed : ∀ x ∈ n, ρ(x) ∈ n312      intros x hx313      exact FunctionBetween.apply_closed with ρFunction, hx314    have start := FunctionBetween.apply_closed with fFunction, member315    have reached := orbitStep.closed at ρ, f(a), n, k with closed, start316    have inverse := converse.function_of_bijective with enumeration317    have back := FunctionBetween.apply_closed with inverse, reached318    rw [orbitStep, ih, (conjugated.apply with enumeration, shift, back),319      (Bijective.apply_inverse with enumeration, reached), orbitStep]320321-- Every finite set has a cyclic permutation: enumerate it by its cardinality322-- and conjugate the cyclic shift.323theorem cyclicPermutation.exists (A : Set)324  requires finite : Finite(A)325  shows ∃ σ, BijectiveBetween(σ, A, A) ∧326    (∀ a ∈ A, ∀ b ∈ A, ∃ n ∈ ℕ, orbitStep(σ, a, n) = b)327proof328  obtain ⟨nNat, f, enumeration⟩ := cardinality.correct with finite329  have shift := rotation.bijective at cardinality(A) with nNat330  have fFunction :=331    Injective.function with (Bijective.injective with enumeration)332  refine ⟨conjugated(f, rotation(cardinality(A)), A, cardinality(A)),333    (conjugated.bijective with enumeration, shift), _⟩334  intros a ha b hb335  have ia := FunctionBetween.apply_closed with fFunction, ha336  have ib := FunctionBetween.apply_closed with fFunction, hb337  obtain ⟨m, hm, reaches⟩ := rotation.orbit with nNat, ia, ib338  refine ⟨m, hm, _⟩339  rw [(conjugated.orbit with enumeration, shift, ha), reaches]340  exact Bijective.inverse_apply with enumeration, hb341342-- The ends at the vertices of W.343def endsAt (leftEnd rightEnd E W : Set) : Set :=344  { h ∈ halfEdges(E) |345    ∃ v ∈ W, h ∈ incidentEnds(leftEnd, rightEnd, E, v) }346347theorem endsAt.of_vertex (leftEnd rightEnd E W v h : Set)348  requires vertex : v ∈ W349  requires end : h ∈ incidentEnds(leftEnd, rightEnd, E, v)350  shows h ∈ endsAt(leftEnd, rightEnd, E, W)351proof352  have inside := incidentEnds.subset_halfEdges at leftEnd, rightEnd, E, v353  exact ⟨(inside with h, end), v, vertex, end⟩354355theorem endsAt.empty (leftEnd rightEnd E : Set)356  shows endsAt(leftEnd, rightEnd, E, ∅) = ∅357proof358  ext h359  simp [endsAt]360361-- Adding a vertex adds its ends, and the ends at a vertex outside W lie at362-- no vertex of W.363theorem endsAt.insert (leftEnd rightEnd E W a : Set)364  shows endsAt(leftEnd, rightEnd, E, W ∪ {a}) =365    endsAt(leftEnd, rightEnd, E, W) ∪ incidentEnds(leftEnd, rightEnd, E, a)366proof367  ext h368  constructor369  . intro hh370    obtain ⟨inEnds, v, hv, atV⟩ := hh371    simp at hv372    apply union2.membership.backward373    rcases hv with inW | rfl374    . left375      exact ⟨inEnds, v, inW, atV⟩376    . right377      exact atV378  . intro hh379    have split := union2.membership.forward with hh380    rcases split with inW | atA381    . obtain ⟨inEnds, v, hv, atV⟩ := inW382      refine ⟨inEnds, v, _, atV⟩383      simp [hv]384    . have inside := incidentEnds.subset_halfEdges at leftEnd, rightEnd, E, a385      refine ⟨(inside with h, atA), a, _, atA⟩386      simp387388theorem endsAt.disjoint (leftEnd rightEnd E W a : Set)389  requires fresh : a ∉ W390  shows Disjoint(endsAt(leftEnd, rightEnd, E, W),391    incidentEnds(leftEnd, rightEnd, E, a))392proof393  apply Disjoint.iff.backward394  intros h hh atA395  obtain ⟨_, v, hv, atV⟩ := hh396  rw (incidentEnds.same_vertex with atV, atA) at hv397  exact fresh with hv398399-- Every end lies at a vertex of the graph.400theorem endsAt.all (V E leftEnd rightEnd : Set)401  requires graph : Graph(V, E, leftEnd, rightEnd)402  shows endsAt(leftEnd, rightEnd, E, V) = halfEdges(E)403proof404  ext h405  constructor406  . intro hh407    exact hh.left408  . intro hh409    obtain ⟨v, hv, atV⟩ := halfEdges.vertex with graph, hh410    exact ⟨hh, v, hv, atV⟩411412-- A rotation system on the ends at the vertices of a finite set W: a cyclic413-- permutation of the ends at each vertex, glued over W.414theorem RotationSystem.exists_on (E leftEnd rightEnd W : Set)415  requires finiteEdges : Finite(E)416  requires finiteVertices : Finite(W)417  shows ∃ σ, BijectiveBetween(σ, endsAt(leftEnd, rightEnd, E, W),418      endsAt(leftEnd, rightEnd, E, W)) ∧419    (∀ v ∈ W, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),420      σ(h) ∈ incidentEnds(leftEnd, rightEnd, E, v)) ∧421    (∀ v ∈ W, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),422      ∀ k ∈ incidentEnds(leftEnd, rightEnd, E, v),423      ∃ n ∈ ℕ, orbitStep(σ, h, n) = k)424proof425  induction finiteVertices with G a426  | empty =>427    obtain ⟨σ, bijective, _⟩ := cyclicPermutation.exists with Finite.empty428    refine ⟨σ, _, _, _⟩429    . rw endsAt.empty430      exact bijective431    . intros v hv432      simp at hv433    . intros v hv434      simp at hv435  | insert using ih =>436    obtain ⟨σ, bijective, closed, orbits⟩ := ih437    obtain ⟨τ, cyclic, orbitsA⟩ := cyclicPermutation.exists438      with (incidentEnds.finite at leftEnd, rightEnd, E, a with finiteEdges)439    have σFunction :=440      Injective.function with (Bijective.injective with bijective)441    have τFunction := Injective.function with (Bijective.injective with cyclic)442    have apart := endsAt.disjoint at leftEnd, rightEnd, E, G, a with aFresh443    -- On the ends at a vertex of G the glued map acts as σ, at a as τ.444    have onOld : ∀ v ∈ G, ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, v),445        (σ ∪ τ)(h) = σ(h)446      intros v hv h hh447      exact FunctionBetween.union_apply_left448        with σFunction, τFunction, apart, (endsAt.of_vertex with hv, hh)449    have onNew : ∀ h ∈ incidentEnds(leftEnd, rightEnd, E, a),450        (σ ∪ τ)(h) = τ(h)451      intros h hh452      exact FunctionBetween.union_apply_right453        with σFunction, τFunction, apart, hh454    have closedA : ∀ x ∈ incidentEnds(leftEnd, rightEnd, E, a),455        τ(x) ∈ incidentEnds(leftEnd, rightEnd, E, a)456      intros x hx457      exact FunctionBetween.apply_closed with τFunction, hx458    refine ⟨σ ∪ τ, _, _, _⟩459    . rw endsAt.insert460      exact Bijective.union_disjoint with bijective, cyclic, apart, apart461    . intros v hv h hh462      simp at hv463      rcases hv with inG | rfl464      . rw onOld with v, inG, h, hh465        exact closed with v, inG, h, hh466      . rw onNew with h, hh467        exact closedA with h, hh468    . intros v hv h hh k hk469      simp at hv470      rcases hv with inG | rfl471      . obtain ⟨n, hn, reaches⟩ := orbits with v, inG, h, hh, k, hk472        refine ⟨n, hn, _⟩473        rw ← reaches474        exact orbitStep.agree with (onOld with v, inG), (closed with v, inG), hh475      . obtain ⟨n, hn, reaches⟩ := orbitsA with h, hh, k, hk476        refine ⟨n, hn, _⟩477        rw ← reaches478        exact orbitStep.agree with onNew, closedA, hh479480theorem RotationSystem.exists (V E leftEnd rightEnd : Set)481  requires graph : Graph(V, E, leftEnd, rightEnd)482  requires finiteVertices : Finite(V)483  requires finiteEdges : Finite(E)484  shows ∃ σ, RotationSystem(V, E, leftEnd, rightEnd, σ)485proof486  obtain ⟨σ, bijective, closed, orbits⟩ :=487    RotationSystem.exists_on at E, leftEnd, rightEnd, V488      with finiteEdges, finiteVertices489  rw endsAt.all with graph at bijective490  refine ⟨σ, _⟩491  exact ⟨bijective, closed, orbits⟩492