The circles of two smoothings differing at one crossing

An edge of the cube of resolutions of a PD-code joins two states s and t that agree at every crossing except one crossing c. This file compares the circles of the two smoothed diagrams.

Smoothing only reconnects the four half-edges D.crossing c k at the crossing c, so a circle avoiding these four half-edges is a circle of both smoothings: it consists of the same half-edges in both (TauCeti.PDCode.eqvGen_circleStep_iff_of_notMem_circlesAt). This gives the bijection TauCeti.PDCode.unchangedCircleEquiv between the circles of s and of t that do not pass through c. The circles passing through c, TauCeti.PDCode.circlesAt D s c, are the circles of the two half-edges in the opposite slots 0 and 2, since each local smoothing joins every slot to one of its two neighbours. So one or two circles of each smoothing pass through c.

They are never two for both smoothings when s c ≠ t c (TauCeti.PDCode.card_circlesAt_add_card_circlesAt_le_three). Delete the smoothing arcs at c from either smoothed diagram: the half-edge x = D.crossing c 0 lies on a component of what remains, the same for s and for t. If two circles of each smoothing passed through c, that component would meet the four half-edges at c in x alone. It is closed under the arc matching, so it has an even number of half-edges, and away from c it is closed under the remaining smoothing arcs, so it has an even number of half-edges other than x; this is impossible.

So the circles passing through c change in one of three ways: two circles of s merge into one circle of t, one circle of s splits into two circles of t, or one circle is replaced by one circle. Nothing here uses planarity. For planar codes the last case does not occur, but it does for the nonplanar code of two circles meeting in a single crossing. Whenever only one circle of t passes through c, sending the circle of a half-edge to its circle in t is a well-defined map TauCeti.PDCode.saddleCircleMap: it is the unchanged-circle bijection away from c and collapses the circles of s through c onto the circle of t through c. It is the correspondence of circles along which the saddle cobordism of a merge acts, and in reverse that of a split.

Main definitions

• TauCeti.PDCode.circlesAt: the circles of a smoothed diagram passing through a crossing.
• TauCeti.PDCode.unchangedCircleEquiv: the circles avoiding the crossing c are the same for two states agreeing away from c.
• TauCeti.PDCode.saddleCircleMap: the correspondence of circles when one circle of the target passes through c.

Main results

• TauCeti.PDCode.circlesAt_eq_pair: the circles through c are those of the half-edges in slots 0 and 2; in particular there are one or two of them (TauCeti.PDCode.card_circlesAt_le_two).
• TauCeti.PDCode.card_circlesAt_add_card_circlesAt_le_three: two states differing exactly at c do not both have two circles through c; if one has two, the other has one (TauCeti.PDCode.card_circlesAt_eq_one_of_card_circlesAt_eq_two).
• TauCeti.PDCode.stateLoopCount_add_card_circlesAt: the change in the number of circles is the change in the number of circles through c; in particular it is at most one (TauCeti.PDCode.stateLoopCount_le_stateLoopCount_add_one).
• TauCeti.PDCode.eqvGen_circleStep_of_forall_card_circlesAt_eq_one: if only one circle of t passes through each crossing at which s and t differ, every circle of s lies on a circle of t.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), 359-426, §2 and §4.2 (the circles of neighbouring resolutions and the merge and split maps).
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), 337-370, §2.

The circles through a crossing

def TauCeti.PDCode.circlesAt {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) : Finset (D.CrossingCircle s)

The circles of the diagram smoothed according to the state s that pass through the crossing c: the circles of the four half-edges at c.

theorem TauCeti.PDCode.mem_circlesAt {n : ℕ} {D : PDCode n} {s : Fin n → Bool} {c : Fin n} {C : D.CrossingCircle s} : C ∈ D.circlesAt s c ↔ ∃ (k : Fin 4), ⟦D.crossing c k⟧ = C

A circle passes through the crossing c when it is the circle of a half-edge at c.

theorem TauCeti.PDCode.mk_crossing_mem_circlesAt {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) (k : Fin 4) : ⟦D.crossing c k⟧ ∈ D.circlesAt s c

