Split maps for actual resolutions of a PD-code

Suppose two states s and t differ at one crossing c, and two circles of t meet c. Exactly one circle of s meets c, and the saddle correspondence of circles runs from t to s: it collapses the two circles of t through c onto the circle of s through c and is a bijection on all other circles, including every labelled crossing-free circle. The map TauCeti.PDCode.resolutionSplitMap applies the comultiplication Δ to the factor of the circle of s through c and transports all remaining factors along this correspondence. It is the split map TauCeti.Khovanov.fiberwiseSplit of the indexed circle tensor along the native quotient correspondence, so it involves no ordering of circles or choice of representatives.

The split is the Frobenius adjoint of the merge along the same saddle in the opposite direction (TauCeti.PDCode.circleDuality_resolutionSplitMap). On the enhanced-state basis it obeys Δ X = X ⊗ X and Δ 1 = X ⊗ 1 + 1 ⊗ X, where the two output circles are those through slots 0 and 2 of c, and every other label is retained (TauCeti.PDCode.resolutionSplitMap_circleBasis). 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 split block of the resolution differential; its cube sign is supplied separately. No planarity assumption is needed for a saddle already known to split one circle into two.

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

Comultiplication on the circle through c, splitting it into the two circles of the target through c, and identity on every other factor of the actual resolved-circle tensor. The one-circle source condition follows from the target count.

theorem TauCeti.PDCode.resolutionSplitMap_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) (ht : (D.circlesAt t c).card = 2) (R : Type u) [CommSemiring R] : D.resolutionSplitMap hst hc ht R = Khovanov.fiberwiseSplit (D.saddleResolvedCircleMap ⋯ ⋯)

The resolution split is the indexed split along the native saddle correspondence from the target to the source.

@[simp]

theorem TauCeti.PDCode.circleDuality_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) (ht : (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.resolutionSplitMap hst hc ht R) x)) y = ((Khovanov.circleDuality R (D.ResolvedCircle s)) x) ((D.resolutionMergeMap ⋯ ⋯ ht R) y)

The resolution split is adjoint, for the Frobenius pairing of circle tensors, to the resolution merge along the same crossing in the opposite direction.

@[simp]

theorem TauCeti.PDCode.resolutionSplitMap_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) (ht : (D.circlesAt t c).card = 2) {R : Type u} [CommSemiring R] (l : D.ResolvedCircle s → Bool) : (D.resolutionSplitMap hst hc ht R) ((Khovanov.circleBasis R (D.ResolvedCircle s)) l) = if l (Sum.inl ⟦D.crossing c 0⟧) = true then (Khovanov.circleBasis R (D.ResolvedCircle t)) fun (C : D.ResolvedCircle t) => l (D.saddleResolvedCircleMap ⋯ ⋯ C) else (Khovanov.circleBasis R (D.ResolvedCircle t)) (Function.update (fun (C : D.ResolvedCircle t) => l (D.saddleResolvedCircleMap ⋯ ⋯ C)) (Sum.inl ⟦D.crossing c 0⟧) true) + (Khovanov.circleBasis R (D.ResolvedCircle t)) (Function.update (fun (C : D.ResolvedCircle t) => l (D.saddleResolvedCircleMap ⋯ ⋯ C)) (Sum.inl ⟦D.crossing c 2⟧) true)

On enhanced states the split obeys Δ X = X ⊗ X and Δ 1 = X ⊗ 1 + 1 ⊗ X on the circle through c, whose two outputs are the circles through slots 0 and 2; every other circle retains the label of its unchanged source circle.

@[simp]

theorem TauCeti.PDCode.resolutionSplitMap_one {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) (ht : (D.circlesAt t c).card = 2) {R : Type u} [CommSemiring R] : (D.resolutionSplitMap hst hc ht R) 1 = (PiTensorProduct.singleAlgHom (Sum.inl ⟦D.crossing c 0⟧)) DualNumber.eps + (PiTensorProduct.singleAlgHom (Sum.inl ⟦D.crossing c 2⟧)) DualNumber.eps

Splitting the unit gives X ⊗ 1 + 1 ⊗ X on the two circles through c, with 1 on every other circle.

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

An actual resolution split has quantum degree -1.