Reading a crossing of a PD-code from another slot

A PD-code lists the four half-edges at each crossing counterclockwise, starting from an arbitrary slot. Reading the crossing i from its next slot counterclockwise instead gives another code for the same diagram, TauCeti.PDCode.rotateCrossing D i: slot k of crossing i in the new code is slot k + 1 in the old one, and every other crossing is read as before. The two local strands at i exchange the parities of their slots, so the over-pair indicator of i flips. Relabelling (TauCeti.PDCode.relabel) renames half-edges and crossings but keeps the slot of every half-edge, so it cannot change where the reading of a crossing starts; relabellings and these rotations together are the isomorphisms of PD-codes. Local moves such as the third Reidemeister move fix the slots at which their tangle meets each crossing, and the rotations let them apply to a tangle however its crossings happen to be read.

The rotation leaves the underlying 4-valent graph unchanged: it keeps the crossing rotation, and so the faces and planarity, and the crossing turn, and so the components. It exchanges the two local smoothings at i exactly as it flips the over-pair indicator, so every state smooths the diagram into the same circles, and the Kauffman bracket is unchanged. On an oriented code it keeps the orientation of every half-edge and the sign of every crossing, so the writhe-normalized bracket is unchanged too.

Main definitions

• TauCeti.PDCode.rotateCrossing: read one crossing of a PD-code from its next slot.
• TauCeti.OrientedPDCode.rotateCrossing: the same for an oriented PD-code.

Main results

• TauCeti.PDCode.toPermutationTriple_rotateCrossing and TauCeti.PDCode.isPlanar_rotateCrossing: the rotation keeps the underlying graph and planarity.
• TauCeti.PDCode.componentCount_rotateCrossing: the rotation keeps the number of components.
• TauCeti.PDCode.kauffmanBracket_rotateCrossing: the rotation keeps the Kauffman bracket.
• TauCeti.OrientedPDCode.crossingSign_rotateCrossing and TauCeti.OrientedPDCode.normalizedKauffmanBracket_rotateCrossing: the rotation keeps every crossing sign and the writhe-normalized bracket.

References

• M. Mastin, Links and Planar Diagram Codes, Definitions 2-3 (the PD convention, reading each crossing counterclockwise).

def TauCeti.PDCode.rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : PDCode n

Read the crossing i of a PD-code from its next slot counterclockwise: slot k of i in the new code is slot k + 1 in D. The local strand on slots 0 and 2 becomes the one on slots 1 and 3, so the over-pair indicator of i flips. The new code describes the same diagram.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

Slot k of the rotated crossing is slot k + 1 of the old one.

@[simp]

theorem TauCeti.PDCode.rotateCrossing_crossing_of_ne {n : ℕ} (D : PDCode n) (i : Fin n) {j : Fin n} (hj : j ≠ i) (slot : Fin 4) : (D.rotateCrossing i).halfEdge ((crossingSlotEquiv n) (j, slot)) = D.halfEdge ((crossingSlotEquiv n) (j, slot))

The other crossings keep their slots.

@[simp]

theorem TauCeti.PDCode.rotateCrossing_edgePair {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).edgePair = D.edgePair

The rotation keeps the arcs.

@[simp]

theorem TauCeti.PDCode.rotateCrossing_crossinglessComponentCount {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).crossinglessComponentCount = D.crossinglessComponentCount

The rotation keeps the crossing-free circles.

@[simp]

theorem TauCeti.PDCode.rotateCrossing_overPair_self {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).overPair i = !D.overPair i

The over-pair indicator of the rotated crossing flips.

@[simp]

theorem TauCeti.PDCode.rotateCrossing_overPair_of_ne {n : ℕ} (D : PDCode n) (i : Fin n) {j : Fin n} (hj : j ≠ i) : (D.rotateCrossing i).overPair j = D.overPair j

The other crossings keep their over-pair indicators.

@[simp]

theorem TauCeti.PDCode.mirror_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).mirror = D.mirror.rotateCrossing i

Mirroring commutes with reading a crossing from another slot.

@[simp]

theorem TauCeti.PDCode.crossingRotation_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).crossingRotation = D.crossingRotation

The rotation keeps the counterclockwise rotation of the slots at every crossing.

@[simp]

theorem TauCeti.PDCode.facePerm_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).facePerm = D.facePerm

The rotation keeps the face traversal.

@[simp]

theorem TauCeti.PDCode.toPermutationTriple_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).toPermutationTriple = D.toPermutationTriple

The rotation keeps the permutation triple of the underlying graph.

@[simp]

theorem TauCeti.PDCode.isPlanar_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).IsPlanar ↔ D.IsPlanar

The rotation keeps planarity.

@[simp]

theorem TauCeti.PDCode.crossingTurn_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).crossingTurn = D.crossingTurn

The rotation keeps the passage through each crossing to the opposite slot.

@[simp]

theorem TauCeti.PDCode.componentPerm_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).componentPerm = D.componentPerm

The rotation keeps the component traversal.

@[simp]

theorem TauCeti.PDCode.componentCount_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) : (D.rotateCrossing i).componentCount = D.componentCount

The rotation keeps the number of components.

theorem TauCeti.PDCode.smoothingTurn_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) (b : Fin n → Bool) : (D.rotateCrossing i).smoothingTurn b = D.smoothingTurn (Function.update b i !b i)

Smoothing the rotated code by a family of local smoothings is smoothing D by the family with the other local smoothing at i.

theorem TauCeti.PDCode.smoothingChoice_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) : (D.rotateCrossing i).smoothingChoice s = Function.update (D.smoothingChoice s) i !D.smoothingChoice s i

A state selects at the rotated crossing the other local smoothing of the rotated code.

@[simp]

theorem TauCeti.PDCode.statePerm_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) : (D.rotateCrossing i).statePerm s = D.statePerm s

Every state smooths the rotated code into the same circles as D.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) (s : Fin n → Bool) : (D.rotateCrossing i).stateLoopCount s = D.stateLoopCount s

Every state leaves as many circles in the rotated code as in D.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_rotateCrossing {n : ℕ} (D : PDCode n) (i : Fin n) {R : Type u_1} [CommRing R] (a : Rˣ) : (D.rotateCrossing i).kauffmanBracket a = D.kauffmanBracket a

The rotation keeps the Kauffman bracket.

def TauCeti.OrientedPDCode.rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : OrientedPDCode n

Read the crossing i of an oriented PD-code from its next slot counterclockwise, keeping the orientation of every half-edge.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.OrientedPDCode.toPDCode_rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : (D.rotateCrossing i).toPDCode = D.rotateCrossing i

Forgetting orientation after the rotation gives the rotation of the underlying code.

@[simp]

theorem TauCeti.OrientedPDCode.rotateCrossing_orientation {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : (D.rotateCrossing i).orientation = D.orientation

The rotation keeps the orientation of every half-edge.

@[simp]

theorem TauCeti.OrientedPDCode.rotateCrossing_crossinglessComponents {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : (D.rotateCrossing i).crossinglessComponents = D.crossinglessComponents

The rotation keeps the oriented crossing-free circles.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i j : Fin n) : (D.rotateCrossing i).crossingSign j = D.crossingSign j

The rotation keeps every crossing sign. At the rotated crossing both the orientation parity of slots 0 and 1 and the over-pair indicator flip.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : (D.rotateCrossing i).writhe = D.writhe

The rotation keeps the writhe.

@[simp]

theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) {R : Type u_1} [CommRing R] (a : Rˣ) : (D.rotateCrossing i).normalizedKauffmanBracket a = D.normalizedKauffmanBracket a

The rotation keeps the writhe-normalized Kauffman bracket.