The Kauffman bracket of a PD-code

Smoothing every crossing of a diagram in one of its two ways turns the diagram into a disjoint union of circles. A state of a PD-code with n crossings is such a choice at each crossing, recorded as s : Fin n → Bool, with s i = true selecting the A-smoothing at crossing i: the smoothing that turns left off the over-strand, equivalently the one joining the two regions swept out when the over-strand is rotated counterclockwise. With the four slots of a crossing in counterclockwise order that smoothing takes each over-slot to the preceding slot, which is TauCeti.PDCode.slotSmoothing applied to the code's own over-pair indicator; the B-smoothing is the same construction applied to the complementary indicator.

Reconnecting the half-edges accordingly gives TauCeti.PDCode.statePerm, the traversal of the smoothed diagram: cross an arc, then follow the smoothing at the crossing reached. Exactly as for TauCeti.PDCode.componentPerm, each circle of the smoothed diagram carries two of its orbits, one for each direction of travel, so TauCeti.PDCode.stateLoopCount halves the orbit count and adds the crossing-free circles that the code records separately.

The Kauffman bracket is the resulting state sum ∑ s, a ^ (A(s) - B(s)) * δ ^ (loops s - 1), formed over a commutative ring with a distinguished unit a at the loop value δ = -(a ^ 2 + a⁻¹ ^ 2) (TauCeti.TemperleyLieb.jonesDelta), which is the value at which the Kauffman-bracket expansion of a crossing is invertible. This is Kauffman's ⟨·⟩ with Lickorish's normalisation ⟨unknot⟩ = 1: a code with no crossings and c ≥ 1 circles has bracket δ ^ (c - 1). The exponent is truncated subtraction, so the empty code has bracket 1; every code with a crossing has at least one circle in each state (TauCeti.PDCode.one_le_stateLoopCount), so this affects only the empty code.

The bracket depends on a PD-code only through its relabelling class, and mirroring a code inverts the unit a. On the one-crossing kink diagram TauCeti.PDCode.kink it takes the value -a ^ 3, the framing factor of the first Reidemeister move. Whether the bracket descends from diagrams to knots is the question of its behaviour under the Reidemeister moves, which are separate constructions on PD-codes; the first move is in TauCeti/KnotTheory/PDCode/Reidemeister/One.lean.

For an oriented PD-code, TauCeti.OrientedPDCode.normalizedKauffmanBracket multiplies the bracket by the writhe correction (-a ^ 3) ^ (-writhe). This is the normalization used to obtain the Jones polynomial from the bracket.

Main definitions

• TauCeti.PDCode.smoothingTurn: the reconnection of the half-edges smoothing every crossing.
• TauCeti.PDCode.smoothingChoice: the over-pair indicator a state selects at each crossing.
• TauCeti.PDCode.statePerm: the traversal of the smoothed diagram.
• TauCeti.PDCode.stateLoopCount: the number of circles of the smoothed diagram.
• TauCeti.PDCode.stateWeight: the weight a ^ (A(s) - B(s)) of a state.
• TauCeti.PDCode.kauffmanBracket: the Kauffman bracket state sum.
• TauCeti.OrientedPDCode.normalizedKauffmanBracket: the writhe-normalized bracket.

Main results

• TauCeti.PDCode.even_orbitCount_statePerm: the traversal orbits of a smoothed diagram come in pairs, and TauCeti.PDCode.one_le_stateLoopCount: a code with a crossing leaves at least one circle in every state.
• TauCeti.PDCode.kauffmanBracket_relabel: the bracket is invariant under relabelling.
• TauCeti.PDCode.kauffmanBracket_mirror: mirroring the code inverts the unit.
• TauCeti.PDCode.kauffmanBracket_eq_jonesDelta_pow: a code with no crossings and c circles has bracket δ ^ (c - 1).
• TauCeti.PDCode.stateLoopCount_kink_true, TauCeti.PDCode.stateLoopCount_kink_false: the two smoothings of a kink leave two circles and one circle.
• TauCeti.PDCode.kauffmanBracket_kink: the kink diagram has bracket -a ^ 3.

References

• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395-407.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3 (the Kauffman bracket and the Jones polynomial).
• M. Mastin, Links and Planar Diagram Codes, Definitions 2-3 (the PD convention).

theorem TauCeti.PDCode.slotSmoothing_ne_oppositeCrossingSlot (b : Bool) (slot : Fin 4) : (slotSmoothing b) slot ≠ oppositeCrossingSlot slot

