The fully blocked stabilization factor

Splitting an X-marking doubles the fully blocked homology. The comparison sends a chain to its center part and the fully blocked X₂-homotopy of its off-center part. The latter comparison is a quasi-isomorphism, and the composite of the connecting map with it is zero after every variable is set to zero. Thus the stabilized mapping cone compares to the cone of zero, whose homology is two copies of the original homology.

The equivalence here concerns ungraded vector spaces. Its first summand comes from center states, whose Maslov and Alexander gradings are both one below the original state; the second summand comes from the X₂-homotopy and has the original gradings. These are the two summands of the usual stabilization factor W, in degrees (-1,-1) and (0,0).

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.

The comparison reuses the reduced off-center-to-center quasi-isomorphism of TauCeti.KnotTheory.Grid.Stabilization.Comparison and Mathlib's mapping cones.

noncomputable def TauCeti.GridDiagram.fullyBlockedStabilizeXMap {n : ℕ} (G : GridDiagram n) (s : Fin n) : GridChain (ZMod 2) (n + 1) →ₗ[ZMod 2] GridChain (ZMod 2) n × GridChain (ZMod 2) n

The fully blocked stabilization comparison: the center part, followed by the X₂-homotopy of the off-center part. The center summand has the (-1,-1) shift.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedStabilizeXMap_fst {n : ℕ} (G : GridDiagram n) (s : Fin n) (c : GridChain (ZMod 2) (n + 1)) : ((G.fullyBlockedStabilizeXMap s) c).1 = (G.stabilizeXCenterProjection s (ZMod 2)).constantCoeffReduction c

The first component of the fully blocked stabilization map is the reduced center projection.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedStabilizeXMap_snd {n : ℕ} (G : GridDiagram n) (s : Fin n) (c : GridChain (ZMod 2) (n + 1)) : ((G.fullyBlockedStabilizeXMap s) c).2 = (G.stabilizeXOffCenterToCenter s (ZMod 2)).constantCoeffReduction ((G.stabilizeXOffCenterProjection s (ZMod 2)).constantCoeffReduction c)

The second component is the reduced X₂-homotopy of the off-center part.

theorem TauCeti.GridDiagram.fullyBlockedStabilizeXMap_comp_differential {n : ℕ} (G : GridDiagram n) (s : Fin n) : G.fullyBlockedStabilizeXMap s ∘ₗ (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedDifferential = G.fullyBlockedDifferential.prodMap G.fullyBlockedDifferential ∘ₗ G.fullyBlockedStabilizeXMap s

The fully blocked stabilization comparison intertwines the differentials.

The following concrete one-object presentations keep the coefficient carriers of the reductions explicit. All comparison components are maps of those actual carriers.

noncomputable def TauCeti.GridDiagram.fullyBlockedHomologyStabilizeXEquivProd {n : ℕ} (G : GridDiagram n) (s : Fin n) : (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedHomology ≃ₗ[ZMod 2] G.fullyBlockedHomology × G.fullyBlockedHomology

The fully blocked homology of an X-split stabilization is two copies of the original homology. The equivalence is induced by fullyBlockedStabilizeXMap; it concerns ungraded vector spaces.

noncomputable def TauCeti.GridDiagram.fullyBlockedStabilizeXCycles {n : ℕ} (G : GridDiagram n) (s : Fin n) : ↥(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedCycles →ₗ[ZMod 2] ↥G.fullyBlockedCycles × ↥G.fullyBlockedCycles

The stabilization comparison takes cycles to pairs of cycles.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedStabilizeXCycles_fst {n : ℕ} (G : GridDiagram n) (s : Fin n) (z : ↥(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedCycles) : ↑((G.fullyBlockedStabilizeXCycles s) z).1 = (G.stabilizeXCenterProjection s (ZMod 2)).constantCoeffReduction ↑z

The first cycle representative is the center part of the stabilized cycle.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedStabilizeXCycles_snd {n : ℕ} (G : GridDiagram n) (s : Fin n) (z : ↥(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedCycles) : ↑((G.fullyBlockedStabilizeXCycles s) z).2 = (G.stabilizeXOffCenterToCenter s (ZMod 2)).constantCoeffReduction ((G.stabilizeXOffCenterProjection s (ZMod 2)).constantCoeffReduction ↑z)

The second cycle representative is the reduced X₂-homotopy of its off-center part.

theorem TauCeti.GridDiagram.coe_fst_fullyBlockedStabilizeXCycles {n : ℕ} (G : GridDiagram n) (s : Fin n) (z : ↥(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedCycles) : ↑((G.fullyBlockedStabilizeXCycles s) z).1 = ((G.fullyBlockedStabilizeXMap s) ↑z).1

The first cycle representative is the first component of the chain comparison.

theorem TauCeti.GridDiagram.coe_snd_fullyBlockedStabilizeXCycles {n : ℕ} (G : GridDiagram n) (s : Fin n) (z : ↥(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedCycles) : ↑((G.fullyBlockedStabilizeXCycles s) z).2 = ((G.fullyBlockedStabilizeXMap s) ↑z).2

The second cycle representative is the second component of the chain comparison.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedHomologyStabilizeXEquivProd_mk {n : ℕ} (G : GridDiagram n) (s : Fin n) (z : ↥(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedCycles) : (G.fullyBlockedHomologyStabilizeXEquivProd s) (Submodule.Quotient.mk z) = (Submodule.Quotient.mk ((G.fullyBlockedStabilizeXCycles s) z).1, Submodule.Quotient.mk ((G.fullyBlockedStabilizeXCycles s) z).2)

The stabilization equivalence sends the class of a cycle to the classes of the two specified comparison cycles.

theorem TauCeti.GridDiagram.finrank_fullyBlockedHomology_stabilizeX {n : ℕ} (G : GridDiagram n) (s : Fin n) : Module.finrank (ZMod 2) (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedHomology = 2 * Module.finrank (ZMod 2) G.fullyBlockedHomology

An X-split stabilization doubles the fully blocked homology dimension.