Enhanced states and the Jones polynomial

An enhanced state of a PD-code is a state s together with a label 1 or X on every circle of the diagram smoothed according to s. The enhanced states form the standard basis of the Khovanov chain groups (Bar-Natan §1), and this file fixes their bigrading. A state selects the B-smoothing at the crossings S where it is false. For an oriented code with n₊ positive and n₋ negative crossings, the enhanced state has cochain degree |S| - n₋. Its quantum degree is |S| + n₊ - 2 n₋ plus 1 for each circle labelled 1 and minus 1 for each circle labelled X (TauCeti.OrientedPDCode.stateCochainDegree, TauCeti.OrientedPDCode.enhancedQuantumDegree).

The signed count of enhanced states by bidegree is the sum TauCeti.OrientedPDCode.enhancedStateSum of (-1) ^ i q ^ j over all enhanced states; here the generator T of ℤ[T;T⁻¹] plays the role of q. With Cⁱʲ the Khovanov chain group, the free module on the enhanced states of bidegree (i, j), this sum is the graded Euler characteristic ∑ (-1) ^ i q ^ j rank Cⁱʲ. This file proves that, for a nonempty diagram, this sum is the Jones polynomial in Khovanov's normalization: with the substitution t ^ (1/2) ↦ -q, it is (q + q⁻¹) times TauCeti.OrientedPDCode.jonesPolynomial (TauCeti.OrientedPDCode.enhancedStateSum_eq_mul_eval₂_jonesPolynomial).

The proof is a state-by-state comparison. Summing over the labels of the k circles of a state gives (q + q⁻¹) ^ k. The substitution turns the Jones weight of a state into the signed monomial (-1) ^ (|S| - n₋) q ^ (|S| + n₊ - 2 n₋), crossing by crossing. The Jones state sum raises the loop value only to the truncated power k - 1, so the extra factor q + q⁻¹ completes it to the k-th power exactly when every state has a circle, that is, when the diagram is nonempty. The empty diagram has a single enhanced state and sum 1 (TauCeti.OrientedPDCode.enhancedStateSum_empty). More generally, a diagram without crossings and with c circles has sum (q + q⁻¹) ^ c (TauCeti.OrientedPDCode.enhancedStateSum_eq_pow).

Main definitions

• TauCeti.PDCode.EnhancedState: a state with a 1/X label on every resolved circle.
• TauCeti.Khovanov.labelingQuantumDegree: the quantum degree contributed by the circle labels.
• TauCeti.OrientedPDCode.stateCochainDegree: the cochain degree |S| - n₋ of a state.
• TauCeti.OrientedPDCode.stateQuantumShift: the quantum shift |S| + n₊ - 2 n₋ of a state.
• TauCeti.OrientedPDCode.enhancedQuantumDegree: the quantum degree of an enhanced state.
• TauCeti.OrientedPDCode.enhancedStateSum: the signed sum of q ^ j over all enhanced states.

Main results

• TauCeti.Khovanov.sum_T_labelingQuantumDegree: the labellings of k circles, counted by quantum degree, give (q + q⁻¹) ^ k.
• TauCeti.OrientedPDCode.enhancedStateSum_eq_sum: the sum over enhanced states as a sum over states, with (q + q⁻¹) ^ k for a state with k circles.
• TauCeti.OrientedPDCode.eval₂_neg_genericUnit_jonesStateWeight: at t ^ (1/2) = -q the Jones weight of a state is (-1) ^ (|S| - n₋) q ^ (|S| + n₊ - 2 n₋).
• TauCeti.OrientedPDCode.enhancedStateSum_eq_mul_eval₂_jonesPolynomial: for a nonempty diagram the enhanced state sum is (q + q⁻¹) times the Jones polynomial at t ^ (1/2) = -q.
• TauCeti.OrientedPDCode.enhancedStateSum_eq_pow, TauCeti.OrientedPDCode.enhancedStateSum_empty: the crossing-free diagrams, including the empty one.
• TauCeti.enhancedStateSum_rightHandedTrefoilPDCode: the right-handed trefoil has enhanced state sum q + q³ + q⁵ - q⁹.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), 359-426.
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), 337-370, §1 (enhanced states, the bigrading, and the unnormalized Jones polynomial (q + q⁻¹) J).

@[reducible, inline]

abbrev TauCeti.PDCode.EnhancedState {n : ℕ} (D : PDCode n) : Type

An enhanced state of a PD-code: a state s, together with a label on every circle of the diagram smoothed according to s. The label false stands for the generator 1 and true for the generator X of the rank-two Khovanov module.

