The X-marking homotopy on the unblocked grid complex

Fix the X-marking X_k of column k of a grid diagram. The map H_k on the unblocked grid complex GC⁻ counts the empty rectangles whose covered squares carry exactly one X-marking, namely X_k, each weighted by the monomial V^{O(r)} of its covered O-markings, exactly as the unblocked differential ∂⁻ weights the empty rectangles that carry no X-marking.

The anticommutator ∂⁻ ∘ H_k + H_k ∘ ∂⁻ is a sum over two-step decompositions: pairs of empty rectangles one of which is counted by ∂⁻ and the other by H_k. When the two rectangles cover disjoint squares this is the condition that together they cover exactly one X-marking, X_k (mem_XHomotopyDecompositions_iff_of_disjoint). Both pairings of the proof that ∂⁻ squares to zero preserve this condition: reordering rectangles with disjoint side columns exchanges the two rectangles, and recutting rectangles with one common side column repartitions the same covered squares. So, exactly as for ∂⁻ ∘ ∂⁻, the off-diagonal entries of the anticommutator cancel in pairs in characteristic two (sum_XHomotopyDecompositions_eq_zero). The diagonal entries, where the two rectangles form a thin annulus through X_k, are computed in TauCeti.KnotTheory.Grid.XHomotopy.Annulus.

Main definitions

• TauCeti.GridDiagram.XHomotopyRectangles: the empty rectangles whose only covered X-marking is X_k.
• TauCeti.GridDiagram.XHomotopyCoefficient: the matrix coefficients of H_k.
• TauCeti.GridDiagram.XHomotopy: the map H_k, linear over the polynomial ring.
• TauCeti.GridDiagram.XHomotopyDecompositions: the two-step decompositions counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻.

Main results

• TauCeti.GridDiagram.left_eq_of_mem_XHomotopyRectangles_X: a rectangle counted by H_k from the X-marking state has initial side k.
• TauCeti.GridDiagram.sum_XHomotopyDecompositions: the matrix entries of ∂⁻ ∘ H_k + H_k ∘ ∂⁻ are the weighted sums over XHomotopyDecompositions.
• TauCeti.GridDiagram.mem_XHomotopyDecompositions_iff_of_disjoint: for rectangles covering disjoint squares, membership says that their union carries the single X-marking X_k.
• TauCeti.GridDiagram.sum_XHomotopyDecompositions_eq_zero: in characteristic two the off-diagonal entries of ∂⁻ ∘ H_k + H_k ∘ ∂⁻ vanish.
• TauCeti.GridDiagram.constantCoeff_XHomotopyCoefficient: setting every variable to zero, a matrix coefficient of H_k counts the empty rectangles whose only marking is X_k.
• TauCeti.GridDiagram.alexander_sub_card_OColumns_eq_alexander_sub_one: H_k lowers the Alexander grading by one.
• TauCeti.GridDiagram.exists_mem_XHomotopyRectangles_of_mem_support_XHomotopyCoefficient: every monomial of a matrix coefficient of H_k is the weight of a contributing rectangle.

References

The homotopy H_{X_k} and the juxtaposition argument follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

Rectangles through a single X-marking

noncomputable def TauCeti.GridDiagram.XHomotopyRectangles {n : ℕ} (G : GridDiagram n) (k : Fin n) (x y : GridState n) : Finset (GridRectangleBetween x y)

The rectangles counted by the X-marking homotopy H_k from x to y: the empty rectangles whose covered squares carry exactly one X-marking, the marking X_k of column k.

@[simp]

theorem TauCeti.GridDiagram.mem_XHomotopyRectangles {n : ℕ} (G : GridDiagram n) (k : Fin n) {x y : GridState n} (r : GridRectangleBetween x y) : r ∈ G.XHomotopyRectangles k x y ↔ r.IsEmpty ∧ r.toGridRectangle.coveredSquares ∩ G.XSet = {(k, G.X.toPerm k)}

Membership in XHomotopyRectangles is emptiness together with covering X_k as the only X-marking.

theorem TauCeti.GridDiagram.left_eq_of_mem_XHomotopyRectangles_X {n : ℕ} (G : GridDiagram n) {k : Fin n} {y : GridState n} {r : GridRectangleBetween G.X y} (hr : r ∈ G.XHomotopyRectangles k G.X y) : r.left = k

A rectangle counted by the X-marking homotopy of column k from the X-marking state has initial side k: its initial lower corner is the lower-left corner of the X-marked square of its initial side column, so it covers that marking.

