Commuting faces of the cube of resolutions

A face of the cube of resolutions of a PD-code consists of four states: s, the states t₁ and t₂ obtained by changing s at the crossings c and c' respectively, and the state u changed at both. Each edge carries the merge map TauCeti.PDCode.resolutionMergeMap when two circles pass through its crossing in its source, and the split map TauCeti.PDCode.resolutionSplitMap when two pass through it in its target. This file proves that the two composites around a face agree whenever all four edges are merges or splits:

• both routes merge twice (associativity, including merges of disjoint pairs of circles);
• both routes split twice (coassociativity);
• one route merges and then splits while the other splits and then merges (the Frobenius relation);
• both routes merge and then split, as for two crossings joining the same two circles;
• both routes split and then merge, as for two interleaved crossings on one circle, where both composites multiply by 2X on that circle.

Up to exchanging the two routes, these are all the faces in which every edge is a merge or a split: each edge changes the number of circles by one, so the numbers of circles of s and u determine whether the routes merge twice, split twice, or do one of each. All identities are stated for the unsigned maps, with every crossing-free circle retained; the cube signs are supplied separately.

The proofs are algebraic. Merges along successive saddles compose to the merge along the composite circle correspondence, and dually for splits. The mixed faces follow from the projection formula TauCeti.Khovanov.fiberwiseSplit_fiberwiseMul_mul, which reduces each composite to multiplication by a merged image of the split X ⊗ 1 + 1 ⊗ X of the unit. The combinatorial input is that all four smoothings are quotients of the same half-edges, so every circle correspondence sends the circle of a half-edge to its circle; when one state has a single circle through each crossing at which it differs from another, TauCeti.PDCode.coarseningResolvedCircleMap compares them directly.

Main results

All in the namespace TauCeti.PDCode:

• resolutionMergeMap_comp_resolutionMergeMap_comm: faces of two merges.
• resolutionSplitMap_comp_resolutionSplitMap_comm: faces of two splits.
• resolutionSplitMap_comp_resolutionMergeMap_eq_resolutionMergeMap_comp_resolutionSplitMap: a merge followed by a split equals a split followed by a merge.
• resolutionSplitMap_comp_resolutionMergeMap_comm: faces in which both routes merge and then split.
• resolutionMergeMap_comp_resolutionSplitMap_comm: faces in which both routes split and then merge.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), §2.
• D. Bar-Natan, On Khovanov's categorification of the Jones polynomial, Algebr. Geom. Topol. 2 (2002), §2.

