Faces and planarity of PD-codes

A TauCeti.PDCode lists the four half-edges at each crossing in counterclockwise order and pairs the two ends of each arc, but nothing in the code forces these data to come from a diagram drawn in the plane. This file supplies the face data that decides it. The half-edges of a code are the darts of its underlying 4-valent graph, the counterclockwise rotation of the slots at each crossing (TauCeti.PDCode.crossingRotation) is its rotation system, and the arc matching is its edge involution. As for any rotation system, the orbits of the composite TauCeti.PDCode.facePerm, which turns to the next slot counterclockwise and then runs along the arc from there, are the faces of the closed oriented surface on which the graph is cellularly embedded (Lando–Zvonkin, §1.3). For a connected diagram in the plane they are the regions of the diagram.

This is the permutation-triple encoding of the graph: TauCeti.PDCode.toPermutationTriple has the crossing rotation and the arc matching as its first two components and the inverse face permutation as the third. Its Euler characteristic counts n vertices, 2 * n edges and the faces, so it is faceCount - n (TauCeti.PDCode.eulerChar_toPermutationTriple). Each connected component of the graph contributes at most 2, with equality exactly for a sphere, so a code is planar (TauCeti.PDCode.IsPlanar) when the Euler characteristic is twice the number of connected components, the monodromy orbits of the triple. For a connected code this is Euler's count of n + 2 regions (TauCeti.PDCode.isPlanar_iff_faceCount_eq_of_isConnected).

Throughout, the underlying graph is the one supported on the crossings: its vertices are the crossings and its edges the arcs between them. The crossing-free circles of a code (TauCeti.PDCode.crossinglessComponentCount) are not part of it, so they contribute neither faces to TauCeti.PDCode.faceCount nor connected components to the monodromy orbits. They play no part in planarity either, since a circle alone always lies in a sphere.

Planarity is invariant under mirroring and relabelling. The one-crossing kink is planar, while the one-crossing code whose arcs join opposite slots, two circles meeting in a single crossing, is not (TauCeti.PDCode.exists_not_isPlanar): its graph embeds only in the torus.

The face permutation locates the arcs that border a common region: two half-edges lie on the same face exactly when TauCeti.PDCode.face agrees on them (TauCeti.PDCode.face_eq_face_iff). This is the locality data that the second and third Reidemeister moves need beyond the algebraic operation TauCeti.PDCode.insertClasp.

Main definitions

• TauCeti.PDCode.crossingRotation: the counterclockwise rotation of the slots at each crossing.
• TauCeti.PDCode.toPermutationTriple: the permutation triple of the underlying graph.
• TauCeti.PDCode.facePerm and TauCeti.PDCode.faceCount: the face traversal and the number of faces of the underlying graph.
• TauCeti.PDCode.Face and TauCeti.PDCode.face: the faces, as orbits of the face traversal, and the face at a half-edge.
• TauCeti.PDCode.IsPlanar: every connected component of the underlying graph is a sphere.

Main results

• TauCeti.PDCode.eulerChar_toPermutationTriple: the Euler characteristic is faceCount - n.
• TauCeti.PDCode.faceCount_le: if the underlying graph has c connected components, it has at most n + 2 * c faces, with equality exactly for planar codes (TauCeti.PDCode.isPlanar_iff_faceCount_eq).
• TauCeti.PDCode.mem_orbit_of_face_eq_face: half-edges on one face lie in one connected component, and so does a half-edge h with every half-edge on the face at the far end D.edgePair.val h of its arc (TauCeti.PDCode.mem_orbit_of_face_edgePair_eq_face).
• TauCeti.PDCode.isPlanar_mirror and TauCeti.PDCode.isPlanar_relabel: invariance.
• TauCeti.PDCode.isPlanar_kink and TauCeti.PDCode.exists_not_isPlanar.

References

• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.3 (rotation systems and their faces) and §1.5.
• M. Mastin, Links and Planar Diagram Codes, Definitions 2--3 (the PD convention).

The crossing rotation

def TauCeti.PDCode.crossingRotation {n : ℕ} (D : PDCode n) : Equiv.Perm (Fin (4 * n))

The rotation of every half-edge to the next slot counterclockwise at its crossing.

Equations

• D.crossingRotation = (Equiv.permCongr D.halfEdge) ((TauCeti.PDCode.crossingSlotEquiv n).permCongr (Equiv.prodCongrRight fun (x : Fin n) => finRotate 4))

