Counting two-rectangle decompositions

The coefficient of the square of the fully blocked grid differential is a sum over intermediate states of products of rectangle counts. This file identifies that expression with the parity of a single finite set: the set of pairs of composable fully blocked empty rectangles with prescribed source and target.

This is the algebraic handoff needed by the juxtaposition proof of ∂² = 0. Its geometric part can now act directly on GridDiagram.fullyBlockedDecompositions G x z: a fixed-point-free involution of this finite set proves that its cardinality is even, and hence that the corresponding coefficient of the differential square vanishes.

The same shared decomposition construction also reindexes the matrix entries of the unblocked differential square as weighted sums over pairs of empty, X-avoiding rectangles. This is the counting form used by the disjoint and one-common-side cases.

Which region carries a marking. Every fully blocked statement below is relative to the ambient GridDiagram.fullyBlockedRectangles, and none of them unfolds the marking condition: they relate two objects assembled from that one finite set. The marking region is fixed upstream by GridRectangle.AvoidsMarkings, which asks that no square a rectangle covers carry an O or an X marking.

Main definitions

• TauCeti.GridDiagram.fullyBlockedDecompositions: composable pairs of fully blocked empty rectangles with fixed endpoints.
• TauCeti.GridDiagram.fullyBlockedDecompositionCount: the cardinality of this set modulo two.
• TauCeti.GridDiagram.unblockedDecompositions: composable pairs of rectangles counted by the unblocked differential.
• TauCeti.GridDiagram.unblockedDecompositionWeight: the product of their two monomial weights.

Main results

• TauCeti.GridDiagram.mem_fullyBlockedDecompositions: membership means that both rectangles in the decomposition are fully blocked.
• TauCeti.GridDiagram.card_fullyBlockedDecompositions: the cardinality is the sum, over intermediate states, of the product of the two rectangle-set cardinalities.
• TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_sum: the parity count is the coefficient sum appearing in the square of the differential.
• TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_zero_iff_even: its vanishing is exactly evenness of the finite decomposition set.
• TauCeti.GridDiagram.fullyBlockedDifferential_comp_self_eq_zero_iff_decompositionCount: the differential squares to zero exactly when every decomposition count vanishes.
• TauCeti.GridDiagram.sum_unblockedDecompositions: a sum over the unblocked decompositions is the iterated sum over intermediate states and counted rectangles.
• TauCeti.GridDiagram.sum_unblockedCoefficient_mul_unblockedCoefficient: an unblocked two-step matrix entry is the weighted sum over the corresponding decompositions.

References

This supplies the counting step for TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.3, "The complexes and ∂² = 0". The pairing of juxtaposed empty rectangles follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.6.

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

The finite set of decompositions from x to z in which both constituent rectangles are fully blocked and empty for the grid diagram G.

The intermediate state is retained as part of GridRectangleDecomposition; it is determined by the first rectangle, but is the index over which the differential-square coefficient is summed.

@[simp]

theorem TauCeti.GridDiagram.mem_fullyBlockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) (D : GridRectangleDecomposition x z) : D ∈ G.fullyBlockedDecompositions x z ↔ D.first ∈ G.fullyBlockedRectangles x D.middle ∧ D.second ∈ G.fullyBlockedRectangles D.middle z

A decomposition is fully blocked exactly when each of its two rectangles belongs to the corresponding fully blocked rectangle set.

The unblocked differential

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

The two-step rectangle decompositions from x to z both of whose rectangles the unblocked differential counts: both are empty and cover no X-marking.

@[simp]

theorem TauCeti.GridDiagram.mem_unblockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) (D : GridRectangleDecomposition x z) : D ∈ G.unblockedDecompositions x z ↔ D.first ∈ G.unblockedRectangles x D.middle ∧ D.second ∈ G.unblockedRectangles D.middle z

A two-step decomposition is counted by the unblocked differential exactly when each of its two rectangles is.

theorem TauCeti.GridDiagram.sum_unblockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) {M : Type u_1} [AddCommMonoid M] (w : (y : GridState n) → GridRectangleBetween x y → GridRectangleBetween y z → M) : ∑ D ∈ G.unblockedDecompositions x z, w D.middle D.first D.second = ∑ y : GridState n, ∑ r₁ ∈ G.unblockedRectangles x y, ∑ r₂ ∈ G.unblockedRectangles y z, w y r₁ r₂

A sum over the decompositions counted by the square of the unblocked differential is the iterated sum over the intermediate state and the two counted rectangles.

noncomputable def TauCeti.GridDiagram.unblockedDecompositionWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleDecomposition x z) : MvPolynomial (Fin n) R

The weight of a two-step rectangle decomposition in the square of the unblocked differential: the product of the weights V^{O(r)} of its two rectangles.

@[simp]

theorem TauCeti.GridDiagram.unblockedDecompositionWeight_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] {x z : GridState n} (D : GridRectangleDecomposition x z) : G.unblockedDecompositionWeight R D = G.OMonomial R D.first.toGridRectangle * G.OMonomial R D.second.toGridRectangle

