Rotations and actual components of disjoint listed graphs

The successor is the disjoint sum of the two original rotations in exact edge/end coordinates. Its components are precisely the original components in their tagged blocks. All declared points, loops and parallel indexed edges are retained.

def Cslib.Complexity.Graph.RotationSystem.disjointUnion {G H : Graph} (r : G.RotationSystem) (s : H.RotationSystem) : (G.disjointUnion H).RotationSystem

The disjoint sum of source rotations, retaining both original directed cycles.

theorem Cslib.Complexity.Graph.RotationSystem.rotate_disjointUnion {G H : Graph} (r : G.RotationSystem) (s : H.RotationSystem) (d : G.Dart ⊕ H.Dart) : (r.disjointUnion s).rotate ((G.disjointDartEquiv H) d) = (G.disjointDartEquiv H) (Sum.map (⇑r.rotate) (⇑s.rotate) d)

Exact forward successors in disjoint edge/end coordinates.

theorem Cslib.Complexity.Graph.RotationSystem.faceNext_disjointUnion {G H : Graph} (r : G.RotationSystem) (s : H.RotationSystem) (d : G.Dart ⊕ H.Dart) : (r.disjointUnion s).faceNext ((G.disjointDartEquiv H) d) = (G.disjointDartEquiv H) (Sum.map (⇑r.faceNext) (⇑s.faceNext) d)

The corresponding inverse-rotation face successor has the same source-block chirality.

theorem Cslib.Complexity.Graph.RotationSystem.sameComponent_disjointUnion_iff {G H : Graph} (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hH : ∀ v ∈ H.incidenceVertices, v ∈ H.vertices) (a b : G.Dart ⊕ H.Dart) : RotationCertificate.SameComponent (G.disjointUnion H) ((G.disjointDartEquiv H) a).vertex ((G.disjointDartEquiv H) b).vertex ↔ match a, b with | Sum.inl a, Sum.inl b => RotationCertificate.SameComponent G a.vertex b.vertex | Sum.inr a, Sum.inr b => RotationCertificate.SameComponent H a.vertex b.vertex | x, x_1 => False

Two actual disjoint-union darts are connected exactly when they come from the same block and were connected in that source graph. Point components are not represented as darts.