Rotation systems of listed multigraphs

A dart is an edge-list position and one of its two ends. Loops retain two different darts; parallel edges retain their different list positions. A rotation permutes darts in one cycle at each incident vertex. This extra structure retains argument order when the graph comes from CSP incidences. It does not impose a degree bound.

The face successor reverses an edge and then takes the inverse vertex rotation. Faces are all its orbits, including singleton orbits. Isolated declared vertices have no darts and are not represented by this face quotient. No genus-zero condition, geometric realization or planarity recognition theorem is asserted here.

Main definitions

• Cslib.Complexity.Graph.Dart: indexed ends of listed edges.
• Cslib.Complexity.Graph.RotationSystem: one rotation cycle per nonempty vertex fiber.
• Cslib.Complexity.Graph.RotationSystem.faceNext: the face successor permutation.
• Cslib.Complexity.Graph.RotationSystem.Face: face orbits, including fixed points.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.Dart (G : Graph) : Type

A listed edge occurrence together with a choice of endpoint.

def Cslib.Complexity.Graph.Dart.vertex {G : Graph} (d : G.Dart) : ℕ

The endpoint of an indexed edge end; false selects the first endpoint.

def Cslib.Complexity.Graph.Dart.reverse {G : Graph} (d : G.Dart) : G.Dart

Reverse an edge while retaining its edge-list occurrence.

@[simp]

theorem Cslib.Complexity.Graph.Dart.reverse_reverse {G : Graph} (d : G.Dart) : d.reverse.reverse = d

Reversing twice returns the same indexed end.

theorem Cslib.Complexity.Graph.Dart.reverse_ne {G : Graph} (d : G.Dart) : d.reverse ≠ d

Even a loop has two distinct indexed ends.

def Cslib.Complexity.Graph.Dart.reversal (G : Graph) : Equiv.Perm G.Dart

Edge reversal as a permutation of all indexed ends.

theorem Cslib.Complexity.Graph.Dart.card (G : Graph) : Fintype.card G.Dart = 2 * G.edges.length

There are two darts per listed edge, counting loops and parallel occurrences.

structure Cslib.Complexity.Graph.RotationSystem (G : Graph) : Type

A cyclic order of the darts at each incident vertex. No cyclic start point is chosen.

• rotate : Equiv.Perm G.Dart

  One successor permutation on all darts.

• sameCycle_iff (d e : G.Dart) : self.rotate.SameCycle d e ↔ d.vertex = e.vertex

  Its orbits are exactly the nonempty endpoint fibers.

theorem Cslib.Complexity.Graph.RotationSystem.vertex_rotate {G : Graph} (r : G.RotationSystem) (d : G.Dart) : (r.rotate d).vertex = d.vertex

Rotating around a vertex keeps that endpoint.

def Cslib.Complexity.Graph.RotationSystem.faceNext {G : Graph} (r : G.RotationSystem) : Equiv.Perm G.Dart

Reverse an edge, then turn backwards around its new endpoint.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.RotationSystem.Face {G : Graph} (r : G.RotationSystem) : Type

All face orbits, including the singleton orbits omitted by nontrivial cycle factors.

theorem Cslib.Complexity.Graph.RotationSystem.face_eq_next {G : Graph} (r : G.RotationSystem) (d : G.Dart) : ⟦r.faceNext d⟧ = ⟦d⟧

A dart and its face successor lie in the same face orbit.

def Cslib.Complexity.Graph.RotationSystem.mirror {G : Graph} (r : G.RotationSystem) : G.RotationSystem

Reverse every vertex rotation, corresponding to reversal of the global orientation.