Edge maps of the cube of resolutions

Let s and t be states of a PD-code differing exactly at the crossing c. The edge from s to t is a saddle when two circles pass through c in one of the two smoothings; then exactly one circle passes through c in the other, and the edge merges two circles or splits one. The map TauCeti.PDCode.resolutionEdgeMap is the merge TauCeti.PDCode.resolutionMergeMap in the first case and the split TauCeti.PDCode.resolutionSplitMap in the second. These are the unsigned blocks of the Khovanov differential; the cube signs are supplied by the signed totalization CategoryTheory.Functor.cubeComplex.

Every edge of the cube of a planar code is a saddle, while a nonplanar code may have an edge replacing one circle through c by another, on which no map is defined here.

Main results

All in the namespace TauCeti.PDCode:

• resolutionEdgeMap_eq_resolutionMergeMap, resolutionEdgeMap_eq_resolutionSplitMap: the edge map is the merge or the split, according to the smoothing with two circles through c.
• isHomogeneous_resolutionEdgeMap: every edge map has quantum degree -1.
• circleDuality_resolutionEdgeMap: the edge maps in the two directions of an edge are adjoint for the Frobenius pairing of circle tensors.
• SmoothingEquiv.reindex_resolutionEdgeMap: edge maps commute with transport of the smoothed diagrams.
• resolutionEdgeMap_comp_resolutionEdgeMap_comm: the faces of the cube commute. If all four edges of a face are saddles, the two composites around it agree.

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.

noncomputable def TauCeti.PDCode.resolutionEdgeMap {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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] : Khovanov.CircleTensor R (D.ResolvedCircle s) →ₗ[R] Khovanov.CircleTensor R (D.ResolvedCircle t)

The map on resolved-circle tensors along a saddle edge of the cube of resolutions: the merge at c when two circles of s pass through c, and the split at c when two circles of t do. Every other factor, including each crossing-free circle, is transported unchanged.

theorem TauCeti.PDCode.resolutionEdgeMap_def {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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] : D.resolutionEdgeMap hst hc h R = if hs : (D.circlesAt s c).card = 2 then (D.resolutionMergeMap hst hc hs R).toLinearMap else D.resolutionSplitMap hst hc ⋯ R

The edge map merges when two circles of the source pass through c, and splits otherwise.

@[simp]

theorem TauCeti.PDCode.resolutionEdgeMap_eq_resolutionMergeMap {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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] (hs : (D.circlesAt s c).card = 2) : D.resolutionEdgeMap hst hc h R = (D.resolutionMergeMap hst hc hs R).toLinearMap

An edge along which two circles merge carries the resolution merge.

@[simp]

theorem TauCeti.PDCode.resolutionEdgeMap_eq_resolutionSplitMap {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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] (ht : (D.circlesAt t c).card = 2) : D.resolutionEdgeMap hst hc h R = D.resolutionSplitMap hst hc ht R

An edge along which a circle splits carries the resolution split.

theorem TauCeti.PDCode.circleDuality_resolutionEdgeMap {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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] (x : Khovanov.CircleTensor R (D.ResolvedCircle s)) (y : Khovanov.CircleTensor R (D.ResolvedCircle t)) : ((Khovanov.circleDuality R (D.ResolvedCircle t)) ((D.resolutionEdgeMap hst hc h R) x)) y = ((Khovanov.circleDuality R (D.ResolvedCircle s)) x) ((D.resolutionEdgeMap ⋯ ⋯ ⋯ R) y)

Edge maps are Frobenius self-adjoint. For the pairing of circle tensors, the edge map from s to t is adjoint to the edge map from t to s at the same crossing: a merge is adjoint to the split in the opposite direction, and a split to the merge.

theorem TauCeti.PDCode.isHomogeneous_resolutionEdgeMap {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) (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (R : Type u) [CommRing R] : LinearMap.IsHomogeneous (D.resolutionEdgeMap hst hc h R) ((Khovanov.circleQuantumGrading R (D.ResolvedCircle s)).piece ℤ) ((Khovanov.circleQuantumGrading R (D.ResolvedCircle t)).piece ℤ) (-1)

An actual resolution edge map has quantum degree -1.

theorem TauCeti.PDCode.resolutionEdgeMap_comp_resolutionEdgeMap_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) (h₁ : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t₁ c).card = 2) (h₁' : (D.circlesAt t₁ c').card = 2 ∨ (D.circlesAt u c').card = 2) (h₂ : (D.circlesAt s c').card = 2 ∨ (D.circlesAt t₂ c').card = 2) (h₂' : (D.circlesAt t₂ c).card = 2 ∨ (D.circlesAt u c).card = 2) (R : Type u) [CommSemiring R] : D.resolutionEdgeMap ht₁u hc₁' h₁' R ∘ₗ D.resolutionEdgeMap hst₁ hc₁ h₁ R = D.resolutionEdgeMap ht₂u hc₂' h₂' R ∘ₗ D.resolutionEdgeMap hst₂ hc₂ h₂ R

The faces of the cube of resolutions commute. Let s, t₁, t₂, u be the states of a face, where t₁ changes s at c, t₂ changes s at c', and u changes both. If all four edges are saddles, the composite of the edge maps through t₁ equals the composite through t₂.

theorem TauCeti.PDCode.SmoothingEquiv.reindex_resolutionEdgeMap {n m : ℕ} {D : PDCode n} {D' : PDCode m} {s t : Fin n → Bool} {s' t' : Fin m → Bool} {c : Fin n} {c' : Fin m} (es : D.SmoothingEquiv s D' s') (et : D.SmoothingEquiv t D' t') (hhalf : es.halfEdgeEquiv = et.halfEdgeEquiv) (hisolated : es.crossinglessEquiv = et.crossinglessEquiv) (slots : Fin 4 ≃ Fin 4) (hcross : ∀ (k : Fin 4), es.halfEdgeEquiv (D.crossing c k) = D'.crossing c' (slots k)) (hst : ∀ (j : Fin n), j ≠ c → s j = t j) (hc : s c ≠ t c) (hst' : ∀ (j : Fin m), j ≠ c' → s' j = t' j) (hc' : s' c' ≠ t' c') (h : (D.circlesAt s c).card = 2 ∨ (D.circlesAt t c).card = 2) (h' : (D'.circlesAt s' c').card = 2 ∨ (D'.circlesAt t' c').card = 2) (R : Type u_1) [CommSemiring R] (x : Khovanov.CircleTensor R (D.ResolvedCircle s)) : (PiTensorProduct.reindex R (fun (x : D.ResolvedCircle t) => DualNumber R) et.resolvedCircleCongr) ((D.resolutionEdgeMap hst hc h R) x) = (D'.resolutionEdgeMap hst' hc' h' R) ((PiTensorProduct.reindex R (fun (x : D.ResolvedCircle s) => DualNumber R) es.resolvedCircleCongr) x)

Reindexing the source and target circles commutes with an actual resolution edge map, when the transports at the two endpoints use the same half-edge and isolated-circle bijections and carry the slots of c to those of c'.