The circle of a half-edge at the crossing c passes through c.

theorem TauCeti.PDCode.circlesAt_eq_pair {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) : D.circlesAt s c = {⟦D.crossing c 0⟧, ⟦D.crossing c 2⟧}

The circles through the crossing c are the circles of the half-edges in the opposite slots 0 and 2: each local smoothing joins the other two slots to one of these.

theorem TauCeti.PDCode.circlesAt_nonempty {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) : (D.circlesAt s c).Nonempty

Some circle passes through the crossing c.

theorem TauCeti.PDCode.card_circlesAt_le_two {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) : (D.circlesAt s c).card ≤ 2

At most two circles pass through a crossing.

theorem TauCeti.PDCode.card_circlesAt_eq_two_iff {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) : (D.circlesAt s c).card = 2 ↔ ⟦D.crossing c 0⟧ ≠ ⟦D.crossing c 2⟧

Two circles pass through the crossing c exactly when the half-edges in the opposite slots 0 and 2 lie on different circles.

theorem TauCeti.PDCode.card_circlesAt_eq_one_iff {n : ℕ} (D : PDCode n) (s : Fin n → Bool) (c : Fin n) : (D.circlesAt s c).card = 1 ↔ ⟦D.crossing c 0⟧ = ⟦D.crossing c 2⟧

One circle passes through the crossing c exactly when the half-edges in the opposite slots 0 and 2 lie on one circle.

The circles avoiding the crossing

theorem TauCeti.PDCode.eqvGen_circleStep_iff_of_notMem_circlesAt {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) {x : Fin (4 * n)} (hx : ⟦x⟧ ∉ D.circlesAt s c) {y : Fin (4 * n)} : Relation.EqvGen (D.CircleStep s) x y ↔ Relation.EqvGen (D.CircleStep t) x y

A circle avoiding the crossing c is a circle of every state agreeing away from c. If the circle of x in the smoothing s does not pass through c, then the half-edges on the circle of x are the same for the smoothings s and t.

theorem TauCeti.PDCode.mk_notMem_circlesAt_of_notMem {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) {x : Fin (4 * n)} (hx : ⟦x⟧ ∉ D.circlesAt s c) : ⟦x⟧ ∉ D.circlesAt t c

A circle of s avoiding the crossing c is a circle of t avoiding c.

