The grid differentials square to zero

The square of the unblocked grid differential ∂⁻ of Unblocked.lean is a sum over pairs of composable rectangles which are empty and cover no X-marking. This file completes the juxtaposition argument that the sum vanishes in characteristic two. That is the square-zero condition a chain complex structure on GC⁻ needs; the structure itself is not built here.

The two side-column pairs of such a two-step term are equal, disjoint, or meet in exactly one column. Equal pairs mean the second rectangle returns to the source of the first; those terms cover a full toroidal annulus, hence an X-marking, and vanish over every coefficient ring. The other two cases pair the terms off two by two, by a weight-preserving involution without fixed points: rectangles with disjoint side columns are applied in the opposite order, and rectangles sharing one side column bound an L-shaped hexagon which is cut the other way. Each pairing changes the intermediate grid state and preserves the covered-square domain, hence the monomial weight, so in characteristic two the two terms of a pair cancel. The pairing is stated separately, for any function on decompositions whose paired terms cancel, so that a sign assignment can reuse it over coefficient rings of other characteristics.

Specializing carries the square-zero identity to the two blocked theories as well. Setting one V_i to zero gives the simply blocked map, and specialization intertwines the two differentials. Setting every V_i to zero — that is, taking constant terms — gives the fully blocked differential TauCeti.GridDiagram.fullyBlockedDifferential, whose rectangles must avoid the O-markings as well: GridDiagram.fullyBlockedRectangleCount_eq_constantCoeff identifies its matrix coefficients with the constant terms of ∂⁻ over ZMod 2.

Main results

• TauCeti.GridRectangleDecomposition.sum_eq_zero_of_pairing: the pairing itself, for any family of decompositions into empty rectangles closed under both pairings and any function on decompositions whose paired terms cancel, over any coefficients.
• TauCeti.GridDiagram.sum_unblockedDecompositions_eq_zero: the pairing for the decompositions counted by the square of ∂⁻.
• TauCeti.GridDiagram.unblockedDecompositionWeight_recut: recutting a decomposition preserves its weight.
• TauCeti.GridDiagram.sum_unblockedCoefficient_mul_unblockedCoefficient_eq_zero: every matrix entry of the square of ∂⁻ vanishes.
• TauCeti.GridDiagram.unblockedDifferential_comp_self_eq_zero: ∂⁻ ∘ ∂⁻ = 0.
• TauCeti.GridDiagram.simplyBlockedDifferential_comp_self_eq_zero: the same for the specialization at V_i = 0.
• TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_zero, TauCeti.GridDiagram.fullyBlockedDifferential_comp_self_eq_zero: the same for the fully blocked differential, the specialization at every V_i = 0.

References

The juxtaposition proof follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

theorem TauCeti.GridRectangleDecomposition.sum_eq_zero_of_pairing {n : ℕ} {M : Type u_1} [AddCommMonoid M] {x z : GridState n} (hzx : z ≠ x) {S : Finset (GridRectangleDecomposition x z)} (hempty : ∀ D ∈ S, D.first.IsEmpty ∧ D.second.IsEmpty) (hcommute_mem : ∀ D ∈ S, ∀ (h : D.HasDisjointSides), D.commute h ∈ S) (hrecut_mem : ∀ D ∈ S, ∀ (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty), D.recut hone hfirst hsecond ∈ S) (f : GridRectangleDecomposition x z → M) (hcommute : ∀ D ∈ S, ∀ (h : D.HasDisjointSides), f D + f (D.commute h) = 0) (hrecut : ∀ D ∈ S, ∀ (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty), f D + f (D.recut hone hfirst hsecond) = 0) : ∑ D ∈ S, f D = 0

The juxtaposition pairing. Let S be a finite family of two-step decompositions from x to a different state z into two empty rectangles, closed under reordering two rectangles with disjoint side columns and under recutting two rectangles that share one side column. A function on decompositions sums to zero over S when each term cancels its partner under both pairings.

Over 𝔽₂ the partners carry equal weights; over a general coefficient ring a sign assignment makes them carry opposite signs.

theorem TauCeti.GridDiagram.sum_unblockedDecompositions_eq_zero {n : ℕ} (G : GridDiagram n) {M : Type u_1} [AddCommMonoid M] {x z : GridState n} (hzx : z ≠ x) (f : GridRectangleDecomposition x z → M) (hcommute : ∀ D ∈ G.unblockedDecompositions x z, ∀ (h : D.HasDisjointSides), f D + f (D.commute h) = 0) (hrecut : ∀ D ∈ G.unblockedDecompositions x z, ∀ (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty), f D + f (D.recut hone hfirst hsecond) = 0) : ∑ D ∈ G.unblockedDecompositions x z, f D = 0

The juxtaposition pairing for the square of ∂⁻: a function on the two-step decompositions counted by the square of ∂⁻ sums to zero over the decompositions from x to a different state z, provided each term cancels its partner under both pairings, reordering two rectangles with disjoint side columns and recutting two rectangles that share one side column.

theorem TauCeti.GridDiagram.unblockedDecompositionWeight_recut {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleDecomposition x z) (hone : D.HasOneCommonSide) (hfirst : D.first.IsEmpty) (hsecond : D.second.IsEmpty) : G.unblockedDecompositionWeight R (D.recut hone hfirst hsecond) = G.unblockedDecompositionWeight R D

Recutting a two-step decomposition by two empty rectangles sharing one side column preserves its weight: the two decompositions cover the same squares.

theorem TauCeti.GridDiagram.sum_unblockedCoefficient_mul_unblockedCoefficient_eq_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (x z : GridState n) : ∑ y : GridState n, G.unblockedCoefficient R x y * G.unblockedCoefficient R y z = 0

In characteristic two every matrix entry of the square of the unblocked grid differential vanishes.

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

In characteristic two the square of the unblocked grid differential vanishes on a generator.

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

In characteristic two the square of the unblocked grid differential kills every generator.

theorem TauCeti.GridDiagram.unblockedDifferential_comp_self_eq_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] : G.unblockedDifferential R ∘ₗ G.unblockedDifferential R = 0

The unblocked grid differential squares to zero in characteristic two.

theorem TauCeti.GridDiagram.simplyBlockedDifferential_comp_self_eq_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (i : Fin n) : G.simplyBlockedDifferential R i ∘ₗ G.simplyBlockedDifferential R i = 0

The simply blocked grid map squares to zero in characteristic two: it is the specialization of ∂⁻ at V_i = 0, and specialization intertwines the two maps.

theorem TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_zero {n : ℕ} (G : GridDiagram n) (x z : GridState n) : G.fullyBlockedDecompositionCount x z = 0

Every fully blocked two-step decomposition count is even.

The fully blocked matrix coefficients are the constant terms of the unblocked ones over ZMod 2, and taking constant terms is a ring homomorphism, so this entry of the fully blocked square is the constant term of the corresponding entry of ∂⁻ ∘ ∂⁻.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_comp_self_eq_zero {n : ℕ} (G : GridDiagram n) : G.fullyBlockedDifferential ∘ₗ G.fullyBlockedDifferential = 0

The fully blocked grid differential TauCeti.GridDiagram.fullyBlockedDifferential squares to zero.