The graded fully blocked grid complex

For each Alexander degree, the fully blocked differential restricts to a chain complex indexed by the integer Maslov grading. Its objects are the homogeneous pieces of the grid chain module, and its differential is the restriction of the rectangle-counting differential. Inclusion into the total chain module intertwines the differentials, so square-zero follows from the total complex. This supplies the graded fully blocked complex whose Euler characteristic agrees with the Alexander-graded chain Euler characteristic.

The coefficient field is ZMod 2, as for the total fully blocked differential. The diagram has an odd number of components so that its Alexander grading is integral. The differential lowers Maslov degree by one and preserves Alexander degree.

Main definitions

• TauCeti.OddComponentGridDiagram.gradedFullyBlockedDifferential: the differential between consecutive Maslov degrees at fixed Alexander degree.
• TauCeti.OddComponentGridDiagram.gradedFullyBlockedComplex: the resulting chain complex.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Sections 4.3--4.4.

theorem TauCeti.OddComponentGridDiagram.bidegree_eq_sub_of_mem_fullyBlockedRectangles {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} {r : GridRectangleBetween x y} (hr : r ∈ (↑G).fullyBlockedRectangles x y) : G.bidegree y = G.bidegree x - (1, 0)

A fully blocked empty rectangle lowers the bidegree by (1, 0).

theorem TauCeti.OddComponentGridDiagram.bidegree_eq_sub_of_fullyBlockedRectangleCount_ne_zero {n : ℕ} (G : OddComponentGridDiagram n) {x y : GridState n} (h : (↑G).fullyBlockedRectangleCount x y ≠ 0) : G.bidegree y = G.bidegree x - (1, 0)

A nonzero fully blocked rectangle count from x to y implies G.bidegree y = G.bidegree x - (1, 0).

theorem TauCeti.OddComponentGridDiagram.fullyBlockedDifferential_bigradedChainInclusion_apply_eq_zero_of_ne {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) (c : G.BigradedChainPiece (ZMod 2) g) {y : GridState n} (hy : G.bidegree y ≠ g - (1, 0)) : ((↑G).fullyBlockedDifferential ((G.bigradedChainInclusion (ZMod 2) g) c)) y = 0

The total differential of a homogeneous chain is supported in bidegree one lower in Maslov and unchanged in Alexander.

theorem TauCeti.OddComponentGridDiagram.fullyBlockedDifferential_bigradedChainInclusion_bigradedChainProjection {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) (c : GridChain (ZMod 2) n) : (↑G).fullyBlockedDifferential ((G.bigradedChainInclusion (ZMod 2) g) ((G.bigradedChainProjection (ZMod 2) g) c)) = (G.bigradedChainInclusion (ZMod 2) (g - (1, 0))) ((G.bigradedChainProjection (ZMod 2) (g - (1, 0))) ((↑G).fullyBlockedDifferential c))

The fully blocked differential sends the homogeneous part of bidegree g of a chain to the part of bidegree g - (1, 0) of its differential.

noncomputable def TauCeti.OddComponentGridDiagram.gradedFullyBlockedDifferential {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) : G.BigradedChainPiece (ZMod 2) (m + 1, a) →ₗ[ZMod 2] G.BigradedChainPiece (ZMod 2) (m, a)

The fully blocked differential from Maslov degree m + 1 to m at Alexander degree a.

@[simp]

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedDifferential_apply {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) (c : G.BigradedChainPiece (ZMod 2) (m + 1, a)) (y : { y : GridState n // G.bidegree y = (m, a) }) : ((G.gradedFullyBlockedDifferential a m) c) y = ((↑G).fullyBlockedDifferential ((G.bigradedChainInclusion (ZMod 2) (m + 1, a)) c)) ↑y

The coefficient of the graded differential is the coefficient of the total differential.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_gradedFullyBlockedDifferential {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) (c : G.BigradedChainPiece (ZMod 2) (m + 1, a)) : (G.bigradedChainInclusion (ZMod 2) (m, a)) ((G.gradedFullyBlockedDifferential a m) c) = (↑G).fullyBlockedDifferential ((G.bigradedChainInclusion (ZMod 2) (m + 1, a)) c)

Inclusion of the homogeneous pieces intertwines the graded and total differentials.

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedDifferential_comp_eq_zero {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) : G.gradedFullyBlockedDifferential a m ∘ₗ G.gradedFullyBlockedDifferential a (m + 1) = 0

Consecutive graded fully blocked differentials compose to zero.

noncomputable def TauCeti.OddComponentGridDiagram.gradedFullyBlockedComplex {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : ChainComplex (ModuleCat (ZMod 2)) ℤ

The Maslov-graded fully blocked grid complex in Alexander degree a.

@[simp]

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedComplex_X {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) : (G.gradedFullyBlockedComplex a).X m = ↧(G.BigradedChainPiece (ZMod 2) (m, a))

The objects of the graded complex are the homogeneous grid-chain pieces.

@[simp]

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedComplex_d {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) : (G.gradedFullyBlockedComplex a).d (m + 1) m = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.gradedFullyBlockedDifferential a m)) (CategoryTheory.eqToHom ⋯))

The consecutive differential is the restriction of the total grid differential.