Planar cube edges merge or split circles

Along an edge of the cube of resolutions, from a state s to the state t differing from it only at the crossing c, two circles of s through c merge into one circle of t, one circle of s through c splits into two circles of t, or one circle through c is replaced by one circle (TauCeti.PDCode.card_circlesAt_add_card_circlesAt_le_three). The last case occurs for the nonplanar code of two circles meeting in a single crossing. This file proves that it never occurs for a planar code: then exactly three circles pass through c in the two smoothings together (TauCeti.PDCode.IsPlanar.card_circlesAt_add_card_circlesAt_eq_three), so every edge of the cube of resolutions is a merge or a split, and the number of circles changes by exactly one. These are the two kinds of edges carrying the merge and split maps of the Khovanov complex.

Main results

• TauCeti.PDCode.IsPlanar.card_circlesAt_add_card_circlesAt_eq_three: for a planar code, three circles pass through the crossing at which two states differ, in the two smoothings together.
• TauCeti.PDCode.IsPlanar.card_circlesAt_eq_two_or_card_circlesAt_eq_two: every edge of the cube of resolutions of a planar code is a merge or a split.
• TauCeti.PDCode.IsPlanar.stateLoopCount_eq_add_one_or_stateLoopCount_eq_add_one: along every edge the number of circles changes by exactly one.

Implementation notes

The proof is a finite Euler-characteristic count, read off from the transposition bound TauCeti.card_add_orbitCount_le_length_add_two_mul_card_orbits. Smoothing the crossings according to s gives the perfect matching σ of the half-edges, and the rotation ρ to the next slot at each crossing is σ * (σ * ρ), where σ * ρ transposes two opposite slots at each crossing. So the face permutation α * ρ of the underlying graph, with α the arc matching, is conjugate to (σ * ρ) * (α * σ), and α * σ is the inverse of the traversal TauCeti.PDCode.statePerm, whose cycles are the circles of s in both directions of travel. Writing this product with n transpositions for σ * ρ, and 2 * n each for α and σ, the bound is Euler's bound TauCeti.PDCode.faceCount_le, attained exactly by planar codes.

Now suppose one circle of s and one circle of t pass through c. Then the two slots x and y transposed by σ * ρ at c lie on one circle of s, but they do not lie on one directed traversal orbit: otherwise, the reversal of directed orbits along the smoothing would put the other two slots at c on one other directed orbit, and resmoothing c would split both, leaving t one circle more than s. A transposition joining two directed orbits of one circle merges two faces without joining two components, so the bound is not attained (TauCeti.card_add_orbitCount_add_two_le_length_add_two_mul_card_orbits), and the code is not planar.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), 359-426, §2 and §4.2 (the merge and split maps on the edges of the cube).
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), 337-370, §2.
• S. K. Lando, A. K. Zvonkin, Graphs on Surfaces and Their Applications, Encyclopaedia of Mathematical Sciences 141, Springer 2004, §1.3 (faces of rotation systems).

The crossing transpositions of a smoothing

Joining two directed orbits of a circle is not planar

One circle through a crossing in both smoothings

Planar cube edges

theorem TauCeti.PDCode.IsPlanar.card_circlesAt_add_card_circlesAt_eq_three {n : ℕ} {D : PDCode n} {s t : Fin n → Bool} {c : Fin n} (hD : D.IsPlanar) (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c) : (D.circlesAt s c).card + (D.circlesAt t c).card = 3

Every edge of the cube of resolutions of a planar code is a merge or a split. If two states differ exactly at the crossing c of a planar code, then three circles pass through c in the two smoothings together: two circles of one smoothing and one circle of the other.

theorem TauCeti.PDCode.IsPlanar.card_circlesAt_eq_two_or_card_circlesAt_eq_two {n : ℕ} {D : PDCode n} {s t : Fin n → Bool} {c : Fin n} (hD : D.IsPlanar) (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c) : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2

Every edge of the cube of resolutions of a planar code is a merge or a split. If two states differ exactly at the crossing c of a planar code, then two circles pass through c in one of the two smoothings: two circles of s merge into one circle of t, or one circle of s splits into two circles of t.

theorem TauCeti.PDCode.IsPlanar.stateLoopCount_eq_add_one_or_stateLoopCount_eq_add_one {n : ℕ} {D : PDCode n} {s t : Fin n → Bool} {c : Fin n} (hD : D.IsPlanar) (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c) : D.stateLoopCount s = D.stateLoopCount t + 1 ∨ D.stateLoopCount t = D.stateLoopCount s + 1

Along every edge of the cube of resolutions of a planar code, the number of circles changes by exactly one.

theorem TauCeti.PDCode.IsPlanar.card_false_add_stateLoopCount_mod_two_eq {n : ℕ} {D : PDCode n} (hD : D.IsPlanar) (s t : Fin n → Bool) : ({i : Fin n | s i = false}.card + D.stateLoopCount s) % 2 = ({i : Fin n | t i = false}.card + D.stateLoopCount t) % 2

For a planar diagram, the sum of the number of B-smoothings and the number of resolution circles has the same parity at every vertex of the resolution cube.