An oriented Reidemeister kink on a crossing-free circle

OrientedPDCode.adjoinKink D o b is the oriented version of PDCode.adjoinKink. The orientation o selects the direction of its isolated component and b selects its over-strand. The first Reidemeister move relates this diagram to D.adjoinCircle o.

The new crossing has sign +1 for b = true and -1 for b = false, independently of o. Its writhe correction cancels the Kauffman bracket factor. Thus adjoining an oriented kink and adjoining a crossing-free circle give the same normalized bracket, even when D is empty. The resulting Jones polynomial equality is in TauCeti.KnotTheory.PDCode.Jones. The construction commutes with reflection and with reversing all component orientations.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapters 1 and 3 (oriented Reidemeister moves and the Jones polynomial).
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395–407.

def TauCeti.OrientedPDCode.adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : OrientedPDCode (n + 1)

Adjoin an oriented isolated kink. Its slots 1 and 2 have direction o, and slots 0 and 3 have the opposite direction. Smoothing away the kink leaves the newly adjoined circle in D.adjoinCircle o.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.toPDCode_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).toPDCode = D.adjoinKink b

Forgetting orientation gives the isolated unoriented kink.

@[simp]

theorem TauCeti.OrientedPDCode.orientation_adjoinKink_inl {n : ℕ} (D : OrientedPDCode n) (o b : Bool) (x : Fin (4 * n)) : (D.adjoinKink o b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inl x)) = D.orientation x

The old half-edges keep their orientations.

@[simp]

theorem TauCeti.OrientedPDCode.orientation_adjoinKink_inr {n : ℕ} (D : OrientedPDCode n) (o b : Bool) (s : Fin 4) : (D.adjoinKink o b).orientation ((PDCode.halfEdgeSuccEquiv n) (Sum.inr s)) = ![!o, o, o, !o] s

The directions at the four new slots.

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).crossinglessComponents = D.crossinglessComponents

The crossing-free components of the surrounding diagram are unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_adjoinKink_castSucc {n : ℕ} (D : OrientedPDCode n) (o b : Bool) (i : Fin n) : (D.adjoinKink o b).crossingSign i.castSucc = D.crossingSign i

Every old crossing keeps its sign.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_adjoinKink_last {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).crossingSign (Fin.last n) = if b = true then 1 else -1

The isolated kink has positive sign exactly when its over-pair indicator is true.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).writhe = D.writhe + if b = true then 1 else -1

The isolated kink changes the writhe by its crossing sign.

@[simp]

theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_adjoinKink {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (o b : Bool) (a : Rˣ) : (D.adjoinKink o b).normalizedKauffmanBracket a = (D.adjoinCircle o).normalizedKauffmanBracket a

Removing the kink from an isolated oriented component leaves the normalized bracket unchanged. No nonemptiness assumption on the surrounding diagram is needed.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).mirror = D.mirror.adjoinKink o !b

Reflection reverses the crossing sign without changing the component direction.

@[simp]

theorem TauCeti.OrientedPDCode.reverse_adjoinKink {n : ℕ} (D : OrientedPDCode n) (o b : Bool) : (D.adjoinKink o b).reverse = D.reverse.adjoinKink (!o) b

Reversing all component directions reverses the new kink as well.