The bigraded fully blocked stabilization factor

Let G' be the stabilization of a grid diagram G with an odd number of components that splits the X-marking of column s. The fully blocked stabilization comparison TauCeti.GridDiagram.fullyBlockedHomologyStabilizeXEquivProd identifies GH~(G') with two copies of GH~(G). Its first component, the center part, raises the bidegree by (1, 1), and its second component, the reduced off-center homotopy, preserves the bidegree. Hence it commutes with the homogeneous projections of fully blocked homology and restricts, in every bidegree g, to an equivalence

GH~(G')_g ≃ GH~(G)_{g + (1, 1)} × GH~(G)_g.

So GH~(G') ≅ GH~(G) ⊗ W as bigraded vector spaces, with W the two-dimensional space with generators in bidegrees (0, 0) and (-1, -1): the Poincaré series of fully blocked homology is multiplied by TauCeti.Bigraded.W. Its class modulo ⊗ W-stabilization is therefore unchanged by this stabilization. The worked 3 × 3 unknot example, with series W ^ 2, is in TauCeti.KnotTheory.Grid.SmallGrid.Stabilization.

Main definitions

• TauCeti.OddComponentGridDiagram.fullyBlockedStabilizeXHomologyPieceEquiv: the equivalence GH~(G')_g ≃ GH~(G)_{g + (1, 1)} × GH~(G)_g.

Main results

• fullyBlockedHomologyStabilizeXEquivProd_bigradedFullyBlockedHomologyProjection: the stabilization comparison intertwines the homogeneous projections, with the shift (1, 1) on the center component.
• TauCeti.OddComponentGridDiagram.finrank_bigradedFullyBlockedHomologyPiece_stabilizeX: the dimension of a piece of GH~(G') is the sum of the dimensions of two pieces of GH~(G).
• TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_stabilizeX: stabilization multiplies the Poincaré series by W.
• OddComponentGridDiagram.isStablyEquiv_bigradedFullyBlockedHomologyPoincareSeries_stabilizeX: the stable class of the Poincaré series is unchanged by stabilization.

References

• Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, for the bigraded identification GH~(G') ≅ GH~(G) ⊗ W.
• Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.2.

theorem TauCeti.OddComponentGridDiagram.fullyBlockedHomologyStabilizeXEquivProd_bigradedFullyBlockedHomologyProjection {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (y : (↑(G.stabilizeX s)).fullyBlockedHomology) : ((↑G).fullyBlockedHomologyStabilizeXEquivProd s) (((G.stabilizeX s).bigradedFullyBlockedHomologyProjection g) y) = ((G.bigradedFullyBlockedHomologyProjection (g + (1, 1))) (((↑G).fullyBlockedHomologyStabilizeXEquivProd s) y).1, (G.bigradedFullyBlockedHomologyProjection g) (((↑G).fullyBlockedHomologyStabilizeXEquivProd s) y).2)

The stabilization comparison intertwines the homogeneous projections of fully blocked homology: the center component shifts the bidegree by (1, 1) and the off-center component preserves it.

theorem TauCeti.OddComponentGridDiagram.fst_fullyBlockedHomologyStabilizeXEquivProd_mem {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) {g : ℤ × ℤ} {y : (↑(G.stabilizeX s)).fullyBlockedHomology} (hy : y ∈ (G.stabilizeX s).bigradedFullyBlockedHomologyPiece g) : (((↑G).fullyBlockedHomologyStabilizeXEquivProd s) y).1 ∈ G.bigradedFullyBlockedHomologyPiece (g + (1, 1))

The center component of the stabilization comparison sends the bidegree-g piece into the bidegree-(g + (1, 1)) piece.

theorem TauCeti.OddComponentGridDiagram.snd_fullyBlockedHomologyStabilizeXEquivProd_mem {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) {g : ℤ × ℤ} {y : (↑(G.stabilizeX s)).fullyBlockedHomology} (hy : y ∈ (G.stabilizeX s).bigradedFullyBlockedHomologyPiece g) : (((↑G).fullyBlockedHomologyStabilizeXEquivProd s) y).2 ∈ G.bigradedFullyBlockedHomologyPiece g

The off-center component of the stabilization comparison preserves the bidegree-g piece.

noncomputable def TauCeti.OddComponentGridDiagram.fullyBlockedStabilizeXHomologyPieceEquiv {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) : ↥((G.stabilizeX s).bigradedFullyBlockedHomologyPiece g) ≃ₗ[ZMod 2] ↥(G.bigradedFullyBlockedHomologyPiece (g + (1, 1))) × ↥(G.bigradedFullyBlockedHomologyPiece g)

The bigraded stabilization factor. The fully blocked stabilization comparison identifies the bidegree-g piece of the homology of the stabilized diagram with the product of the pieces of bidegrees g + (1, 1) and g of the homology of the original diagram. These are the two summands of GH~(G) ⊗ W in bidegree g.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coe_fst_fullyBlockedStabilizeXHomologyPieceEquiv_apply {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (y : ↥((G.stabilizeX s).bigradedFullyBlockedHomologyPiece g)) : ↑((G.fullyBlockedStabilizeXHomologyPieceEquiv s g) y).1 = (((↑G).fullyBlockedHomologyStabilizeXEquivProd s) ↑y).1

The first component of the piece equivalence is the center component of the stabilization comparison.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coe_snd_fullyBlockedStabilizeXHomologyPieceEquiv_apply {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) (y : ↥((G.stabilizeX s).bigradedFullyBlockedHomologyPiece g)) : ↑((G.fullyBlockedStabilizeXHomologyPieceEquiv s g) y).2 = (((↑G).fullyBlockedHomologyStabilizeXEquivProd s) ↑y).2

The second component of the piece equivalence is the off-center component of the stabilization comparison.

theorem TauCeti.OddComponentGridDiagram.finrank_bigradedFullyBlockedHomologyPiece_stabilizeX {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (g : ℤ × ℤ) : Module.finrank (ZMod 2) ↥((G.stabilizeX s).bigradedFullyBlockedHomologyPiece g) = Module.finrank (ZMod 2) ↥(G.bigradedFullyBlockedHomologyPiece (g + (1, 1))) + Module.finrank (ZMod 2) ↥(G.bigradedFullyBlockedHomologyPiece g)

The dimension of a homogeneous piece of the fully blocked homology of the stabilized diagram is the sum of the dimensions of the pieces of bidegrees g + (1, 1) and g of the original homology.

theorem TauCeti.OddComponentGridDiagram.bigradedFullyBlockedHomologyPoincareSeries_stabilizeX {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) : (G.stabilizeX s).bigradedFullyBlockedHomologyPoincareSeries = G.bigradedFullyBlockedHomologyPoincareSeries * Bigraded.W

Stabilization multiplies the Poincaré series by W. The Poincaré series of the fully blocked homology of the stabilization splitting an X-marking is that of the original diagram times the series W of the stabilization factor.

theorem TauCeti.OddComponentGridDiagram.isStablyEquiv_bigradedFullyBlockedHomologyPoincareSeries_stabilizeX {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) : Bigraded.IsStablyEquiv (G.stabilizeX s).bigradedFullyBlockedHomologyPoincareSeries G.bigradedFullyBlockedHomologyPoincareSeries

The class of the Poincaré series of fully blocked homology modulo ⊗ W-stabilization is unchanged by the stabilization splitting an X-marking.