theorem TauCeti.PDCode.crossingRotation_def {n : ℕ} (D : PDCode n) : D.crossingRotation = (Equiv.permCongr D.halfEdge) ((crossingSlotEquiv n).permCongr (Equiv.prodCongrRight fun (x : Fin n) => finRotate 4))

The defining equation of the crossing rotation.

@[simp]

theorem TauCeti.PDCode.crossingRotation_crossing {n : ℕ} (D : PDCode n) (i : Fin n) (slot : Fin 4) : D.crossingRotation (D.halfEdge ((crossingSlotEquiv n) (i, slot))) = D.crossing i (slot + 1)

The crossing rotation moves the half-edge in a slot to the next slot counterclockwise.

@[simp]

theorem TauCeti.PDCode.orbitCount_crossingRotation {n : ℕ} (D : PDCode n) : orbitCount D.crossingRotation = n

Each crossing is one orbit of the crossing rotation.

@[simp]

theorem TauCeti.PDCode.crossingRotation_mirror {n : ℕ} (D : PDCode n) : D.mirror.crossingRotation = D.crossingRotation

Mirroring preserves the crossing rotation.

@[simp]

theorem TauCeti.PDCode.crossingRotation_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).crossingRotation = half.permCongr D.crossingRotation

Relabelling conjugates the crossing rotation by the half-edge relabelling.

@[simp]

theorem TauCeti.PDCode.orbitCount_edgePair {n : ℕ} (D : PDCode n) : orbitCount ↑D.edgePair = 2 * n

Every arc is an orbit of the arc matching, so a code with n crossings has 2 * n arcs.

Faces

def TauCeti.PDCode.facePerm {n : ℕ} (D : PDCode n) : Equiv.Perm (Fin (4 * n))

The face traversal: turn to the next slot counterclockwise, then run along the arc from there. Its orbits are the faces of the underlying graph.

Equations

• D.facePerm = ↑D.edgePair * D.crossingRotation

theorem TauCeti.PDCode.facePerm_def {n : ℕ} (D : PDCode n) : D.facePerm = ↑D.edgePair * D.crossingRotation

The defining equation of the face traversal.

theorem TauCeti.PDCode.facePerm_apply {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) : D.facePerm h = ↑D.edgePair (D.crossingRotation h)

The face traversal rotates at the crossing and then crosses the arc.

noncomputable def TauCeti.PDCode.faceCount {n : ℕ} (D : PDCode n) : ℕ

The number of faces of the underlying graph: the orbits of the face traversal. Crossing-free circles are not part of this graph and contribute no faces.

Equations

• D.faceCount = TauCeti.orbitCount D.facePerm

theorem TauCeti.PDCode.faceCount_def {n : ℕ} (D : PDCode n) : D.faceCount = orbitCount D.facePerm

The number of faces is the number of orbits of the face traversal.

@[reducible, inline]

abbrev TauCeti.PDCode.Face {n : ℕ} (D : PDCode n) : Type

The faces of the underlying graph: the orbits of the face traversal.

Equations

• D.Face = Quotient (Equiv.Perm.SameCycle.setoid D.facePerm)

def TauCeti.PDCode.face {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) : D.Face

The face at a half-edge: the one in the corner at its crossing running counterclockwise from it to the next slot.

Equations

• D.face h = ⟦h⟧

theorem TauCeti.PDCode.face_eq_face_iff {n : ℕ} (D : PDCode n) {h h' : Fin (4 * n)} : D.face h = D.face h' ↔ D.facePerm.SameCycle h h'

Two half-edges have the same face exactly when the face traversal carries one to the other.

theorem TauCeti.PDCode.face_surjective {n : ℕ} (D : PDCode n) : Function.Surjective D.face

Every face is the face at some half-edge.

@[simp]

theorem TauCeti.PDCode.face_facePerm {n : ℕ} (D : PDCode n) (h : Fin (4 * n)) : D.face (D.facePerm h) = D.face h

The face traversal stays in one face.

@[simp]

theorem TauCeti.PDCode.card_face {n : ℕ} (D : PDCode n) : Nat.card D.Face = D.faceCount

The number of faces is the cardinality of the type of faces.

@[simp]

theorem TauCeti.PDCode.facePerm_mirror {n : ℕ} (D : PDCode n) : D.mirror.facePerm = D.facePerm

Mirroring preserves the face traversal.

@[simp]

theorem TauCeti.PDCode.facePerm_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).facePerm = half.permCongr D.facePerm