noncomputable def TauCeti.PDCode.unchangedCircleEquiv {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) : { C : D.CrossingCircle s // C ∉ D.circlesAt s c } ≃ { C : D.CrossingCircle t // C ∉ D.circlesAt t c }

The unchanged circles. For two states agreeing away from the crossing c, the circles avoiding c are the same: the circle of a half-edge in one smoothing corresponds to its circle in the other (TauCeti.PDCode.coe_unchangedCircleEquiv_mk).

@[simp]

theorem TauCeti.PDCode.coe_unchangedCircleEquiv_mk {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) {x : Fin (4 * n)} (hx : ⟦x⟧ ∉ D.circlesAt s c) : ↑((D.unchangedCircleEquiv hst) ⟨⟦x⟧, hx⟩) = ⟦x⟧

The unchanged-circle bijection sends the circle of a half-edge to its circle in the other smoothing.

@[simp]

theorem TauCeti.PDCode.coe_unchangedCircleEquiv_symm_mk {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) {x : Fin (4 * n)} (hx : ⟦x⟧ ∉ D.circlesAt t c) : ↑((D.unchangedCircleEquiv hst).symm ⟨⟦x⟧, hx⟩) = ⟦x⟧

The inverse of the unchanged-circle bijection sends the circle of a half-edge to its circle in the first smoothing.

theorem TauCeti.PDCode.unchangedCircleEquiv_symm {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) : (D.unchangedCircleEquiv hst).symm = D.unchangedCircleEquiv ⋯

The inverse of the unchanged-circle bijection is the unchanged-circle bijection in the other direction.

theorem TauCeti.PDCode.stateLoopCount_add_card_circlesAt {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) : D.stateLoopCount s + (D.circlesAt t c).card = D.stateLoopCount t + (D.circlesAt s c).card

The number of circles changes as the number of circles through the crossing does.

theorem TauCeti.PDCode.stateLoopCount_le_stateLoopCount_add_one {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) : D.stateLoopCount t ≤ D.stateLoopCount s + 1

The number of circles changes by at most one along an edge of the cube of resolutions.

theorem TauCeti.PDCode.stateLoopCount_le_add_card_filter_ne {n : ℕ} (D : PDCode n) (s t : Fin n → Bool) : D.stateLoopCount t ≤ D.stateLoopCount s + {i : Fin n | s i ≠ t i}.card

Changing the smoothings at a set of crossings increases the number of circles by at most the number of changed crossings. No planarity assumption is needed.

The circles through the crossing

theorem TauCeti.PDCode.card_circlesAt_add_card_circlesAt_le_three {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (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

Two states differing exactly at a crossing do not both have two circles through it. So along an edge of the cube of resolutions two circles merge into one, one circle splits into two, or one circle through the crossing is replaced by one circle.

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

If two circles of s pass through the crossing c at which s and t differ, then only one circle of t does: the two circles of s merge.

Coarser smoothings

theorem TauCeti.PDCode.eqvGen_circleStep_of_forall_card_circlesAt_eq_one {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} (h : ∀ (j : Fin n), s j ≠ t j → (D.circlesAt t j).card = 1) {x y : Fin (4 * n)} (hxy : Relation.EqvGen (D.CircleStep s) x y) : Relation.EqvGen (D.CircleStep t) x y

If only one circle of t passes through each crossing at which s and t differ, then half-edges on one circle of s lie on one circle of t.

The saddle correspondence

theorem TauCeti.PDCode.eqvGen_circleStep_of_card_circlesAt_eq_one {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) {x y : Fin (4 * n)} (h : Relation.EqvGen (D.CircleStep s) x y) : Relation.EqvGen (D.CircleStep t) x y

If only one circle of t passes through the crossing c, then half-edges on one circle of s lie on one circle of t.

def TauCeti.PDCode.saddleCircleMap {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) : D.CrossingCircle s → D.CrossingCircle t

The saddle correspondence of circles. When only one circle of t passes through the crossing c, the circle of a half-edge in the smoothing s determines its circle in the smoothing t (TauCeti.PDCode.saddleCircleMap_mk). This map is the unchanged-circle bijection away from c (TauCeti.PDCode.saddleCircleMap_of_notMem) and sends the circles of s through c onto the circle of t through c (TauCeti.PDCode.image_saddleCircleMap_circlesAt).

@[simp]

theorem TauCeti.PDCode.saddleCircleMap_mk {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (x : Fin (4 * n)) : D.saddleCircleMap hst ht ⟦x⟧ = ⟦x⟧

The saddle correspondence sends the circle of a half-edge to its circle in the target.

theorem TauCeti.PDCode.saddleCircleMap_surjective {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) : Function.Surjective (D.saddleCircleMap hst ht)

Every circle of the target comes from a circle of the source.

theorem TauCeti.PDCode.saddleCircleMap_of_notMem {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) {C : D.CrossingCircle s} (hC : C ∉ D.circlesAt s c) : D.saddleCircleMap hst ht C = ↑((D.unchangedCircleEquiv hst) ⟨C, hC⟩)

Away from the crossing, the saddle correspondence is the unchanged-circle bijection.

theorem TauCeti.PDCode.image_saddleCircleMap_circlesAt {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) : Finset.image (D.saddleCircleMap hst ht) (D.circlesAt s c) = D.circlesAt t c

The saddle correspondence sends the circles of the source through the crossing onto the circle of the target through the crossing.

theorem TauCeti.PDCode.saddleCircleMap_saddleCircleMap {n : ℕ} (D : PDCode n) {s t : Fin n → Bool} {c : Fin n} (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (ht : (D.circlesAt t c).card = 1) (hs : (D.circlesAt s c).card = 1) (C : D.CrossingCircle s) : D.saddleCircleMap ⋯ hs (D.saddleCircleMap hst ht C) = C

When only one circle of each state passes through the crossing, the saddle correspondences in the two directions are mutually inverse.