def TauCeti.Khovanov.labelingQuantumDegree (ι : Type u_1) [Fintype ι] (l : ι → Bool) : ℤ

The quantum degree of a labelling of the circles: +1 for each circle labelled 1 and -1 for each circle labelled X.

theorem TauCeti.Khovanov.labelingQuantumDegree_def {ι : Type u_1} [Fintype ι] (l : ι → Bool) : labelingQuantumDegree ι l = ∑ i : ι, bif l i then -1 else 1

The defining sum of the quantum degree of a labelling.

@[simp]

theorem TauCeti.Khovanov.labelingQuantumDegree_not {ι : Type u_1} [Fintype ι] (l : ι → Bool) : (labelingQuantumDegree ι fun (i : ι) => !l i) = -labelingQuantumDegree ι l

Complementary labellings have opposite quantum degrees.

theorem TauCeti.Khovanov.labelingQuantumDegree_eq {ι : Type u_1} [Fintype ι] (l : ι → Bool) : labelingQuantumDegree ι l = ↑(Fintype.card ι) - 2 * ↑{i : ι | l i = true}.card

The quantum degree of a labelling is the number of circles minus twice the number of X-labels.

theorem TauCeti.Khovanov.abs_labelingQuantumDegree_le {ι : Type u_1} [Fintype ι] (l : ι → Bool) : |labelingQuantumDegree ι l| ≤ ↑(Fintype.card ι)

The quantum degree of a labelling of k circles lies between -k and k.

theorem TauCeti.Khovanov.sum_T_labelingQuantumDegree {ι : Type u_1} [Fintype ι] [DecidableEq ι] : ∑ l : ι → Bool, LaurentPolynomial.T (labelingQuantumDegree ι l) = (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) ^ Fintype.card ι

The graded count of labellings: labelling k circles by 1 or X in all possible ways gives ∑ q ^ (quantum degree) = (q + q⁻¹) ^ k.

theorem TauCeti.Khovanov.labelingQuantumDegree_update_true {ι : Type u_1} [Fintype ι] [DecidableEq ι] {l : ι → Bool} {i : ι} (hi : l i = false) : labelingQuantumDegree ι (Function.update l i true) = labelingQuantumDegree ι l - 2

Relabelling a circle from 1 to X lowers the quantum degree by two.

theorem TauCeti.Khovanov.labelingQuantumDegree_merge {σ : Type u_2} {τ : Type u_3} [Fintype σ] [Fintype τ] [DecidableEq τ] {f : σ → τ} {l : σ → Bool} (h : ∀ (j : τ), {i : σ | f i = j ∧ l i = true}.card ≤ 1) : (labelingQuantumDegree τ fun (j : τ) => decide (∃ (i : σ), f i = j ∧ l i = true)) = labelingQuantumDegree σ l + (↑(Fintype.card τ) - ↑(Fintype.card σ))

When no fibre of f carries two X-labels of l, merging along f changes the quantum degree of l by |τ| - |σ|.

