Adjoining a crossing-free circle to a PD-code

A PDCode records components that never visit a crossing by their count. This file makes the corresponding diagram operation explicit: PDCode.adjoinCircle adds one disjoint circle without changing any crossing data. The oriented and framed versions also record the orientation and relative framing of the new component.

The component and state-circle formulas make the operation usable in local move calculations. For a nonempty diagram, adjoining a circle multiplies the Kauffman bracket by the loop value jonesDelta; the nonemptiness hypothesis is necessary because the empty code is normalised to have bracket one rather than a negative power of the loop value.

ClaspInsertion applies to clasps whose arcs meet crossings and does not treat a clasp through a crossing-free circle; this file supplies the separate operation of adjoining a disjoint crossing-free circle, which local move calculations need alongside it.

The PD-code convention follows M. Mastin, Links and Planar Diagram Codes, Definitions 2--3. The disjoint-circle Kauffman-bracket relation follows L. H. Kauffman, State models and the Jones polynomial, and W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3.

Unoriented codes

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

Adjoin one disjoint circle to a PD-code. The crossing data and all crossing-bearing components are unchanged; only the explicit count of crossing-free components increases.

Equations

• D.adjoinCircle = { halfEdge := D.halfEdge, edgePair := D.edgePair, crossinglessComponentCount := D.crossinglessComponentCount + 1, overPair := D.overPair }

@[simp]

theorem TauCeti.PDCode.adjoinCircle_halfEdge {n : ℕ} (D : PDCode n) : D.adjoinCircle.halfEdge = D.halfEdge

Adjoining a circle leaves the crossing labels unchanged.

@[simp]

theorem TauCeti.PDCode.adjoinCircle_edgePair {n : ℕ} (D : PDCode n) : D.adjoinCircle.edgePair = D.edgePair

Adjoining a circle leaves the arc matching unchanged.

@[simp]

theorem TauCeti.PDCode.adjoinCircle_overPair {n : ℕ} (D : PDCode n) : D.adjoinCircle.overPair = D.overPair

Adjoining a circle leaves the over-strand choice at every crossing unchanged.

@[simp]

theorem TauCeti.PDCode.adjoinCircle_crossinglessComponentCount {n : ℕ} (D : PDCode n) : D.adjoinCircle.crossinglessComponentCount = D.crossinglessComponentCount + 1

The new circle contributes one crossing-free component.

@[simp]

theorem TauCeti.PDCode.crossingTurn_adjoinCircle {n : ℕ} (D : PDCode n) : D.adjoinCircle.crossingTurn = D.crossingTurn

Adjoining a circle leaves the crossing traversal unchanged.

@[simp]

theorem TauCeti.PDCode.componentPerm_adjoinCircle {n : ℕ} (D : PDCode n) : D.adjoinCircle.componentPerm = D.componentPerm

Adjoining a circle leaves the component traversal permutation unchanged.

@[simp]

theorem TauCeti.PDCode.crossingComponentCount_adjoinCircle {n : ℕ} (D : PDCode n) : D.adjoinCircle.crossingComponentCount = D.crossingComponentCount

Adjoining a circle does not change the crossing-bearing components.

@[simp]

theorem TauCeti.PDCode.componentCount_adjoinCircle {n : ℕ} (D : PDCode n) : D.adjoinCircle.componentCount = D.componentCount + 1

Adjoining a circle increases the total component count by one.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_adjoinCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.adjoinCircle.smoothingTurn s = D.smoothingTurn s

Adjoining a circle leaves the smoothing traversal permutation unchanged.

@[simp]

theorem TauCeti.PDCode.smoothingChoice_adjoinCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.adjoinCircle.smoothingChoice s = D.smoothingChoice s

Adjoining a circle leaves the chosen local smoothing at every crossing unchanged.

@[simp]

theorem TauCeti.PDCode.statePerm_adjoinCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.adjoinCircle.statePerm s = D.statePerm s

Adjoining a circle leaves the state traversal permutation unchanged.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_adjoinCircle {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.adjoinCircle.stateLoopCount s = D.stateLoopCount s + 1

Every smoothing has exactly one additional circle after adjoining a circle.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_adjoinCircle {n : ℕ} {R : Type u_1} [CommRing R] (D : PDCode n) (h : 0 < D.componentCount) (a : Rˣ) : D.adjoinCircle.kauffmanBracket a = TemperleyLieb.jonesDelta a * D.kauffmanBracket a

Adjoining a circle to a nonempty diagram multiplies its Kauffman bracket by the loop value. The empty code is excluded because its bracket is normalized to one.

@[simp]

theorem TauCeti.PDCode.mirror_adjoinCircle {n : ℕ} (D : PDCode n) : D.adjoinCircle.mirror = D.mirror.adjoinCircle

Mirroring commutes with adjoining an unoriented circle.

Oriented codes

def TauCeti.OrientedPDCode.adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) : OrientedPDCode n

