Merge maps for actual resolutions of a PD-code

Suppose two states differ at one crossing and two source circles meet that crossing. Exactly one target circle meets it. The map TauCeti.PDCode.resolutionMergeMap multiplies the factors of these two source circles and transports all remaining factors, including every labelled crossing-free circle. It uses the native quotient correspondence of circles and the indexed circle tensor, with no ordering or choice of representatives.

On the enhanced-state basis, two X labels on the merged circles give zero. In every other case their labels multiply and every other label is retained. The map has quantum degree -1, compensating for the increase of the state quantum shift along an A-to-B edge. This is the unsigned merge block of the resolution differential; its cube sign is supplied separately. No planarity assumption is needed for a saddle already known to merge two circles.

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.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) (hs : (D.circlesAt s c).card = 2) (R : Type u) [CommSemiring R] : Khovanov.CircleTensor R (D.ResolvedCircle s) →ₐ[R] Khovanov.CircleTensor R (D.ResolvedCircle t)

Multiplication on the two circles merged at c, and identity on every other factor of the actual resolved-circle tensor. The one-circle target condition follows from the source count.

theorem TauCeti.PDCode.resolutionMergeMap_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) (hs : (D.circlesAt s c).card = 2) (R : Type u) [CommSemiring R] : D.resolutionMergeMap hst hc hs R = PiTensorProduct.fiberwiseMul (D.saddleResolvedCircleMap hst ⋯)

The resolution merge is the indexed multiplication along the native saddle correspondence.

@[simp]

theorem TauCeti.PDCode.resolutionMergeMap_tprod {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) (R : Type u) [CommSemiring R] (x : D.ResolvedCircle s → DualNumber R) : (D.resolutionMergeMap hst hc hs R) ((PiTensorProduct.tprod R) x) = (PiTensorProduct.tprod R) fun (C : D.ResolvedCircle t) => ∏ C' : D.ResolvedCircle s with D.saddleResolvedCircleMap hst ⋯ C' = C, x C'

The merge sends a pure tensor to the tensor of the products over the saddle fibres. Each unchanged fibre is a singleton, and the changed fibre consists of the two source circles.

@[simp]

theorem TauCeti.PDCode.resolutionMergeMap_circleBasis {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) {R : Type u} [CommSemiring R] (l : D.ResolvedCircle s → Bool) : (D.resolutionMergeMap hst hc hs R) ((Khovanov.circleBasis R (D.ResolvedCircle s)) l) = if l (Sum.inl ⟦D.crossing c 0⟧) = true ∧ l (Sum.inl ⟦D.crossing c 2⟧) = true then 0 else (Khovanov.circleBasis R (D.ResolvedCircle t)) fun (C : D.ResolvedCircle t) => decide (∃ (C' : D.ResolvedCircle s), D.saddleResolvedCircleMap hst ⋯ C' = C ∧ l C' = true)

On enhanced states the merged labels obey 1·1=1, 1·X=X·1=X, and X·X=0; all other labels follow their unchanged circle.

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

An actual resolution merge has quantum degree -1.