def TauCeti.OrientedPDCode.stateCochainDegree {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : ℤ

The cochain degree |S| - n₋ of a state s of an oriented code, where S is the set of crossings at which s selects the B-smoothing, that is, where s is false.

theorem TauCeti.OrientedPDCode.stateCochainDegree_def {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : D.stateCochainDegree s = ↑{i : Fin n | s i = false}.card - ↑D.negativeCrossingCount

The defining formula of the cochain degree of a state.

def TauCeti.OrientedPDCode.stateQuantumShift {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : ℤ

The quantum shift |S| + n₊ - 2 n₋ of a state s of an oriented code, where S is the set of crossings at which s selects the B-smoothing.

theorem TauCeti.OrientedPDCode.stateQuantumShift_def {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : D.stateQuantumShift s = ↑{i : Fin n | s i = false}.card + ↑D.positiveCrossingCount - 2 * ↑D.negativeCrossingCount

The defining formula of the quantum shift of a state.

def TauCeti.OrientedPDCode.enhancedQuantumDegree {n : ℕ} (D : OrientedPDCode n) (e : D.EnhancedState) : ℤ

The quantum degree of an enhanced state: the quantum shift of its state, plus 1 for each circle labelled 1 and minus 1 for each circle labelled X.

theorem TauCeti.OrientedPDCode.enhancedQuantumDegree_def {n : ℕ} (D : OrientedPDCode n) (e : D.EnhancedState) : D.enhancedQuantumDegree e = D.stateQuantumShift e.fst + Khovanov.labelingQuantumDegree (D.ResolvedCircle e.fst) e.snd

The defining formula of the quantum degree of an enhanced state.

noncomputable def TauCeti.OrientedPDCode.enhancedStateSum {n : ℕ} (D : OrientedPDCode n) : LaurentPolynomial ℤ

The enhanced state sum of an oriented code: the sum of (-1) ^ i q ^ j over all enhanced states, where i is the cochain degree and j the quantum degree, with q = T; that is, the signed count of enhanced states by bidegree. With Cⁱʲ the free module on the enhanced states of bidegree (i, j), this is the graded Euler characteristic ∑ (-1) ^ i q ^ j rank Cⁱʲ.

theorem TauCeti.OrientedPDCode.enhancedStateSum_def {n : ℕ} (D : OrientedPDCode n) : D.enhancedStateSum = ∑ e : D.EnhancedState, (D.stateCochainDegree e.fst).negOnePow • LaurentPolynomial.T (D.enhancedQuantumDegree e)

The defining sum of the enhanced state sum.

theorem TauCeti.OrientedPDCode.enhancedStateSum_eq_sum {n : ℕ} (D : OrientedPDCode n) : D.enhancedStateSum = ∑ s : Fin n → Bool, (D.stateCochainDegree s).negOnePow • LaurentPolynomial.T (D.stateQuantumShift s) * (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) ^ D.stateLoopCount s

The enhanced state sum as a sum over states: the labels of the k circles of a state contribute (q + q⁻¹) ^ k to the signed monomial (-1) ^ (|S| - n₋) q ^ (|S| + n₊ - 2 n₋) of the state.

theorem TauCeti.OrientedPDCode.eval₂_neg_genericUnit_jonesStateWeight {n : ℕ} (D : OrientedPDCode n) (s : Fin n → Bool) : (LaurentPolynomial.eval₂ (Int.castRingHom (LaurentPolynomial ℤ)) (-LaurentPolynomial.genericUnit ℤ)) (D.jonesStateWeight s) = (D.stateCochainDegree s).negOnePow • LaurentPolynomial.T (D.stateQuantumShift s)

The Jones weight of a state at t ^ (1/2) = -q is the signed monomial (-1) ^ (|S| - n₋) q ^ (|S| + n₊ - 2 n₋). Crossing by crossing, a positive crossing contributes q to a state that smooths it by A and -q² to one that smooths it by B, and a negative crossing contributes -q⁻² and q⁻¹.

theorem TauCeti.OrientedPDCode.enhancedStateSum_eq_mul_eval₂_jonesPolynomial {n : ℕ} (D : OrientedPDCode n) (h : 0 < D.componentCount) : D.enhancedStateSum = (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) * (LaurentPolynomial.eval₂ (Int.castRingHom (LaurentPolynomial ℤ)) (-LaurentPolynomial.genericUnit ℤ)) D.jonesPolynomial

The enhanced state sum of a nonempty diagram is (q + q⁻¹) times its Jones polynomial at t ^ (1/2) = -q. The hypothesis 0 < componentCount says that the diagram is nonempty; it excludes the empty diagram, whose enhanced state sum is 1.

theorem TauCeti.OrientedPDCode.enhancedStateSum_eq_pow (D : OrientedPDCode 0) : D.enhancedStateSum = (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) ^ D.crossinglessComponentCount

A diagram without crossings has enhanced state sum (q + q⁻¹) ^ c, where c is the number of its crossing-free circles.

@[simp]

theorem TauCeti.OrientedPDCode.enhancedStateSum_empty : empty.enhancedStateSum = 1

The empty diagram has enhanced state sum 1: its only enhanced state is the empty state with no circles, in bidegree (0, 0).

@[simp]

theorem TauCeti.OrientedPDCode.enhancedStateSum_unknot (orientation : Bool) : (unknot orientation).enhancedStateSum = LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)

The unknot has enhanced state sum q + q⁻¹.

theorem TauCeti.enhancedStateSum_rightHandedTrefoilPDCode : rightHandedTrefoilPDCode.enhancedStateSum = LaurentPolynomial.T 1 + LaurentPolynomial.T 3 + LaurentPolynomial.T 5 - LaurentPolynomial.T 9

The enhanced state sum of the right-handed trefoil is q + q³ + q⁵ - q⁹. This agrees with Khovanov's computation of its homology, whose free summands lie in bidegrees (0, 1), (0, 3), (2, 5) and (3, 9).