A local smoothing never joins a slot to the opposite slot: the two arcs of a smoothing cut across the two local strands instead of following them, which is what distinguishes a smoothing from TauCeti.PDCode.crossingTurn.

theorem TauCeti.PDCode.slotSmoothing_ne_slotSmoothing_not (b : Bool) : slotSmoothing b ≠ slotSmoothing !b

The two local smoothings at a crossing are distinct.

def TauCeti.PDCode.smoothingTurn {n : ℕ} (D : PDCode n) (b : Fin n → Bool) : Equiv.Perm (Fin (4 * n))

Smooth every crossing of a PD-code, using at crossing i the local smoothing slotSmoothing (b i). This is the smoothing counterpart of TauCeti.PDCode.crossingTurn, which instead follows a local strand through a crossing.

Equations

• D.smoothingTurn b = (Equiv.permCongr D.halfEdge) ((TauCeti.PDCode.crossingSlotEquiv n).permCongr (Equiv.prodCongrRight fun (i : Fin n) => TauCeti.PDCode.slotSmoothing (b i)))

theorem TauCeti.PDCode.smoothingTurn_def {n : ℕ} (D : PDCode n) (b : Fin n → Bool) : D.smoothingTurn b = (Equiv.permCongr D.halfEdge) ((crossingSlotEquiv n).permCongr (Equiv.prodCongrRight fun (i : Fin n) => slotSmoothing (b i)))

The defining equation for the smoothing traversal permutation.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_crossing {n : ℕ} (D : PDCode n) (b : Fin n → Bool) (i : Fin n) (slot : Fin 4) : (D.smoothingTurn b) (D.halfEdge ((crossingSlotEquiv n) (i, slot))) = D.crossing i ((slotSmoothing (b i)) slot)

Smoothing reconnects the slots at a crossing by the chosen local smoothing.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_apply_apply {n : ℕ} (D : PDCode n) (b : Fin n → Bool) (h : Fin (4 * n)) : (D.smoothingTurn b) ((D.smoothingTurn b) h) = h

Smoothing is an involution of the half-edges.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_mirror {n : ℕ} (D : PDCode n) (b : Fin n → Bool) : D.mirror.smoothingTurn b = D.smoothingTurn b

Mirroring a code does not change how a prescribed family of local smoothings reconnects its half-edges; only which of them is the A-smoothing changes.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_reconnect {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (c : Fin n → Bool) : (D.reconnect p q).smoothingTurn c = D.smoothingTurn c

Reconnecting arcs does not change how the crossings are smoothed.

@[simp]

theorem TauCeti.PDCode.smoothingTurn_relabel {n m : ℕ} (D : PDCode n) (b : Fin m → Bool) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).smoothingTurn b = half.permCongr (D.smoothingTurn (b ∘ ⇑cross))

Relabelling conjugates smoothing by the half-edge relabelling, after transporting the family of local smoothings along the crossing relabelling.

