Transport of resolution saddle maps

The merge and split maps on actual resolved-circle tensors commute with transport of the smoothed diagrams. The smoothing equivalences at the two endpoints must use the same half-edge bijection and the same bijection of labelled isolated circles. This includes native relabellings, slot rotations, mirror with complemented states, and isolated-circle permutations. The resulting squares retain all factors, including the circles disjoint from the saddle.

These are unsigned identities over every commutative semiring. Cube-order signs belong to the signed totalization, while circle reindexing contributes no sign. The combinatorial square is TauCeti.PDCode.SmoothingEquiv.resolvedCircleCongr_saddleResolvedCircleMap; multiplication and the adjoint split transport along that square by their existing composition laws.

References

• M. Khovanov, A categorification of the Jones polynomial, Duke Math. J. 101 (2000), §2.

theorem TauCeti.PDCode.SmoothingEquiv.reindex_resolutionMergeMap {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) (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') (R : Type u_1) [CommSemiring R] (hs : (D.circlesAt s c).card = 2) (hs' : (D'.circlesAt s' c').card = 2) (x : Khovanov.CircleTensor R (D.ResolvedCircle s)) : (PiTensorProduct.reindex R (fun (x : D.ResolvedCircle t) => DualNumber R) et.resolvedCircleCongr) ((D.resolutionMergeMap hst hc hs R) x) = (D'.resolutionMergeMap hst' hc' hs' 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 merge. The circle bijections retain every isolated-circle label.

theorem TauCeti.PDCode.SmoothingEquiv.reindex_resolutionSplitMap {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) (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') (R : Type u_1) [CommSemiring R] (ht : (D.circlesAt t c).card = 2) (ht' : (D'.circlesAt t' c').card = 2) (x : Khovanov.CircleTensor R (D.ResolvedCircle s)) : (PiTensorProduct.reindex R (fun (x : D.ResolvedCircle t) => DualNumber R) et.resolvedCircleCongr) ((D.resolutionSplitMap hst hc ht R) x) = (D'.resolutionSplitMap hst' hc' ht' 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 split. This uses the same endpoint transports as the reverse merge.