The unblocked decomposition weight is the product of the monomial weights of its two rectangles.

theorem TauCeti.GridDiagram.sum_unblockedCoefficient_mul_unblockedCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x z : GridState n) : ∑ y : GridState n, G.unblockedCoefficient R x y * G.unblockedCoefficient R y z = ∑ D ∈ G.unblockedDecompositions x z, G.unblockedDecompositionWeight R D

The two-step matrix entry of the square of the unblocked differential is the sum of the weights of the two-step decompositions it counts.

Fully blocked counts

theorem TauCeti.GridDiagram.isEmpty_first_of_mem_fullyBlockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) {D : GridRectangleDecomposition x z} (hD : D ∈ G.fullyBlockedDecompositions x z) : D.first.IsEmpty

The first rectangle in a fully blocked decomposition is empty.

theorem TauCeti.GridDiagram.isEmpty_second_of_mem_fullyBlockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) {D : GridRectangleDecomposition x z} (hD : D ∈ G.fullyBlockedDecompositions x z) : D.second.IsEmpty

The second rectangle in a fully blocked decomposition is empty.

theorem TauCeti.GridDiagram.avoidsMarkings_first_of_mem_fullyBlockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) {D : GridRectangleDecomposition x z} (hD : D ∈ G.fullyBlockedDecompositions x z) : D.first.AvoidsMarkings G

The first rectangle in a fully blocked decomposition avoids every marking.

theorem TauCeti.GridDiagram.avoidsMarkings_second_of_mem_fullyBlockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) {D : GridRectangleDecomposition x z} (hD : D ∈ G.fullyBlockedDecompositions x z) : D.second.AvoidsMarkings G

The second rectangle in a fully blocked decomposition avoids every marking.

theorem TauCeti.GridDiagram.card_fullyBlockedDecompositions {n : ℕ} (G : GridDiagram n) (x z : GridState n) : (G.fullyBlockedDecompositions x z).card = ∑ y : GridState n, (G.fullyBlockedRectangles x y).card * (G.fullyBlockedRectangles y z).card

The number of fully blocked decompositions is the sum over intermediate states of the product of the two rectangle-set cardinalities.

theorem TauCeti.GridDiagram.fullyBlockedDecompositions_eq_empty_of_notMem_twoStep {n : ℕ} (G : GridDiagram n) (x z : GridState n) (hz : z ∉ x.twoStepColumnSwapNeighbors) : G.fullyBlockedDecompositions x z = ∅

There are no fully blocked decompositions from x to a state outside the two-step column-swap support of x.

noncomputable def TauCeti.GridDiagram.fullyBlockedDecompositionCount {n : ℕ} (G : GridDiagram n) (x z : GridState n) : ZMod 2

The number modulo two of fully blocked two-rectangle decompositions from x to z.

theorem TauCeti.GridDiagram.fullyBlockedDecompositionCount_def {n : ℕ} (G : GridDiagram n) (x z : GridState n) : G.fullyBlockedDecompositionCount x z = ↑(G.fullyBlockedDecompositions x z).card

The fully blocked decomposition count is the cardinality of fullyBlockedDecompositions, coerced to ZMod 2.

theorem TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_zero_iff_even {n : ℕ} (G : GridDiagram n) (x z : GridState n) : G.fullyBlockedDecompositionCount x z = 0 ↔ Even (G.fullyBlockedDecompositions x z).card

A fully blocked decomposition count vanishes exactly when the corresponding finite set has even cardinality. This is the parity form consumed by a fixed-point-free pairing of decompositions.

theorem TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_zero_of_notMem_twoStep {n : ℕ} (G : GridDiagram n) (x z : GridState n) (hz : z ∉ x.twoStepColumnSwapNeighbors) : G.fullyBlockedDecompositionCount x z = 0

The fully blocked decomposition count vanishes outside the two-step column-swap support.

theorem TauCeti.GridDiagram.fullyBlockedDecompositionCount_eq_sum {n : ℕ} (G : GridDiagram n) (x z : GridState n) : G.fullyBlockedDecompositionCount x z = ∑ y : GridState n, G.fullyBlockedRectangleCount x y * G.fullyBlockedRectangleCount y z

The parity of fully blocked decompositions is the sum over intermediate states of the product of the two fully blocked rectangle counts.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_sq_single_apply_eq_decompositionCount {n : ℕ} (G : GridDiagram n) (x z : GridState n) : (G.fullyBlockedDifferential (G.fullyBlockedDifferential (Finsupp.single x 1))) z = G.fullyBlockedDecompositionCount x z

The coefficient of z in the square of the differential applied to the generator x is the parity of the fully blocked decompositions from x to z.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_comp_self_eq_zero_iff_decompositionCount {n : ℕ} (G : GridDiagram n) : G.fullyBlockedDifferential ∘ₗ G.fullyBlockedDifferential = 0 ↔ ∀ (x z : GridState n), G.fullyBlockedDecompositionCount x z = 0

The fully blocked differential squares to zero exactly when every fully blocked two-rectangle decomposition set has even cardinality.