theorem TauCeti.GridDiagram.XHomotopyRectangles_subset_emptyRectangles {n : ℕ} (G : GridDiagram n) (k : Fin n) (x y : GridState n) : G.XHomotopyRectangles k x y ⊆ GridRectangleBetween.emptyRectangles x y

The rectangles counted by H_k are empty rectangles.

theorem TauCeti.GridDiagram.disjoint_unblockedRectangles_XHomotopyRectangles {n : ℕ} (G : GridDiagram n) (k : Fin n) (x y : GridState n) : Disjoint (G.unblockedRectangles x y) (G.XHomotopyRectangles k x y)

No rectangle is counted both by the unblocked differential, which forbids every X-marking, and by H_k, which requires the marking X_k.

theorem TauCeti.GridDiagram.alexander_sub_card_OColumns_eq_alexander_sub_one {n : ℕ} (G : GridDiagram n) {k : Fin n} {x y : GridState n} {r : GridRectangleBetween x y} (hr : r ∈ G.XHomotopyRectangles k x y) : G.alexander y - ↑(G.OColumns r.toGridRectangle).card = G.alexander x - 1

A rectangle counted by H_k lowers the Alexander grading by one, once its weight V^{O(r)} is charged -1 per variable, since it covers the single X-marking X_k: the term V^{O(r)} · y of H_k x has Alexander grading A(x) - 1.

noncomputable def TauCeti.GridDiagram.XHomotopyCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (x y : GridState n) : MvPolynomial (Fin n) R

The matrix coefficient of H_k from x to y: the sum of the weights V^{O(r)} of the empty rectangles from x to y whose only covered X-marking is X_k.

theorem TauCeti.GridDiagram.XHomotopyCoefficient_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (x y : GridState n) : G.XHomotopyCoefficient R k x y = ∑ r ∈ G.XHomotopyRectangles k x y, G.OMonomial R r.toGridRectangle

The matrix coefficient of H_k is the sum of the weights of its contributing rectangles.

theorem TauCeti.GridDiagram.exists_mem_XHomotopyRectangles_of_mem_support_XHomotopyCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {k : Fin n} {x y : GridState n} {d : Fin n →₀ ℕ} (hd : d ∈ (G.XHomotopyCoefficient R k x y).support) : ∃ r ∈ G.XHomotopyRectangles k x y, d = ∑ c ∈ G.OColumns r.toGridRectangle, Finsupp.single c 1

Every monomial of a matrix coefficient of H_k is the weight V^{O(r)} of a contributing rectangle.

@[simp]

theorem TauCeti.GridDiagram.constantCoeff_XHomotopyCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (x y : GridState n) : MvPolynomial.constantCoeff (G.XHomotopyCoefficient R k x y) = ↑{r ∈ G.XHomotopyRectangles k x y | G.OColumns r.toGridRectangle = ∅}.card

The constant term of a matrix coefficient of H_k counts the contributing rectangles that carry no O-marking either: setting every variable to zero leaves the count of the empty rectangles whose only marking is X_k.

