The homotopy equation of a grid commutation

Let C be a validated column commutation of a grid diagram G, write G' for the commuted diagram G.swapColumns C.column (finRotate n C.column), ∂ for the unblocked differential of G, Φ : GC⁻(G) → GC⁻(G') for the commutation map GridDiagram.commutationMap of C, Ψ : GC⁻(G') → GC⁻(G) for the commutation map of the reverse data C.reverse, and H : GC⁻(G) → GC⁻(G) for the hexagon-counting map GridDiagram.commutationHomotopy. Over 𝔽₂, commutation invariance rests on the homotopy equation

∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ.

This file writes that equation as a finite identity between matrix coefficients.

Both Φ and Ψ are semilinear over the renaming of the variables by the swap of the two commuted columns. That swap is an involution, so the round trip Ψ ∘ Φ is linear over the polynomial ring (GridDiagram.reverse_commutationMap_commutationMap_smul), like ∂ and H, and the equation holds on all chains as soon as it holds on the grid-state generators. On a generator x, the coefficient of ∂ (H x) + H (∂ x) at z is a sum over intermediate states of products of rectangle and hexagon coefficients, and that of Ψ (Φ x) is a sum of products of pentagon coefficients, the first one renamed into the variables of G.

Every term is then a product, over the squares covered by a two-step domain, of one per-square weight in the variables of G: the variable of the square's column at an O-marking of G and 1 elsewhere. This is GridDiagram.OMonomial_eq_prod_coveredSquares for rectangles, GridDiagram.hexagonWeight_eq_prod_coveredSquares and its initial version for hexagons, GridDiagram.rename_pentagonWeight and its initial version for the pentagons of Φ, and GridDiagram.pentagonWeight_reverse and its initial version for the pentagons of Ψ, whose squares are read in G by exchanging the two commuted columns. Comparing the weights of two two-step domains thus reduces to comparing the multisets of squares they cover.

Main results

• TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_single_apply, TauCeti.GridDiagram.commutationHomotopy_unblockedDifferential_single_apply and TauCeti.GridDiagram.reverse_commutationMap_commutationMap_single_apply: the matrix coefficients of ∂ ∘ H, H ∘ ∂ and Ψ ∘ Φ. The last is the case of TauCeti.GridDiagram.commutationMap_withTurnRow_commutationMap_single_apply, for a return map turning in an arbitrary row.
• TauCeti.GridDiagram.reverse_commutationMap_commutationMap_smul: the round trip Ψ ∘ Φ is linear over the polynomial ring. It is the case of TauCeti.GridDiagram.commutationMap_withTurnRow_commutationMap_smul, for a return map turning in an arbitrary row.
• TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff: the homotopy equation holds on every chain exactly when, for all grid states x and z, the rectangle and hexagon coefficient products from x to z sum to δ_{xz} plus the pentagon coefficient products.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559).

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_single_apply {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ((G.unblockedDifferential R) ((G.commutationHomotopy R C) (Finsupp.single x 1))) z = ∑ y : GridState n, G.commutationHexagonCoefficient R C x y * G.unblockedCoefficient R y z

On a grid-state generator, the coefficient of the unblocked differential after the commutation homotopy is the sum over intermediate states of the commutation hexagon coefficient times the rectangle coefficient.

theorem TauCeti.GridDiagram.commutationHomotopy_unblockedDifferential_single_apply {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ((G.commutationHomotopy R C) ((G.unblockedDifferential R) (Finsupp.single x 1))) z = ∑ y : GridState n, G.unblockedCoefficient R x y * G.commutationHexagonCoefficient R C y z

On a grid-state generator, the coefficient of the commutation homotopy after the unblocked differential is the sum over intermediate states of the rectangle coefficient times the commutation hexagon coefficient.

theorem TauCeti.GridDiagram.commutationMap_withTurnRow_commutationMap_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (T : ColumnTurn n) (t : Fin n) (x z : GridState n) : (((swapColumns T.column ((finRotate n) T.column) G).commutationMap R (T.withTurnRow t)) ((G.commutationMap R T) (Finsupp.single x 1))) z = ∑ y : GridState n, (MvPolynomial.rename ⇑(Equiv.swap T.column ((finRotate n) T.column))) (G.commutationPentagonCoefficient R T x y) * (swapColumns T.column ((finRotate n) T.column) G).commutationPentagonCoefficient R (T.withTurnRow t) y z

On a grid-state generator, the coefficient of the round trip through the commuted diagram, first the commutation map of a turn T and then that of the commuted diagram at the same columns turning in row t, is the sum over intermediate states of the commutation pentagon coefficient of the first map, renamed by the column swap, times that of the second.

theorem TauCeti.GridDiagram.reverse_commutationMap_commutationMap_single_apply {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (x z : GridState n) : (((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) (Finsupp.single x 1))) z = ∑ y : GridState n, (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.commutationPentagonCoefficient R C.toColumnTurn x y) * (swapColumns C.column ((finRotate n) C.column) G).commutationPentagonCoefficient R C.reverse.toColumnTurn y z

On a grid-state generator, the coefficient of the round trip Ψ ∘ Φ through the commuted diagram is the sum over intermediate states of the commutation pentagon coefficient of Φ, renamed by the column swap, times that of the reverse commutation map Ψ.

theorem TauCeti.GridDiagram.commutationMap_withTurnRow_commutationMap_smul {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (T : ColumnTurn n) (t : Fin n) (p : MvPolynomial (Fin n) R) (c : GridChainMinus R n) : ((swapColumns T.column ((finRotate n) T.column) G).commutationMap R (T.withTurnRow t)) ((G.commutationMap R T) (p • c)) = p • ((swapColumns T.column ((finRotate n) T.column) G).commutationMap R (T.withTurnRow t)) ((G.commutationMap R T) c)

The round trip through the commuted diagram, first the commutation map of a turn T and then that of the commuted diagram at the same columns turning in row t, is linear over the polynomial ring: both maps are semilinear over the renaming of the variables by the swap of the two commuted columns, and that renaming is an involution.

theorem TauCeti.GridDiagram.reverse_commutationMap_commutationMap_smul {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] (p : MvPolynomial (Fin n) R) (c : GridChainMinus R n) : ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) (p • c)) = p • ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) c)

