The grid differentials on grids of size at most two

This file records the small-grid computations for the grid differentials.

For the fully blocked differential the whole differential vanishes. An oriented rectangle needs two distinct side columns, so grids of size at most one have no rectangles at all. On a 2 × 2 grid, an oriented rectangle covers a single square, and the four markings of the diagram occupy all four squares — two O markings and two X markings on the two diagonals — so every oriented rectangle contains a marking and no rectangle is fully blocked. In either case every fully blocked count vanishes, hence so does the whole differential.

The cases n = 0 and n = 1 already follow from the column-swap support bound. The new content here is the size-two computation, which is the first sanity check for the marking-avoidance condition defining the fully blocked grid complex: on the 2 × 2 unknot grid every square is marked, so the fully blocked theory sees no rectangles at all.

The unblocked differential ∂⁻ need not vanish, but it does square to zero, and on these grids the annular case of Differential/Square/Annulus.lean settles that on its own. At most two grid states are available, which leaves no room for the disjoint and overlapping juxtaposition cases: if the source and the target of a two-step term are distinct they exhaust the grid states, so every intermediate state is one of them and its term carries a diagonal matrix coefficient, while if the source and the target coincide the term is annular.

Main results

• TauCeti.GridDiagram.fullyBlockedRectangles_eq_empty_of_le_two: no rectangle is fully blocked in grid size at most two.
• TauCeti.GridDiagram.fullyBlockedRectangleCount_eq_zero_of_le_two: every fully blocked rectangle coefficient vanishes in grid size at most two.
• TauCeti.GridDiagram.fullyBlockedDifferential_eq_zero_of_le_two: the fully blocked differential is the zero linear map in grid size at most two.
• TauCeti.GridDiagram.fullyBlockedDifferential_eq_zero_of_two: the explicit 2 × 2 form.
• TauCeti.GridDiagram.unblockedDifferential_comp_self_eq_zero_of_le_two: in grid size at most two the unblocked differential squares to zero.

References

This supplies a prerequisite for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0", and for the standing convention that the grid complexes compute on explicit small grids. The rectangle-count convention follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3; the marking-avoidance condition defining the fully blocked complex is in Chapter 4, Section 4.4.

theorem TauCeti.GridDiagram.fullyBlockedRectangles_eq_empty_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x y : GridState n) : G.fullyBlockedRectangles x y = ∅

In grid size at most two, no oriented rectangle is fully blocked. A rectangle needs two distinct side columns and two distinct side rows, so it covers exactly the one square at its initial corner; that square holds a point of the source state, and in a column of only two squares the two distinct markings of that column leave no unmarked square for it.

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_eq_zero_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x y : GridState n) : G.fullyBlockedRectangleCount x y = 0

Every fully blocked rectangle coefficient vanishes in grid size at most two: no rectangle is fully blocked.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedRectangleCount_eq_zero_of_two (G : GridDiagram 2) (x y : GridState 2) : G.fullyBlockedRectangleCount x y = 0

Every fully blocked rectangle coefficient vanishes on every 2 × 2 grid.

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_eq_zero_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : G.fullyBlockedDifferentialOnGenerator x = 0

The fully blocked differential of one generator vanishes in grid size at most two.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferentialOnGenerator_eq_zero_of_two (G : GridDiagram 2) (x : GridState 2) : G.fullyBlockedDifferentialOnGenerator x = 0

The fully blocked differential of one generator vanishes on every 2 × 2 grid.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_eq_zero_of_le_two {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : G.fullyBlockedDifferential = 0

The fully blocked differential is zero on every chain in grid size at most two.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedDifferential_eq_zero_of_two (G : GridDiagram 2) : G.fullyBlockedDifferential = 0

The fully blocked differential is zero on every 2 × 2 grid. This is the first sanity check for the marking-avoidance condition: every square of a 2 × 2 grid is marked.

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

On a grid of size at most two the unblocked differential squares to zero.

At most two grid states are available. If the source and the target of a two-step term are distinct they exhaust those states, so every intermediate state coincides with the source or with the target and its term is killed by the vanishing of the diagonal matrix coefficient. If instead the source and the target coincide, the term returns to its source and the annular argument applies. Unlike the general square-zero theorem GridDiagram.unblockedDifferential_comp_self_eq_zero, which pairs juxtaposed rectangles and so needs characteristic two, this small-grid instance holds over every commutative coefficient semiring.