The annular terms of the unblocked grid differential square vanish

The square of the unblocked grid differential ∂⁻ of Unblocked.lean is a sum over pairs of composable rectangles. The juxtaposition argument for ∂⁻ ∘ ∂⁻ = 0 splits those pairs according to how the two rectangles meet, and the annular case is the one in which the second rectangle returns to the source of the first. This file closes that case.

The mechanism is that a returning pair covers a full toroidal annulus, GridRectangleBetween.coveredSquares_union_coveredSquares, and a grid diagram has an X-marking in every column and in every row. So a returning pair always covers an X-marking, and the unblocked differential counts only rectangles that cover none: between two grid states, at most one of the two directions contributes at all (GridDiagram.unblockedRectangles_eq_empty_or_unblockedRectangles_eq_empty). The unblocked differential therefore has no two-step return, and the diagonal entries of the matrix of ∂⁻ ∘ ∂⁻ are zero.

The argument never inspects the O-markings, so it is insensitive to the weights V^{O(r)} and runs over an arbitrary commutative coefficient ring, characteristic two included. The three cases of the juxtaposition analysis are told apart by how many side columns the two rectangles have in common: both for the annular case treated here, none for the disjoint case of Differential/Square/DoubleTransposition.lean, and exactly one for the overlapping case. On a grid of size at most two the annular case already suffices, because there is no room for the other two: that consequence is GridDiagram.unblockedDifferential_comp_self_eq_zero_of_le_two in SmallGrid/Differential.lean.

Main results

• TauCeti.GridDiagram.unblockedRectangles_eq_empty_or_unblockedRectangles_eq_empty: between two grid states, one of the two directions carries no rectangle the unblocked differential counts.
• TauCeti.GridDiagram.unblockedCoefficient_mul_unblockedCoefficient_eq_zero: the product of the two matrix coefficients of ∂⁻ between a pair of grid states vanishes.
• TauCeti.GridDiagram.unblockedDifferential_sq_single_apply_self: its diagonal entries vanish.

References

This is the annular case of the juxtaposition case analysis for ∂² = 0. The argument follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

theorem TauCeti.GridDiagram.unblockedRectangles_eq_empty_or_unblockedRectangles_eq_empty {n : ℕ} (G : GridDiagram n) (x y : GridState n) : G.unblockedRectangles x y = ∅ ∨ G.unblockedRectangles y x = ∅

Between two grid states, the unblocked differential counts rectangles in at most one of the two directions: a rectangle from x to y and a rectangle from y back to x would cover a full toroidal annulus between them, and every annulus carries an X-marking.

theorem TauCeti.GridDiagram.unblockedCoefficient_eq_zero_of_ne_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (h : G.unblockedCoefficient R x y ≠ 0) : G.unblockedCoefficient R y x = 0

A nonzero matrix coefficient of the unblocked differential forces the opposite coefficient to vanish.

@[simp]

theorem TauCeti.GridDiagram.unblockedCoefficient_mul_unblockedCoefficient_eq_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : G.unblockedCoefficient R x y * G.unblockedCoefficient R y x = 0

The two matrix coefficients of the unblocked differential between a pair of grid states have zero product: the unblocked differential admits no two-step return.

@[simp]

theorem TauCeti.GridDiagram.unblockedDifferential_sq_single_apply_self {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x : GridState n) : ((G.unblockedDifferential R) ((G.unblockedDifferential R) (Finsupp.single x 1))) x = 0

The diagonal entries of the matrix of ∂⁻ ∘ ∂⁻ vanish: every annular term of the square of the unblocked grid differential is individually zero, for every coefficient ring.

@[simp]

theorem TauCeti.GridDiagram.notMem_support_unblockedDifferential_sq_single {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x : GridState n) : x ∉ ((G.unblockedDifferential R) ((G.unblockedDifferential R) (Finsupp.single x 1))).support

The source generator does not survive two applications of the unblocked differential.

theorem TauCeti.GridDiagram.notMem_support_unblockedDifferentialOnGenerator_of_mem_support {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x y : GridState n} (h : y ∈ (G.unblockedDifferentialOnGenerator R x).support) : x ∉ (G.unblockedDifferentialOnGenerator R y).support

The support of the unblocked differential contains no two-step return: if y occurs in ∂⁻ x, then x does not occur in ∂⁻ y.