Relabelling conjugates the face traversal by the half-edge relabelling.

@[simp]

theorem TauCeti.PDCode.faceCount_mirror {n : ℕ} (D : PDCode n) : D.mirror.faceCount = D.faceCount

Mirroring preserves the number of faces.

@[simp]

theorem TauCeti.PDCode.faceCount_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).faceCount = D.faceCount

Relabelling preserves the number of faces.

@[simp]

theorem TauCeti.PDCode.face_relabel_eq_face_relabel_iff {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) {h h' : Fin (4 * n)} : (D.relabel half cross).face (half h) = (D.relabel half cross).face (half h') ↔ D.face h = D.face h'

Relabelling preserves face incidence: two relabelled half-edges lie on the same face of the relabelled code exactly when the original half-edges lie on the same face of the code.

theorem TauCeti.PDCode.sameCycle_crossingRotation_mul_edgePair_iff {n : ℕ} (D : PDCode n) {h h' : Fin (4 * n)} : (D.crossingRotation * ↑D.edgePair).SameCycle h h' ↔ D.face (↑D.edgePair h) = D.face (↑D.edgePair h')

Two half-edges lie in one orbit of running along an arc and then turning exactly when the far ends of their arcs lie on one face: this traversal is conjugate to the face traversal by the arc matching.

theorem TauCeti.PDCode.faceCount_eq_orbitCount_crossingRotation_mul_edgePair {n : ℕ} (D : PDCode n) : D.faceCount = orbitCount (D.crossingRotation * ↑D.edgePair)

The faces may equally be counted as the orbits of running along an arc and then turning to the next slot, which is conjugate to the face traversal.

The permutation triple

def TauCeti.PDCode.toPermutationTriple {n : ℕ} (D : PDCode n) : PermutationTriple (4 * n)

The permutation triple of the underlying graph of a PD-code: the crossing rotation, the arc matching, and the inverse face traversal.

Equations

• D.toPermutationTriple = TauCeti.PermutationTriple.ofTwo D.crossingRotation ↑D.edgePair

@[simp]

theorem TauCeti.PDCode.toPermutationTriple_σ0 {n : ℕ} (D : PDCode n) : D.toPermutationTriple.σ0 = D.crossingRotation

The first component of the triple is the crossing rotation.

@[simp]

theorem TauCeti.PDCode.toPermutationTriple_σ1 {n : ℕ} (D : PDCode n) : D.toPermutationTriple.σ1 = ↑D.edgePair

The second component of the triple is the arc matching.

@[simp]

theorem TauCeti.PDCode.toPermutationTriple_σinf {n : ℕ} (D : PDCode n) : D.toPermutationTriple.σinf = D.facePerm⁻¹

The third component of the triple is the inverse face traversal.

@[simp]

theorem TauCeti.PDCode.toPermutationTriple_mirror {n : ℕ} (D : PDCode n) : D.mirror.toPermutationTriple = D.toPermutationTriple

Mirroring preserves the underlying graph.

@[simp]

theorem TauCeti.PDCode.toPermutationTriple_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).toPermutationTriple = (PermutationTriple.transport half) D.toPermutationTriple

Relabelling relabels the sheets of the permutation triple by the half-edge relabelling.

@[simp]

theorem TauCeti.PDCode.crossingRotation_mem_monodromyGroup {n : ℕ} (D : PDCode n) : D.crossingRotation ∈ D.toPermutationTriple.monodromyGroup

The crossing rotation lies in the monodromy group of the underlying graph.

@[simp]

theorem TauCeti.PDCode.edgePair_mem_monodromyGroup {n : ℕ} (D : PDCode n) : ↑D.edgePair ∈ D.toPermutationTriple.monodromyGroup

The arc matching lies in the monodromy group of the underlying graph.

@[simp]

theorem TauCeti.PDCode.facePerm_mem_monodromyGroup {n : ℕ} (D : PDCode n) : D.facePerm ∈ D.toPermutationTriple.monodromyGroup

The face traversal lies in the monodromy group of the underlying graph.

theorem TauCeti.PDCode.mem_orbit_of_face_eq_face {n : ℕ} (D : PDCode n) {h h' : Fin (4 * n)} (hface : D.face h = D.face h') : h' ∈ MulAction.orbit (↥D.toPermutationTriple.monodromyGroup) h

Two half-edges on one face lie in one connected component of the underlying graph: the face traversal is a product of the crossing rotation and the arc matching.

theorem TauCeti.PDCode.mem_orbit_of_face_edgePair_eq_face {n : ℕ} (D : PDCode n) {h h' : Fin (4 * n)} (hface : D.face (↑D.edgePair h) = D.face h') : h' ∈ MulAction.orbit (↥D.toPermutationTriple.monodromyGroup) h

If the face at the far end of the arc ending at h is the face at h', then h' lies in the connected component of h.

theorem TauCeti.PDCode.eulerChar_toPermutationTriple {n : ℕ} (D : PDCode n) : D.toPermutationTriple.eulerChar = ↑D.faceCount - ↑n

Euler's formula for a PD-code. The underlying graph has n vertices and 2 * n edges, so its Euler characteristic is the number of faces less the number of crossings.

theorem TauCeti.PDCode.faceCount_le {n : ℕ} (D : PDCode n) : D.faceCount ≤ n + 2 * Nat.card D.toPermutationTriple.MonodromyOrbit

If the underlying graph of a PD-code has c connected components, it has at most n + 2 * c faces.

Planarity

def TauCeti.PDCode.IsPlanar {n : ℕ} (D : PDCode n) : Prop

A PD-code is planar when every connected component of its underlying graph, with the counterclockwise rotation at each crossing, is embedded in a sphere. Since each component has Euler characteristic at most 2, with equality exactly for the sphere, this says that the Euler characteristic is twice the number of components. Crossing-free circles are not part of the underlying graph and do not affect planarity.

Equations

• D.IsPlanar = (D.toPermutationTriple.eulerChar = 2 * ↑(Nat.card D.toPermutationTriple.MonodromyOrbit))

theorem TauCeti.PDCode.isPlanar_def {n : ℕ} (D : PDCode n) : D.IsPlanar ↔ D.toPermutationTriple.eulerChar = 2 * ↑(Nat.card D.toPermutationTriple.MonodromyOrbit)

The defining equation of planarity.

theorem TauCeti.PDCode.isPlanar_iff_faceCount_eq {n : ℕ} (D : PDCode n) : D.IsPlanar ↔ D.faceCount = n + 2 * Nat.card D.toPermutationTriple.MonodromyOrbit

A PD-code whose underlying graph has c connected components is planar exactly when the graph has n + 2 * c faces, the largest possible number.

theorem TauCeti.PDCode.isPlanar_iff_faceCount_eq_of_isConnected {n : ℕ} {D : PDCode n} (hD : D.toPermutationTriple.IsConnected) : D.IsPlanar ↔ D.faceCount = n + 2

A PD-code with n crossings and connected underlying graph is planar exactly when the graph has n + 2 faces.

@[simp]

theorem TauCeti.PDCode.isPlanar_of_zero (D : PDCode 0) : D.IsPlanar

A PD-code without crossings is planar.

@[simp]

theorem TauCeti.PDCode.isPlanar_mirror {n : ℕ} (D : PDCode n) : D.mirror.IsPlanar ↔ D.IsPlanar

Mirroring preserves planarity.

@[simp]

theorem TauCeti.PDCode.isPlanar_relabel {n m : ℕ} (D : PDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).IsPlanar ↔ D.IsPlanar

Relabelling preserves planarity.

One-crossing codes

theorem TauCeti.PDCode.isConnected_toPermutationTriple_of_one_crossing (D : PDCode 1) : D.toPermutationTriple.IsConnected

The underlying graph of a one-crossing code is connected: the rotation at its single crossing already moves every half-edge to every other.

@[simp]

theorem TauCeti.PDCode.faceCount_kink : kink.faceCount = 3

The kink has three faces: the two sides of its loop and the region outside the strand.

@[simp]

theorem TauCeti.PDCode.isPlanar_kink : kink.IsPlanar

The kink is planar.

theorem TauCeti.PDCode.exists_not_isPlanar : ∃ (D : PDCode 1), ¬D.IsPlanar

Not every PD-code is planar. The one-crossing code whose two arcs join opposite slots consists of two circles meeting in a single crossing, which no diagram in the plane can have. Its face traversal is a single cycle, so its graph has one face and embeds in the torus but not in the sphere.