theorem TauCeti.PDCode.resolutionMergeMap_comp_resolutionMergeMap_comm {n : ℕ} (D : PDCode n) {s t₁ t₂ u : Fin n → Bool} {c c' : Fin n} (hst₁ : ∀ (j : Fin n), j ≠ c → s j = t₁ j) (hc₁ : s c ≠ t₁ c) (ht₁u : ∀ (j : Fin n), j ≠ c' → t₁ j = u j) (hc₁' : t₁ c' ≠ u c') (hst₂ : ∀ (j : Fin n), j ≠ c' → s j = t₂ j) (hc₂ : s c' ≠ t₂ c') (ht₂u : ∀ (j : Fin n), j ≠ c → t₂ j = u j) (hc₂' : t₂ c ≠ u c) (R : Type u) [CommSemiring R] (hs : (D.circlesAt s c).card = 2) (ht₁ : (D.circlesAt t₁ c').card = 2) (hs' : (D.circlesAt s c').card = 2) (ht₂ : (D.circlesAt t₂ c).card = 2) : (D.resolutionMergeMap ht₁u hc₁' ht₁ R).comp (D.resolutionMergeMap hst₁ hc₁ hs R) = (D.resolutionMergeMap ht₂u hc₂' ht₂ R).comp (D.resolutionMergeMap hst₂ hc₂ hs' R)

Associativity. If both routes around a face merge twice, the two composite merges agree: both multiply the factors on each circle of u coming from the circles of s on it.

theorem TauCeti.PDCode.resolutionSplitMap_comp_resolutionSplitMap_comm {n : ℕ} (D : PDCode n) {s t₁ t₂ u : Fin n → Bool} {c c' : Fin n} (hst₁ : ∀ (j : Fin n), j ≠ c → s j = t₁ j) (hc₁ : s c ≠ t₁ c) (ht₁u : ∀ (j : Fin n), j ≠ c' → t₁ j = u j) (hc₁' : t₁ c' ≠ u c') (hst₂ : ∀ (j : Fin n), j ≠ c' → s j = t₂ j) (hc₂ : s c' ≠ t₂ c') (ht₂u : ∀ (j : Fin n), j ≠ c → t₂ j = u j) (hc₂' : t₂ c ≠ u c) (R : Type u) [CommSemiring R] (ht₁ : (D.circlesAt t₁ c).card = 2) (hu : (D.circlesAt u c').card = 2) (ht₂ : (D.circlesAt t₂ c').card = 2) (hu' : (D.circlesAt u c).card = 2) : D.resolutionSplitMap ht₁u hc₁' hu R ∘ₗ D.resolutionSplitMap hst₁ hc₁ ht₁ R = D.resolutionSplitMap ht₂u hc₂' hu' R ∘ₗ D.resolutionSplitMap hst₂ hc₂ ht₂ R

Coassociativity. If both routes around a face split twice, the two composite splits agree.

theorem TauCeti.PDCode.resolutionSplitMap_comp_resolutionMergeMap_eq_resolutionMergeMap_comp_resolutionSplitMap {n : ℕ} (D : PDCode n) {s t₁ t₂ u : Fin n → Bool} {c c' : Fin n} (hst₁ : ∀ (j : Fin n), j ≠ c → s j = t₁ j) (hc₁ : s c ≠ t₁ c) (ht₁u : ∀ (j : Fin n), j ≠ c' → t₁ j = u j) (hc₁' : t₁ c' ≠ u c') (hst₂ : ∀ (j : Fin n), j ≠ c' → s j = t₂ j) (hc₂ : s c' ≠ t₂ c') (ht₂u : ∀ (j : Fin n), j ≠ c → t₂ j = u j) (hc₂' : t₂ c ≠ u c) (R : Type u) [CommSemiring R] (hs : (D.circlesAt s c).card = 2) (hu : (D.circlesAt u c').card = 2) (ht₂ : (D.circlesAt t₂ c').card = 2) (ht₂' : (D.circlesAt t₂ c).card = 2) : D.resolutionSplitMap ht₁u hc₁' hu R ∘ₗ (D.resolutionMergeMap hst₁ hc₁ hs R).toLinearMap = (D.resolutionMergeMap ht₂u hc₂' ht₂' R).toLinearMap ∘ₗ D.resolutionSplitMap hst₂ hc₂ ht₂ R

The Frobenius relation on a face. Merging at c and then splitting at c' equals splitting at c' and then merging at c.

theorem TauCeti.PDCode.resolutionSplitMap_comp_resolutionMergeMap_comm {n : ℕ} (D : PDCode n) {s t₁ t₂ u : Fin n → Bool} {c c' : Fin n} (hst₁ : ∀ (j : Fin n), j ≠ c → s j = t₁ j) (hc₁ : s c ≠ t₁ c) (ht₁u : ∀ (j : Fin n), j ≠ c' → t₁ j = u j) (hc₁' : t₁ c' ≠ u c') (hst₂ : ∀ (j : Fin n), j ≠ c' → s j = t₂ j) (hc₂ : s c' ≠ t₂ c') (ht₂u : ∀ (j : Fin n), j ≠ c → t₂ j = u j) (hc₂' : t₂ c ≠ u c) (R : Type u) [CommSemiring R] (hs : (D.circlesAt s c).card = 2) (hu : (D.circlesAt u c').card = 2) (hs' : (D.circlesAt s c').card = 2) (hu' : (D.circlesAt u c).card = 2) : D.resolutionSplitMap ht₁u hc₁' hu R ∘ₗ (D.resolutionMergeMap hst₁ hc₁ hs R).toLinearMap = D.resolutionSplitMap ht₂u hc₂' hu' R ∘ₗ (D.resolutionMergeMap hst₂ hc₂ hs' R).toLinearMap

Merging and then splitting along both routes. If both routes around a face merge and then split, the two composites agree. This is the face of two crossings joining the same two circles in a planar diagram.

theorem TauCeti.PDCode.resolutionMergeMap_comp_resolutionSplitMap_comm {n : ℕ} (D : PDCode n) {s t₁ t₂ u : Fin n → Bool} {c c' : Fin n} (hst₁ : ∀ (j : Fin n), j ≠ c → s j = t₁ j) (hc₁ : s c ≠ t₁ c) (ht₁u : ∀ (j : Fin n), j ≠ c' → t₁ j = u j) (hc₁' : t₁ c' ≠ u c') (hst₂ : ∀ (j : Fin n), j ≠ c' → s j = t₂ j) (hc₂ : s c' ≠ t₂ c') (ht₂u : ∀ (j : Fin n), j ≠ c → t₂ j = u j) (hc₂' : t₂ c ≠ u c) (R : Type u) [CommSemiring R] (ht₁ : (D.circlesAt t₁ c).card = 2) (ht₁' : (D.circlesAt t₁ c').card = 2) (ht₂ : (D.circlesAt t₂ c').card = 2) (ht₂' : (D.circlesAt t₂ c).card = 2) : (D.resolutionMergeMap ht₁u hc₁' ht₁' R).toLinearMap ∘ₗ D.resolutionSplitMap hst₁ hc₁ ht₁ R = (D.resolutionMergeMap ht₂u hc₂' ht₂' R).toLinearMap ∘ₗ D.resolutionSplitMap hst₂ hc₂ ht₂ R

Splitting and then merging along both routes. If both routes around a face split and then merge, the two composites agree: after identifying the circles of s with those of u, both multiply by 2X on the circle of u through c and c'. This is the face of two interleaved crossings on one circle in a planar diagram.