noncomputable def TauCeti.GridDiagram.XHomotopy {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n

The X-marking homotopy H_k on the unblocked grid complex GC⁻, linear over the polynomial ring: a generator x is sent to the sum of the generators y weighted by XHomotopyCoefficient R k x y.

theorem TauCeti.GridDiagram.XHomotopy_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (x y : GridState n) : ((G.XHomotopy R k) (Finsupp.single x 1)) y = G.XHomotopyCoefficient R k x y

The matrix coefficients of the X-marking homotopy.

theorem TauCeti.GridDiagram.XHomotopy_single {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (x : GridState n) : (G.XHomotopy R k) (Finsupp.single x 1) = Finsupp.equivFunOnFinite.symm fun (y : GridState n) => G.XHomotopyCoefficient R k x y

The X-marking homotopy sends a generator to its row of matrix coefficients.

@[simp]

theorem TauCeti.GridDiagram.XHomotopy_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (c : GridChainMinus R n) (y : GridState n) : ((G.XHomotopy R k) c) y = Finsupp.sum c fun (x : GridState n) (a : MvPolynomial (Fin n) R) => a * G.XHomotopyCoefficient R k x y

The coefficient formula for the X-marking homotopy on an arbitrary chain.

The two-step decompositions of the anticommutator

noncomputable def TauCeti.GridDiagram.XHomotopyDecompositions {n : ℕ} (G : GridDiagram n) (k : Fin n) (x z : GridState n) : Finset (GridRectangleDecomposition x z)

The two-step decompositions counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻ from x to z: one rectangle is counted by the unblocked differential and the other by the X-marking homotopy H_k.

@[simp]

theorem TauCeti.GridDiagram.mem_XHomotopyDecompositions {n : ℕ} (G : GridDiagram n) (k : Fin n) {x z : GridState n} (D : GridRectangleDecomposition x z) : D ∈ G.XHomotopyDecompositions k x z ↔ D.first ∈ G.unblockedRectangles x D.middle ∧ D.second ∈ G.XHomotopyRectangles k D.middle z ∨ D.first ∈ G.XHomotopyRectangles k x D.middle ∧ D.second ∈ G.unblockedRectangles D.middle z

A decomposition is counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻ when one rectangle is counted by ∂⁻ and the other by H_k.

theorem TauCeti.GridDiagram.isEmpty_of_mem_XHomotopyDecompositions {n : ℕ} (G : GridDiagram n) {k : Fin n} {x z : GridState n} {D : GridRectangleDecomposition x z} (hD : D ∈ G.XHomotopyDecompositions k x z) : D.first.IsEmpty ∧ D.second.IsEmpty

Every rectangle of a decomposition counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻ is empty.

theorem TauCeti.GridDiagram.mem_XHomotopyDecompositions_iff_of_disjoint {n : ℕ} (G : GridDiagram n) (k : Fin n) {x z : GridState n} (D : GridRectangleDecomposition x z) (hD : Disjoint D.first.toGridRectangle.coveredSquares D.second.toGridRectangle.coveredSquares) : D ∈ G.XHomotopyDecompositions k x z ↔ D.first.IsEmpty ∧ D.second.IsEmpty ∧ (D.first.toGridRectangle.coveredSquares ∪ D.second.toGridRectangle.coveredSquares) ∩ G.XSet = {(k, G.X.toPerm k)}

For two rectangles covering disjoint squares, being counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻ means that both are empty and that together they carry exactly one X-marking, the marking X_k.

theorem TauCeti.GridDiagram.sum_XHomotopyDecompositions {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (k : Fin n) (x z : GridState n) : ∑ D ∈ G.XHomotopyDecompositions k x z, G.unblockedDecompositionWeight R D = ∑ y : GridState n, (G.unblockedCoefficient R x y * G.XHomotopyCoefficient R k y z + G.XHomotopyCoefficient R k x y * G.unblockedCoefficient R y z)

The matrix entries of ∂⁻ ∘ H_k + H_k ∘ ∂⁻, written as the sum over intermediate states of the products of matrix coefficients, are the weighted sums over the decompositions counted by XHomotopyDecompositions.

Cancellation off the diagonal

theorem TauCeti.GridDiagram.commute_mem_XHomotopyDecompositions {n : ℕ} (G : GridDiagram n) {k : Fin n} {x z : GridState n} {D : GridRectangleDecomposition x z} (h : D.HasDisjointSides) (hD : D ∈ G.XHomotopyDecompositions k x z) : D.commute h ∈ G.XHomotopyDecompositions k x z

Reordering two rectangles with disjoint side columns keeps a decomposition counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻: it exchanges the two covered domains, and so exchanges the roles of ∂⁻ and H_k.

theorem TauCeti.GridDiagram.recut_mem_XHomotopyDecompositions {n : ℕ} (G : GridDiagram n) {k : Fin n} {x z : GridState n} {D : GridRectangleDecomposition x z} (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) (hD : D ∈ G.XHomotopyDecompositions k x z) : D.recut hone hfirst hsecond ∈ G.XHomotopyDecompositions k x z

Recutting two empty rectangles with one common side column keeps a decomposition counted by ∂⁻ ∘ H_k + H_k ∘ ∂⁻: the recut covers the same squares, hence the same X-markings.

theorem TauCeti.GridDiagram.sum_XHomotopyDecompositions_eq_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (k : Fin n) {x z : GridState n} (hzx : z ≠ x) : ∑ D ∈ G.XHomotopyDecompositions k x z, G.unblockedDecompositionWeight R D = 0

In characteristic two the off-diagonal matrix entries of ∂⁻ ∘ H_k + H_k ∘ ∂⁻ vanish: the decompositions they count pair off by reordering or by recutting, and paired decompositions have the same weight.