Bigrading of the fully blocked stabilization comparison

The fully blocked stabilization comparison has two components. The center projection raises both Maslov and Alexander degree by one, while the reduced off-center X₂-homotopy preserves both degrees. Thus a stabilized chain in degree (m, a) maps to original chains in degrees (m + 1, a + 1) and (m, a). These are the shifts of the stabilization factor W, whose summands have degrees (-1,-1) and (0,0).

This file restricts the specified comparison to homogeneous chain pieces and proves that its two components intertwine the graded differentials. It also shows that, on an arbitrary stabilized chain, the center component sends the homogeneous part of degree g to the homogeneous part of degree g + (1,1) of the image, and the off-center component preserves homogeneous parts. These chain comparisons supply the grading input for the fully blocked homology stabilization equivalence.

References

• Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2.
• Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.2.

theorem TauCeti.OddComponentGridDiagram.fullyBlockedStabilizeXMap_fst_bigradedChainInclusion_eq_zero_of_ne {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g) {x : GridState n} (hx : G.bidegree x ≠ g + (1, 1)) : (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) c)).1 x = 0

On a homogeneous stabilized chain, the first comparison component is supported in degree g + (1,1), reflecting the degree (-1,-1) of the center summand of W.

theorem TauCeti.OddComponentGridDiagram.fullyBlockedStabilizeXMap_snd_bigradedChainInclusion_eq_zero_of_ne {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g) {x : GridState n} (hx : G.bidegree x ≠ g) : (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) c)).2 x = 0

On a homogeneous stabilized chain, the second comparison component is supported in the same bidegree. Only rectangles carrying no O-marking survive coefficient reduction.

noncomputable def TauCeti.OddComponentGridDiagram.gradedFullyBlockedStabilizeXCenter {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g →ₗ[ZMod 2] G.BigradedChainPiece (ZMod 2) (g + (1, 1))

The center component of fully blocked stabilization on homogeneous chains. Its target bidegree is one higher in both coordinates.

noncomputable def TauCeti.OddComponentGridDiagram.gradedFullyBlockedStabilizeXOffCenter {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g →ₗ[ZMod 2] G.BigradedChainPiece (ZMod 2) g

The off-center homotopy component of fully blocked stabilization on homogeneous chains, with no grading shift.

@[simp]

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedStabilizeXCenter_apply {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g) (x : { x : GridState n // G.bidegree x = g + (1, 1) }) : ((G.gradedFullyBlockedStabilizeXCenter s g) c) x = (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) c) ((↑x).insertPoint s.succ ((↑G).X.toPerm s).succ)

At a state of the target degree, the graded center map reads the center coefficient.

@[simp]

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedStabilizeXOffCenter_apply {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g) (x : { x : GridState n // G.bidegree x = g }) : ((G.gradedFullyBlockedStabilizeXOffCenter s g) c) x = (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) c)).2 ↑x

At a state of the target degree, the graded off-center map has the coefficient of the specified total comparison.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_gradedFullyBlockedStabilizeXCenter {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g) : (G.bigradedChainInclusion (ZMod 2) (g + (1, 1))) ((G.gradedFullyBlockedStabilizeXCenter s g) c) = (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) c)).1

Inclusion of the graded center comparison recovers the specified total comparison.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bigradedChainInclusion_gradedFullyBlockedStabilizeXOffCenter {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) g) : (G.bigradedChainInclusion (ZMod 2) g) ((G.gradedFullyBlockedStabilizeXOffCenter s g) c) = (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) c)).2

Inclusion of the graded off-center comparison recovers the specified total comparison.

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedStabilizeXCenter_differential {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (a m : ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) (m + 1, a)) : (G.gradedFullyBlockedStabilizeXCenter s (m, a)) (((G.stabilizeX s).gradedFullyBlockedDifferential a m) c) = (G.gradedFullyBlockedDifferential (a + 1) (m + 1)) ((G.gradedFullyBlockedStabilizeXCenter s (m + 1, a)) c)

The graded center comparison intertwines the differentials, with the (-1,-1) summand shift on the original complex.

theorem TauCeti.OddComponentGridDiagram.gradedFullyBlockedStabilizeXOffCenter_differential {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (a m : ℤ) (c : (G.stabilizeX s).BigradedChainPiece (ZMod 2) (m + 1, a)) : (G.gradedFullyBlockedStabilizeXOffCenter s (m, a)) (((G.stabilizeX s).gradedFullyBlockedDifferential a m) c) = (G.gradedFullyBlockedDifferential a m) ((G.gradedFullyBlockedStabilizeXOffCenter s (m + 1, a)) c)

The graded off-center comparison intertwines the differentials without a grading shift.

theorem TauCeti.OddComponentGridDiagram.fst_fullyBlockedStabilizeXMap_bigradedChainInclusion {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : GridChain (ZMod 2) (n + 1)) : (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) (((G.stabilizeX s).bigradedChainProjection (ZMod 2) g) c))).1 = (G.bigradedChainInclusion (ZMod 2) (g + (1, 1))) ((G.bigradedChainProjection (ZMod 2) (g + (1, 1))) (((↑G).fullyBlockedStabilizeXMap s) c).1)

The center component of the chain comparison sends the part of bidegree g of a stabilized chain to the part of bidegree g + (1, 1) of its image.

theorem TauCeti.OddComponentGridDiagram.snd_fullyBlockedStabilizeXMap_bigradedChainInclusion {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (c : GridChain (ZMod 2) (n + 1)) : (((↑G).fullyBlockedStabilizeXMap s) (((G.stabilizeX s).bigradedChainInclusion (ZMod 2) g) (((G.stabilizeX s).bigradedChainProjection (ZMod 2) g) c))).2 = (G.bigradedChainInclusion (ZMod 2) g) ((G.bigradedChainProjection (ZMod 2) g) (((↑G).fullyBlockedStabilizeXMap s) c).2)

The off-center component of the chain comparison preserves homogeneous parts.