Disjoint double-transposition terms vanish

The square of a grid differential is a sum over pairs of composable rectangles, and the juxtaposition argument for ∂ ∘ ∂ = 0 splits those pairs according to how many side columns the two rectangles have in common. Both columns in common is the annular case of Annulus.lean, where the second rectangle returns to the source of the first. This file treats the opposite extreme, for the fully blocked and the unblocked differential alike: the target state is obtained from the source by two disjoint column transpositions.

That configuration is exactly the disjoint-side case of the case split in SideOverlap.lean. Two disjoint column transpositions move four columns, whereas two transpositions sharing a column move only three, so every two-step decomposition of such a target has disjoint pairs of side columns. Reordering the two rectangle moves, GridRectangleDecomposition.commute, is then an involution on the decompositions the unblocked differential counts. Exchanging the two toroidal domains preserves X-avoidance and the weight V^{O(r)}. Emptiness is transferred separately by isEmpty_commute_first and isEmpty_commute_second, using the cyclic-separation lemma Grid.mem_cIoo_and_mem_cIoo_swap_of_notMem. Reordering also changes the intermediate state, so it has no fixed point. In characteristic two the paired terms cancel.

The shared bookkeeping in Count.lean first reindexes the two-step terms as a single sum over the finite set of decompositions both of whose rectangles the unblocked differential counts. That reindexing holds for every pair of grid states and coefficient ring, so it serves the intermediate case of two rectangles sharing exactly one side column, GridRectangleDecomposition.HasOneCommonSide, just as well.

Main results

The following results are in the TauCeti.GridDiagram namespace.

• fullyBlockedDifferential_sq_single_apply_swapColumns_swapColumns_eq_zero_of_disjoint: the fully blocked differential-square entry for two disjoint column transpositions vanishes.
• unblockedDecompositionWeight_commute: commuting a disjoint-side decomposition preserves its unblocked weight.
• commute_mem_unblockedDecompositions_iff and commute_mem_fullyBlockedDecompositions_iff: commuting preserves whether the unblocked, respectively fully blocked, differential counts a decomposition.
• sum_unblockedCoefficient_mul_unblockedCoefficient_swapColumns_swapColumns_eq_zero_of_disjoint: the weighted sum for two disjoint column transpositions vanishes in characteristic two.
• unblockedDifferential_sq_single_apply_swapColumns_swapColumns_eq_zero_of_disjoint: in characteristic two, that entry vanishes when the target is the source with two disjoint column transpositions applied.

References

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

theorem TauCeti.GridDiagram.unblockedDecompositionWeight_commute {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : G.unblockedDecompositionWeight R (D.commute h) = G.unblockedDecompositionWeight R D

Reordering a two-step decomposition with disjoint side columns preserves its weight: the two toroidal domains are exchanged.

theorem TauCeti.GridDiagram.commute_mem_unblockedDecompositions_iff {n : ℕ} (G : GridDiagram n) {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : D.commute h ∈ G.unblockedDecompositions x z ↔ D ∈ G.unblockedDecompositions x z

Reordering a two-step decomposition with disjoint side columns preserves whether the unblocked differential counts it: both rectangles stay empty and the two domains, hence the covered squares, are merely exchanged.

This is not a simp lemma: mem_unblockedDecompositions, mem_unblockedRectangles and commute_first_toGridRectangle/commute_second_toGridRectangle are all @[simp], so the left-hand side is never in simp-normal form.

theorem TauCeti.GridDiagram.commute_mem_fullyBlockedDecompositions_iff {n : ℕ} (G : GridDiagram n) {x z : GridState n} (D : GridRectangleDecomposition x z) (h : D.HasDisjointSides) : D.commute h ∈ G.fullyBlockedDecompositions x z ↔ D ∈ G.fullyBlockedDecompositions x z

Reordering a two-step decomposition with disjoint side columns preserves whether the fully blocked differential counts it: both rectangles stay empty and the two domains, hence the covered squares, are merely exchanged.

This is not a simp lemma: mem_fullyBlockedDecompositions, mem_fullyBlockedRectangles and commute_first_toGridRectangle/commute_second_toGridRectangle are all @[simp], so the left-hand side is never in simp-normal form.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_apply_swapColumns_swapColumns_eq_zero_of_disjoint {n : ℕ} (G : GridDiagram n) (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) (hcd : c ≠ d) (hdisjoint : Disjoint {a, b} {c, d}) : (G.fullyBlockedDifferential (G.fullyBlockedDifferential (Finsupp.single x 1))) (GridState.swapColumns c d (GridState.swapColumns a b x)) = 0

The square of the fully blocked grid differential has zero matrix entry between a grid state and the state obtained from it by two disjoint column transpositions.

This is the disjoint clause of the juxtaposition case analysis for the fully blocked complex.

theorem TauCeti.GridDiagram.sum_unblockedCoefficient_mul_unblockedCoefficient_swapColumns_swapColumns_eq_zero_of_disjoint {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) (hcd : c ≠ d) (hdisjoint : Disjoint {a, b} {c, d}) : ∑ y : GridState n, G.unblockedCoefficient R x y * G.unblockedCoefficient R y (GridState.swapColumns c d (GridState.swapColumns a b x)) = 0

In characteristic two, the two-step matrix entry of the square of the unblocked differential between a grid state and the state obtained from it by two disjoint column transpositions vanishes.

This is the sum-level form of the disjoint case, and the form the remaining one-common-side case will consume.

theorem TauCeti.GridDiagram.unblockedDifferential_sq_single_apply_swapColumns_swapColumns_eq_zero_of_disjoint {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (x : GridState n) {a b c d : Fin n} (hab : a ≠ b) (hcd : c ≠ d) (hdisjoint : Disjoint {a, b} {c, d}) : ((G.unblockedDifferential R) ((G.unblockedDifferential R) (Finsupp.single x 1))) (GridState.swapColumns c d (GridState.swapColumns a b x)) = 0

In characteristic two, the square of the unblocked grid differential has zero matrix entry between a grid state and the state obtained from it by two disjoint column transpositions.

Among the targets obtained from a grid state by two column transpositions, this leaves only the case of two transpositions sharing exactly one column: two transpositions on the same pair of columns return to the source, whose entry vanishes by the diagonal case in Annulus.lean.