Reidemeister equivalence of oriented PD-codes

Two diagrams present isotopic oriented links exactly when they are related by a chain of planar isotopies and Reidemeister moves (Reidemeister's theorem; Lickorish, Chapter 1). On oriented PD-codes a planar isotopy that keeps the crossings is an isomorphism of codes, generated by relabelling half-edges and crossings (TauCeti.OrientedPDCode.relabel) and by reading a crossing from another slot (TauCeti.OrientedPDCode.rotateCrossing). The Reidemeister moves are the local moves on PD-codes:

• the first move, a kink added to an arc (TauCeti.OrientedPDCode.reidemeisterOne) or to a crossing-free circle (TauCeti.OrientedPDCode.adjoinKink);
• the second move, a clasp inserted between two distinct arcs (TauCeti.OrientedPDCode.insertClasp), between an arc and a crossing-free circle (TauCeti.OrientedPDCode.insertCircleClasp), or between two crossing-free circles (TauCeti.OrientedPDCode.adjoinTwoCircleClasp);
• the third move, across a triangle of three crossings (TauCeti.OrientedPDCode.reidemeisterThree).

TauCeti.OrientedPDCode.IsReidemeisterMove collects these generators as a relation between oriented PD-codes with any numbers of crossings, and TauCeti.OrientedPDCode.ReidemeisterEquiv is the equivalence relation they generate. The orientation of every new arc is inherited from the arcs and circles a move cuts, so each move comes in all of its oriented forms.

A clasp between two distinct arcs is a generator only when the arcs border a common face on the sides the clasp uses, or lie in different connected components of the underlying graph. The relation itself places no planarity hypothesis on the codes it relates, but for a planar input code these are exactly the clasps that can be drawn in the plane: in the first case TauCeti.PDCode.isPlanar_insertClasp_iff keeps planarity, and in the second a drawing can place the two components so that their two faces meet. Inserting the clasp across two different faces of one component is excluded: the result is never planar (TauCeti.PDCode.not_isPlanar_insertClasp_of_face_ne). A clasp between two parts of a single arc is not a generator, since clasp insertion cuts two distinct arcs; such a clasp can be made by first splitting the arc with a kink, inserting the clasp between the two arcs this creates, and removing the kink again. The third move needs the three crossings to bound a triangular face, with an acyclic height order on the three strands (TauCeti.PDCode.HasReidemeisterThreeTriangle). That condition fixes the slots at which the triangle meets each crossing; the rotations of crossings let it apply however the three crossings are read.

Each generator keeps the Jones polynomial, the writhe-normalized Kauffman bracket and the number of components, so these are invariants of Reidemeister equivalence. In particular the right-handed trefoil is not Reidemeister equivalent to the unknot, nor to its mirror image. Reidemeister's theorem itself, comparing this relation with ambient isotopy of the realized links, is not proved here.

Main definitions

• TauCeti.OrientedPDCode.IsReidemeisterMove: the generating moves, an isomorphism of codes or a Reidemeister move.
• TauCeti.OrientedPDCode.ReidemeisterEquiv: Reidemeister equivalence, the equivalence relation they generate, between codes with possibly different numbers of crossings.

Main results

• TauCeti.OrientedPDCode.ReidemeisterEquiv.jonesPolynomial_eq: Reidemeister equivalent codes have the same Jones polynomial.
• TauCeti.OrientedPDCode.ReidemeisterEquiv.normalizedKauffmanBracket_eq: they have the same writhe-normalized Kauffman bracket, over every commutative ring.
• TauCeti.OrientedPDCode.ReidemeisterEquiv.componentCount_eq: they have the same number of components.
• TauCeti.OrientedPDCode.not_reidemeisterEquiv_rightHandedTrefoilPDCode_unknot and TauCeti.OrientedPDCode.not_reidemeisterEquiv_rightHandedTrefoilPDCode_mirror: the right-handed trefoil is neither Reidemeister equivalent to the unknot nor to its mirror image.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 1 (Reidemeister moves and Reidemeister's theorem) and Chapter 3 (invariance of the Jones polynomial, Theorem 3.5).
• K. Reidemeister, Elementare Begründung der Knotentheorie, Abh. Math. Sem. Univ. Hamburg 5 (1927), 24-32.

inductive TauCeti.OrientedPDCode.IsReidemeisterMove : (n : ℕ) × OrientedPDCode n → (n : ℕ) × OrientedPDCode n → Prop

The generating moves of Reidemeister equivalence, between oriented PD-codes with any numbers of crossings: the isomorphisms of codes and the Reidemeister moves. A move that adds crossings is stated in the direction that adds them; TauCeti.OrientedPDCode.ReidemeisterEquiv symmetrizes.

• relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : IsReidemeisterMove ⟨n, D⟩ ⟨m, D.relabel half cross⟩

  Relabelling the half-edges and the crossings.

• rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : IsReidemeisterMove ⟨n, D⟩ ⟨n, D.rotateCrossing i⟩

  Reading a crossing from its next slot.

• reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) : IsReidemeisterMove ⟨n, D⟩ ⟨n + 1, D.reidemeisterOne h b⟩

  The first move: a kink added to the arc ending at a half-edge.

• adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : IsReidemeisterMove ⟨n, D.adjoinCircle o⟩ ⟨n + 1, D.adjoinKink o b⟩

  The first move on a crossing-free circle.

• insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (hpq : D.face (↑D.edgePair p) = D.face q ∨ q ∉ MulAction.orbit (↥D.toPermutationTriple.monodromyGroup) p) : IsReidemeisterMove ⟨n, D⟩ ⟨n + 2, D.insertClasp p q b hqp hqe⟩

  The second move between two distinct arcs: inside a face both arcs border on the sides the clasp uses, or between two connected components of the underlying graph.

• insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) : IsReidemeisterMove ⟨n, D.adjoinCircle o⟩ ⟨n + 2, D.insertCircleClasp p o b⟩

  The second move between an arc and a crossing-free circle.

• adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : IsReidemeisterMove ⟨n, (D.adjoinCircle o₁).adjoinCircle o₂⟩ ⟨n + 2, D.adjoinTwoCircleClasp o₁ o₂ b⟩

  The second move between two crossing-free circles.

• reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangle c) : IsReidemeisterMove ⟨n, D⟩ ⟨n, D.reidemeisterThree c⟩

  The third move, across a triangle of three crossings with an acyclic height order.

def TauCeti.OrientedPDCode.ReidemeisterEquiv {n m : ℕ} (D : OrientedPDCode n) (D' : OrientedPDCode m) : Prop

Reidemeister equivalence of oriented PD-codes, possibly with different numbers of crossings: the equivalence relation generated by the isomorphisms of codes and the Reidemeister moves, TauCeti.OrientedPDCode.IsReidemeisterMove.

Equations

• D.ReidemeisterEquiv D' = Relation.EqvGen TauCeti.OrientedPDCode.IsReidemeisterMove ⟨n, D⟩ ⟨m, D'⟩

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_def {n m : ℕ} (D : OrientedPDCode n) (D' : OrientedPDCode m) : D.ReidemeisterEquiv D' ↔ Relation.EqvGen IsReidemeisterMove ⟨n, D⟩ ⟨m, D'⟩

The defining equation for Reidemeister equivalence: the equivalence relation generated by TauCeti.OrientedPDCode.IsReidemeisterMove, between the codes paired with their numbers of crossings.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.refl {n : ℕ} (D : OrientedPDCode n) : D.ReidemeisterEquiv D

Every code is Reidemeister equivalent to itself.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.symm {n m : ℕ} {D : OrientedPDCode n} {D' : OrientedPDCode m} (h : D.ReidemeisterEquiv D') : D'.ReidemeisterEquiv D

Reidemeister equivalence is symmetric.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.trans {n m k : ℕ} {D : OrientedPDCode n} {D' : OrientedPDCode m} {D'' : OrientedPDCode k} (h : D.ReidemeisterEquiv D') (h' : D'.ReidemeisterEquiv D'') : D.ReidemeisterEquiv D''

Reidemeister equivalence is transitive.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.induction {n m : ℕ} {motive : (n : ℕ) × OrientedPDCode n → (n : ℕ) × OrientedPDCode n → Prop} (move : ∀ {x y : (n : ℕ) × OrientedPDCode n}, IsReidemeisterMove x y → motive x y) (refl : ∀ (x : (n : ℕ) × OrientedPDCode n), motive x x) (symm : ∀ {x y : (n : ℕ) × OrientedPDCode n}, x.snd.ReidemeisterEquiv y.snd → motive x y → motive y x) (trans : ∀ {x y z : (n : ℕ) × OrientedPDCode n}, x.snd.ReidemeisterEquiv y.snd → y.snd.ReidemeisterEquiv z.snd → motive x y → motive y z → motive x z) {D : OrientedPDCode n} {D' : OrientedPDCode m} (h : D.ReidemeisterEquiv D') : motive ⟨n, D⟩ ⟨m, D'⟩

The induction principle for Reidemeister equivalence. A Prop-valued definition does not unfold outside the file that introduces it, so this, or rewriting with TauCeti.OrientedPDCode.reidemeisterEquiv_def, is how TauCeti.OrientedPDCode.ReidemeisterEquiv is eliminated: a property of every generating move that is closed under reflexivity, symmetry and transitivity holds of every Reidemeister equivalent pair.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.eq_of_isReidemeisterMove {n m : ℕ} {α : Sort u_1} (f : (n : ℕ) × OrientedPDCode n → α) (hf : ∀ (x y : (n : ℕ) × OrientedPDCode n), IsReidemeisterMove x y → f x = f y) {D : OrientedPDCode n} {D' : OrientedPDCode m} (h : D.ReidemeisterEquiv D') : f ⟨n, D⟩ = f ⟨m, D'⟩

A function of oriented PD-codes that every generating move keeps is an invariant of Reidemeister equivalence.

theorem TauCeti.OrientedPDCode.IsReidemeisterMove.reidemeisterEquiv {n m : ℕ} {D : OrientedPDCode n} {D' : OrientedPDCode m} (h : IsReidemeisterMove ⟨n, D⟩ ⟨m, D'⟩) : D.ReidemeisterEquiv D'

A single generating move relates Reidemeister equivalent codes.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_relabel {n m : ℕ} (D : OrientedPDCode n) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : D.ReidemeisterEquiv (D.relabel half cross)

Relabelling gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_rotateCrossing {n : ℕ} (D : OrientedPDCode n) (i : Fin n) : D.ReidemeisterEquiv (D.rotateCrossing i)

Reading a crossing from another slot gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_reidemeisterOne {n : ℕ} (D : OrientedPDCode n) (h : Fin (4 * n)) (b : Bool) : D.ReidemeisterEquiv (D.reidemeisterOne h b)

The first Reidemeister move gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinCircle o).ReidemeisterEquiv (D.adjoinKink o b)

The first Reidemeister move on a crossing-free circle gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_insertClasp {n : ℕ} (D : OrientedPDCode n) (p q : Fin (4 * n)) (b : Bool) (hqp : q ≠ p) (hqe : q ≠ ↑D.edgePair p) (hpq : D.face (↑D.edgePair p) = D.face q ∨ q ∉ MulAction.orbit (↥D.toPermutationTriple.monodromyGroup) p) : D.ReidemeisterEquiv (D.insertClasp p q b hqp hqe)

The second Reidemeister move between two distinct arcs, inside a face both border on the sides the clasp uses or between two connected components, gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_insertCircleClasp {n : ℕ} (D : OrientedPDCode n) (p : Fin (4 * n)) (o b : Bool) : (D.adjoinCircle o).ReidemeisterEquiv (D.insertCircleClasp p o b)

The second Reidemeister move between an arc and a crossing-free circle gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_adjoinTwoCircleClasp {n : ℕ} (D : OrientedPDCode n) (o₁ o₂ b : Bool) : ((D.adjoinCircle o₁).adjoinCircle o₂).ReidemeisterEquiv (D.adjoinTwoCircleClasp o₁ o₂ b)

The second Reidemeister move between two crossing-free circles gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.reidemeisterEquiv_reidemeisterThree {n : ℕ} (D : OrientedPDCode n) (c : Fin 3 ↪ Fin n) (h : D.HasReidemeisterThreeTriangle c) : D.ReidemeisterEquiv (D.reidemeisterThree c)

The third Reidemeister move gives a Reidemeister equivalent code.

theorem TauCeti.OrientedPDCode.IsReidemeisterMove.jonesPolynomial_eq {x y : (n : ℕ) × OrientedPDCode n} (h : IsReidemeisterMove x y) : x.snd.jonesPolynomial = y.snd.jonesPolynomial

Every generating move keeps the Jones polynomial.

theorem TauCeti.OrientedPDCode.IsReidemeisterMove.componentCount_eq {x y : (n : ℕ) × OrientedPDCode n} (h : IsReidemeisterMove x y) : x.snd.componentCount = y.snd.componentCount

Every generating move keeps the number of components.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.jonesPolynomial_eq {n m : ℕ} {D : OrientedPDCode n} {D' : OrientedPDCode m} (h : D.ReidemeisterEquiv D') : D.jonesPolynomial = D'.jonesPolynomial

The Jones polynomial is an invariant of Reidemeister equivalence.

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.normalizedKauffmanBracket_eq {n m : ℕ} {D : OrientedPDCode n} {D' : OrientedPDCode m} {R : Type u_1} [CommRing R] (h : D.ReidemeisterEquiv D') (a : Rˣ) : D.normalizedKauffmanBracket a = D'.normalizedKauffmanBracket a

The writhe-normalized Kauffman bracket is an invariant of Reidemeister equivalence, over every commutative ring: it is the Jones polynomial evaluated at t^(1/2) = A⁻².

theorem TauCeti.OrientedPDCode.ReidemeisterEquiv.componentCount_eq {n m : ℕ} {D : OrientedPDCode n} {D' : OrientedPDCode m} (h : D.ReidemeisterEquiv D') : D.componentCount = D'.componentCount

The number of components is an invariant of Reidemeister equivalence.

theorem TauCeti.OrientedPDCode.not_reidemeisterEquiv_rightHandedTrefoilPDCode_unknot (o : Bool) : ¬rightHandedTrefoilPDCode.ReidemeisterEquiv (unknot o)

The right-handed trefoil is knotted: no chain of Reidemeister moves turns its diagram into the crossing-free unknot, since its Jones polynomial t + t³ - t⁴ is not 1.

theorem TauCeti.OrientedPDCode.not_reidemeisterEquiv_rightHandedTrefoilPDCode_mirror : ¬rightHandedTrefoilPDCode.ReidemeisterEquiv rightHandedTrefoilPDCode.mirror

The right-handed trefoil is chiral: no chain of Reidemeister moves turns its diagram into its mirror image, since mirroring substitutes t⁻¹ for t in its Jones polynomial t + t³ - t⁴.