def TauCeti.PDCode.smoothingChoice {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (i : Fin n) : Bool

The over-pair indicator of the local smoothing that a state selects at a crossing: the code's own indicator where the state chooses the A-smoothing, and the complementary one where it chooses the B-smoothing.

Equations

• D.smoothingChoice s i = bif s i then D.overPair i else !D.overPair i

@[simp]

theorem TauCeti.PDCode.smoothingChoice_of_true {n : ℕ} (D : PDCode n) {s : Fin n → Bool} {i : Fin n} (hs : s i = true) : D.smoothingChoice s i = D.overPair i

Where a state is true it selects the A-smoothing, the one built from the code's own over-pair indicator.

@[simp]

theorem TauCeti.PDCode.smoothingChoice_of_false {n : ℕ} (D : PDCode n) {s : Fin n → Bool} {i : Fin n} (hs : s i = false) : D.smoothingChoice s i = !D.overPair i

Where a state is false it selects the B-smoothing, the one built from the complementary over-pair indicator.

@[simp]

theorem TauCeti.PDCode.smoothingChoice_mirror {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.mirror.smoothingChoice s = D.smoothingChoice fun (j : Fin n) => !s j

Mirroring a code exchanges the A- and B-smoothings, so it acts on states by negation.

@[simp]

theorem TauCeti.PDCode.smoothingChoice_reconnect {n : ℕ} (D : PDCode n) (p q : Fin (4 * n)) (s : Fin n → Bool) : (D.reconnect p q).smoothingChoice s = D.smoothingChoice s

Reconnecting arcs does not change which smoothing a state selects.

@[simp]

theorem TauCeti.PDCode.smoothingChoice_relabel {n m : ℕ} (D : PDCode n) (s : Fin m → Bool) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).smoothingChoice s = D.smoothingChoice (s ∘ ⇑cross) ∘ ⇑cross.symm

Relabelling reads a state's choice at the old crossing name.

def TauCeti.PDCode.statePerm {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Equiv.Perm (Fin (4 * n))

The traversal of the diagram smoothed according to the state s: cross an arc, then follow the chosen smoothing at the crossing reached. Its orbits are the two directed traversals of each circle of the smoothed diagram.

Equations

• D.statePerm s = D.smoothingTurn (D.smoothingChoice s) * ↑D.edgePair

theorem TauCeti.PDCode.statePerm_def {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.statePerm s = D.smoothingTurn (D.smoothingChoice s) * ↑D.edgePair

The defining equation of smoothed traversal.

@[simp]

theorem TauCeti.PDCode.statePerm_apply {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (h : Fin (4 * n)) : (D.statePerm s) h = (D.smoothingTurn (D.smoothingChoice s)) (↑D.edgePair h)

Smoothed traversal pairs the arc first, then follows the chosen smoothing.

@[simp]

theorem TauCeti.PDCode.statePerm_mirror {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.mirror.statePerm s = D.statePerm fun (i : Fin n) => !s i

Mirroring a code negates the state that produces a given smoothed diagram.

@[simp]

theorem TauCeti.PDCode.statePerm_relabel {n m : ℕ} (D : PDCode n) (s : Fin m → Bool) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).statePerm s = half.permCongr (D.statePerm (s ∘ ⇑cross))

Relabelling conjugates smoothed traversal by the half-edge relabelling.

Codes with one crossing more

Let D' be a code with one crossing more than D, whose first n crossings keep the half-edges and over-strands of D, and whose last crossing takes the four new half-edge positions and has over-pair indicator b. Crossing insertion and the first Reidemeister move build such codes. A state of D' is a state of D together with a choice at the new crossing, and the lemmas below split its smoothing accordingly.

theorem TauCeti.PDCode.smoothingTurn_eq_permCongr_sumCongr {n : ℕ} {D : PDCode n} {D' : PDCode (n + 1)} (hD : D'.halfEdge = (halfEdgeSuccEquiv n).permCongr (D.halfEdge.sumCongr 1)) (c : Fin (n + 1) → Bool) : D'.smoothingTurn c = (halfEdgeSuccEquiv n).permCongr ((D.smoothingTurn (Fin.init c)).sumCongr (slotSmoothing (c (Fin.last n))))

Smoothing D' is smoothing D together with the chosen local smoothing of the new crossing.

theorem TauCeti.PDCode.init_smoothingChoice_of_overPair_eq {n : ℕ} {D : PDCode n} {D' : PDCode (n + 1)} {b : Bool} (hO : D'.overPair = Fin.snoc D.overPair b) (s : Fin (n + 1) → Bool) : Fin.init (D'.smoothingChoice s) = D.smoothingChoice (Fin.init s)

At the old crossings, a state of D' selects the smoothings its restriction selects in D.

theorem TauCeti.PDCode.smoothingChoice_last_of_overPair_eq {n : ℕ} {D : PDCode n} {D' : PDCode (n + 1)} {b : Bool} (hO : D'.overPair = Fin.snoc D.overPair b) (s : Fin (n + 1) → Bool) : D'.smoothingChoice s (Fin.last n) = (s (Fin.last n) == b)

At the new crossing, a state of D' selects the local smoothing slotSmoothing true exactly when its choice there is b.

noncomputable def TauCeti.PDCode.stateLoopCount {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : ℕ

The number of circles of the diagram smoothed according to the state s, the crossing-free circles of the code included. Each circle meeting a crossing is represented by the two directed orbits of TauCeti.PDCode.statePerm, one for each direction of travel, exactly as for TauCeti.PDCode.crossingComponentCount.

Equations

• D.stateLoopCount s = TauCeti.orbitCount (D.statePerm s) / 2 + D.crossinglessComponentCount

theorem TauCeti.PDCode.stateLoopCount_def {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.stateLoopCount s = orbitCount (D.statePerm s) / 2 + D.crossinglessComponentCount

The number of circles of a smoothed diagram is half the number of directed traversal orbits, plus the crossing-free circles.

theorem TauCeti.PDCode.isPerfectMatching_smoothingTurn {n : ℕ} (D : PDCode n) (b : Fin n → Bool) : IsPerfectMatching (D.smoothingTurn b)

Smoothing every crossing of a code pairs off its half-edges.

theorem TauCeti.PDCode.even_orbitCount_statePerm {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : Even (orbitCount (D.statePerm s))

The directed traversal orbits of a smoothed diagram come in pairs, as the halving in TauCeti.PDCode.stateLoopCount presumes: smoothed traversal is a product of two perfect matchings.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_eq_crossinglessComponentCount (D : PDCode 0) (s : Fin 0 → Bool) : D.stateLoopCount s = D.crossinglessComponentCount

A code with no crossings has one circle per crossing-free component, in every state.

theorem TauCeti.PDCode.one_le_stateLoopCount_of_componentCount_pos {n : ℕ} (D : PDCode n) (h : 0 < D.componentCount) (s : Fin n → Bool) : 1 ≤ D.stateLoopCount s

Every smoothing of a diagram with a component has at least one circle.

theorem TauCeti.PDCode.one_le_stateLoopCount {n : ℕ} (D : PDCode n) (hn : n ≠ 0) (s : Fin n → Bool) : 1 ≤ D.stateLoopCount s

A code with a crossing has at least one circle in every state.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_mirror {n : ℕ} (D : PDCode n) (s : Fin n → Bool) : D.mirror.stateLoopCount s = D.stateLoopCount fun (i : Fin n) => !s i

Mirroring a code negates the state producing a given circle count.

@[simp]

theorem TauCeti.PDCode.stateLoopCount_relabel {n m : ℕ} (D : PDCode n) (s : Fin m → Bool) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).stateLoopCount s = D.stateLoopCount (s ∘ ⇑cross)

Relabelling preserves the circle count of every state.

def TauCeti.PDCode.stateWeight {n : ℕ} {R : Type u_1} [CommMonoid R] (s : Fin n → Bool) (a : Rˣ) : Rˣ

The weight of a state: the unit a at each A-smoothing and a⁻¹ at each B-smoothing, so that a state with p of the former and q of the latter has weight a ^ (p - q).

Equations

• TauCeti.PDCode.stateWeight s a = ∏ i : Fin n, bif s i then a else a⁻¹

theorem TauCeti.PDCode.stateWeight_def {n : ℕ} {R : Type u_1} [CommMonoid R] (s : Fin n → Bool) (a : Rˣ) : stateWeight s a = ∏ i : Fin n, bif s i then a else a⁻¹

The defining equation of a state's Kauffman-bracket weight.

@[simp]

theorem TauCeti.PDCode.stateWeight_append {n : ℕ} {R : Type u_1} [CommMonoid R] {m : ℕ} (s : Fin n → Bool) (t : Fin m → Bool) (a : Rˣ) : stateWeight (Fin.append s t) a = stateWeight s a * stateWeight t a

Concatenating states multiplies their weights.

@[simp]

theorem TauCeti.PDCode.stateWeight_not {n : ℕ} {R : Type u_1} [CommMonoid R] (s : Fin n → Bool) (a : Rˣ) : stateWeight (fun (i : Fin n) => !s i) a = (stateWeight s a)⁻¹

Negating a state inverts its weight, since it exchanges the A- and B-smoothings.

@[simp]

theorem TauCeti.PDCode.stateWeight_inv {n : ℕ} {R : Type u_1} [CommMonoid R] (s : Fin n → Bool) (a : Rˣ) : stateWeight s a⁻¹ = (stateWeight s a)⁻¹

Inverting the unit inverts every state weight.

@[simp]

theorem TauCeti.PDCode.stateWeight_comp {n : ℕ} {R : Type u_1} [CommMonoid R] {m : ℕ} (s : Fin m → Bool) (a : Rˣ) (cross : Fin n ≃ Fin m) : stateWeight (s ∘ ⇑cross) a = stateWeight s a

Transporting a state along a relabelling of the crossings preserves its weight.

@[simp]

theorem TauCeti.PDCode.stateWeight_snoc {n : ℕ} {R : Type u_1} [CommMonoid R] (s : Fin n → Bool) (c : Bool) (a : Rˣ) : stateWeight (Fin.snoc s c) a = stateWeight s a * bif c then a else a⁻¹

Extending a state by a choice at a new last crossing multiplies its weight by the weight of that choice.

noncomputable def TauCeti.PDCode.kauffmanBracket {n : ℕ} {R : Type u_1} [CommRing R] (D : PDCode n) (a : Rˣ) : R

The Kauffman bracket of a PD-code at a unit a: the sum, over all 2 ^ n states, of the weight of the state times the loop value TauCeti.TemperleyLieb.jonesDelta a raised to one less than the number of circles of the smoothed diagram. This is Lickorish's normalisation ⟨unknot⟩ = 1; with truncated subtraction the empty diagram also has bracket 1.

Equations

• D.kauffmanBracket a = ∑ s : Fin n → Bool, ↑(TauCeti.PDCode.stateWeight s a) * TauCeti.TemperleyLieb.jonesDelta a ^ (D.stateLoopCount s - 1)

theorem TauCeti.PDCode.kauffmanBracket_def {n : ℕ} {R : Type u_1} [CommRing R] (D : PDCode n) (a : Rˣ) : D.kauffmanBracket a = ∑ s : Fin n → Bool, ↑(stateWeight s a) * TemperleyLieb.jonesDelta a ^ (D.stateLoopCount s - 1)

The defining state-sum equation of the Kauffman bracket.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_relabel {n : ℕ} {R : Type u_1} [CommRing R] {m : ℕ} (D : PDCode n) (a : Rˣ) (half : Fin (4 * n) ≃ Fin (4 * m)) (cross : Fin n ≃ Fin m) : (D.relabel half cross).kauffmanBracket a = D.kauffmanBracket a

The Kauffman bracket depends on a PD-code only through its relabelling class.

@[simp]

theorem TauCeti.PDCode.kauffmanBracket_mirror {n : ℕ} {R : Type u_1} [CommRing R] (D : PDCode n) (a : Rˣ) : D.mirror.kauffmanBracket a = D.kauffmanBracket a⁻¹

Mirroring a PD-code inverts the unit in its Kauffman bracket.

theorem TauCeti.PDCode.kauffmanBracket_eq_jonesDelta_pow {R : Type u_1} [CommRing R] (D : PDCode 0) (a : Rˣ) : D.kauffmanBracket a = TemperleyLieb.jonesDelta a ^ (D.crossinglessComponentCount - 1)

A PD-code with no crossings and c crossing-free circles has Kauffman bracket δ ^ (c - 1). This pins the normalisation of TauCeti.PDCode.kauffmanBracket: the unknot has bracket 1, and each further circle contributes one factor of the loop value.

@[simp]

theorem TauCeti.PDCode.kink_smoothingTurn (b : Fin 1 → Bool) (i : Fin 1) (t : Fin 4) : (kink.smoothingTurn b) ((crossingSlotEquiv 1) (i, t)) = (crossingSlotEquiv 1) (i, (slotSmoothing (b i)) t)

Smoothing the kink reconnects its slots by the chosen local smoothing.

theorem TauCeti.PDCode.stateLoopCount_kink_true : (kink.stateLoopCount fun (x : Fin 1) => true) = 2

The A-smoothing of the kink leaves two circles.

theorem TauCeti.PDCode.stateLoopCount_kink_false : (kink.stateLoopCount fun (x : Fin 1) => false) = 1

The B-smoothing of the kink leaves one circle.

theorem TauCeti.PDCode.kauffmanBracket_kink {R : Type u_1} [CommRing R] (a : Rˣ) : kink.kauffmanBracket a = -↑a ^ 3

The Kauffman bracket of the kink is -a ^ 3, that is, -a ^ 3 times that of the unknot. The two smoothings of the single crossing contribute a * δ and a⁻¹, and the loop value collapses their sum to -a ^ 3: this is the framing factor by which the bracket fails to be invariant under the first Reidemeister move.

noncomputable def TauCeti.OrientedPDCode.normalizedKauffmanBracket {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (a : Rˣ) : R

The writhe-normalized Kauffman bracket. Its correction factor is a unit, so the definition makes sense over every commutative ring and does not require the bracket value itself to be invertible.

Equations

• D.normalizedKauffmanBracket a = ↑((-a ^ 3) ^ (-D.writhe)) * D.kauffmanBracket a

theorem TauCeti.OrientedPDCode.normalizedKauffmanBracket_def {n : ℕ} {R : Type u_1} [CommRing R] (D : OrientedPDCode n) (a : Rˣ) : D.normalizedKauffmanBracket a = ↑((-a ^ 3) ^ (-D.writhe)) * D.kauffmanBracket a

The writhe-normalized Kauffman bracket is the bracket multiplied by its writhe correction factor.