Edge components of indexed rotations

The source and actual indexed dual have the same edge components on identified darts. Vertex and edge-reversal invariants connect the permutation generators to the existing graph reachability relation. Loops and parallel positions are retained; isolated source points have no darts in this correspondence.

Main results

• Cslib.Complexity.Graph.RotationSystem.sameComponent_dual_iff: exact edge components.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_dual_iff {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d e : G.Dart) : RotationCertificate.SameComponent r.dualGraph (r.dualDartEquiv d).vertex (r.dualDartEquiv e).vertex ↔ RotationCertificate.SameComponent G d.vertex e.vertex

Dual and source edge components agree on the same indexed darts. Isolated source points are excluded automatically, since this correspondence is stated at darts.