Adjoin a crossing-free component with the specified orientation.

Equations

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

@[simp]

theorem TauCeti.OrientedPDCode.toPDCode_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) : (D.adjoinCircle orientation).toPDCode = D.adjoinCircle

Forgetting orientation leaves the added circle in the underlying code.

@[simp]

theorem TauCeti.OrientedPDCode.orientation_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) : (D.adjoinCircle orientation).orientation = D.orientation

The directions at existing crossings remain unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.crossinglessComponents_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) : (D.adjoinCircle orientation).crossinglessComponents = orientation ::ₘ D.crossinglessComponents

The orientation of the new circle is added to the crossing-free orientation multiset.

@[simp]

theorem TauCeti.OrientedPDCode.crossingSign_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) (i : Fin n) : (D.adjoinCircle orientation).crossingSign i = D.crossingSign i

Adjoining a circle leaves every existing crossing sign unchanged.

@[simp]

theorem TauCeti.OrientedPDCode.writhe_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) : (D.adjoinCircle orientation).writhe = D.writhe

An isolated circle does not change the writhe.

theorem TauCeti.OrientedPDCode.exists_eq_adjoinCircle_of_mem {n : ℕ} {D : OrientedPDCode n} {o : Bool} (h : o ∈ D.crossinglessComponents) : ∃ (D₀ : OrientedPDCode n), D = D₀.adjoinCircle o

A code with a crossing-free circle of orientation o is obtained by adjoining that circle to the code without it.

@[simp]

theorem TauCeti.OrientedPDCode.mirror_adjoinCircle {n : ℕ} (D : OrientedPDCode n) (orientation : Bool) : (D.adjoinCircle orientation).mirror = D.mirror.adjoinCircle orientation

Mirroring commutes with adjoining an oriented crossing-free circle.

@[simp]

theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_adjoinCircle {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (orientation : Bool) (h : 0 < D.componentCount) (a : Rˣ) : (D.adjoinCircle orientation).normalizedKauffmanBracket a = TemperleyLieb.jonesDelta a * D.normalizedKauffmanBracket a

Adjoining a circle to a nonempty oriented diagram multiplies the normalized bracket by the same loop value as the unoriented bracket, since the writhe is unchanged.

Framed oriented codes

def TauCeti.FramedOrientedPDCode.adjoinCircle {n : ℕ} (D : FramedOrientedPDCode n) (orientation : Bool) (framing : ℤ) : FramedOrientedPDCode n

Adjoin a crossing-free component with its orientation and Seifert-relative framing.

Equations

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

@[simp]

theorem TauCeti.FramedOrientedPDCode.toOrientedPDCode_adjoinCircle {n : ℕ} (D : FramedOrientedPDCode n) (orientation : Bool) (framing : ℤ) : (D.adjoinCircle orientation framing).toOrientedPDCode = D.adjoinCircle orientation

Forgetting framing retains the orientation of the added circle.

@[simp]

theorem TauCeti.FramedOrientedPDCode.framing_adjoinCircle {n : ℕ} (D : FramedOrientedPDCode n) (orientation : Bool) (framing : ℤ) : (D.adjoinCircle orientation framing).framing = D.framing

Existing framing coefficients are unchanged.

@[simp]

theorem TauCeti.FramedOrientedPDCode.crossinglessFramings_adjoinCircle {n : ℕ} (D : FramedOrientedPDCode n) (orientation : Bool) (framing : ℤ) : (D.adjoinCircle orientation framing).crossinglessFramings = (orientation, framing) ::ₘ D.crossinglessFramings

The new circle's orientation and framing are recorded together.

@[simp]

theorem TauCeti.FramedOrientedPDCode.mirror_adjoinCircle {n : ℕ} (D : FramedOrientedPDCode n) (orientation : Bool) (framing : ℤ) : (D.adjoinCircle orientation framing).mirror = D.mirror.adjoinCircle orientation (-framing)

Mirroring commutes with adjoining a framed oriented crossing-free circle and negates its framing.