The round trip Ψ ∘ Φ through the commuted diagram is linear over the polynomial ring: the commutation map and its reverse are semilinear over the same renaming of the variables by the swap of the two commuted columns, and that renaming is an involution.

theorem TauCeti.GridDiagram.unblockedDifferential_commutationHomotopy_add_eq_iff {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (R : Type u_1) [CommSemiring R] : (∀ (c : GridChainMinus R n), (G.unblockedDifferential R) ((G.commutationHomotopy R C) c) + (G.commutationHomotopy R C) ((G.unblockedDifferential R) c) = c + ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R C.reverse.toColumnTurn) ((G.commutationMap R C.toColumnTurn) c)) ↔ ∀ (x z : GridState n), ∑ y : GridState n, (G.commutationHexagonCoefficient R C x y * G.unblockedCoefficient R y z + G.unblockedCoefficient R x y * G.commutationHexagonCoefficient R C y z) = (if x = z then 1 else 0) + ∑ y : GridState n, (MvPolynomial.rename ⇑(Equiv.swap C.column ((finRotate n) C.column))) (G.commutationPentagonCoefficient R C.toColumnTurn x y) * (swapColumns C.column ((finRotate n) C.column) G).commutationPentagonCoefficient R C.reverse.toColumnTurn y z

The homotopy equation ∂ ∘ H + H ∘ ∂ = 1 + Ψ ∘ Φ of a column commutation holds on every chain exactly when, for all grid states x and z, the products of rectangle and hexagon coefficients through intermediate states, in both orders, sum to the Kronecker delta of x and z plus the products of the coefficients of the commutation map, renamed by the column swap, and of its reverse.