Stabilization invariance: the reduced comparison is a quasi-isomorphism

Let G' = G.stabilizeX s.castSucc (G.X s).castSucc s be the stabilization of a grid diagram G splitting the X-marking of column s, write κ = s.castSucc, ρ = (G.X s).castSucc, and ρ' = (G.X s).succ for the row above ρ. TauCeti.KnotTheory.Grid.Stabilization.Reduction reduces stabilization invariance of GH⁻ along G' to one statement over the coefficient ring R with every variable set to zero: the reduced H_I^N, from the reduced off-center complex (fully blocked rectangles of G' between states not containing the center (s.succ, ρ') of the new block) to the reduced center complex (fully blocked rectangles of G), induces a bijection on homology. This file proves that statement, so H_I^N is a quasi-isomorphism without further hypotheses. With the instance TauCeti.GridDiagram.quasiIso_stabilizeXMap, the comparison map GC⁻(G') ⟶ GC⁻(G) is then a quasi-isomorphism.

The proof shows that the mapping cone of the reduced H_I^N, a square-zero endomorphism of the free module on the generators G.StabilizeXOffCenterState s ⊕ GridState n, is exact (LinearMap.ker_le_range_mappingCone_iff), by the matching criterion LinearMap.ker_le_range_of_matching applied to the generator matching of TauCeti.KnotTheory.Grid.Stabilization.Matching: the involution TauCeti.GridDiagram.stabilizeXMatching swapping the rows ρ and ρ', with the sources TauCeti.GridDiagram.StabilizeXMatchingSource. It remains to show that every term of the cone strictly lowers a weight except the edges of this matching, which have coefficient one.

Generators are weighted lexicographically by the level of their underlying state of G' (GridDiagram.stabilizeXLevel), which is constant on matched pairs (GridDiagram.stabilizeXLevel_stabilizeXMatching), and by the position of the row the state uses in column s.succ, read cyclically from the row above ρ' (Grid.cyclicPosition), a center generator getting the position of ρ. The terms of equal weight are the row swaps, along the thin rectangle in row ρ between a state and its row swap (GridDiagram.stabilizeXRowSwapRectangle); the other rectangles covering no outer square are width-one moves in column κ, which lower the position. A row swap term of the cone is a matching edge:

• between off-center states using neither ρ nor ρ' in column s.succ, the thin rectangle from the source avoids the markings O_new = (κ, ρ) and X₂ = (s.succ, ρ) of row ρ, while the one from its partner covers them;
• an off-center state using ρ in column s.succ is a source, matched with the center state of its row swap along the thin rectangle through X₂ counted by the reduced H_I^N.

Main results

• TauCeti.GridDiagram.homologyMap_constantCoeffReduction_stabilizeXOffCenterToCenter_bijective: the reduced H_I^N induces a bijection on homology.
• TauCeti.GridDiagram.quasiIso_stabilizeXOffCenterToCenterHom: H_I^N is a quasi-isomorphism.

References

The statement is stabilization invariance in the form of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, for the fully blocked comparison. The weight refines the Q-filtration of Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Geom. Topol. 11 (2007), Section 3.2. Where MOST split the associated graded complex, the leading terms are here matched by row swaps, in the sense of algebraic discrete Morse theory (Sköldberg, Trans. Amer. Math. Soc. 358 (2006)).

The row swap rectangle

Rectangles to the row swap

The matching in terms of states

The weight

Rectangles lower the weight

The reduced cone

theorem TauCeti.GridDiagram.homologyMap_constantCoeffReduction_stabilizeXOffCenterToCenter_bijective {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] : Function.Bijective ⇑(LinearMap.homologyMap (G.stabilizeXOffCenterToCenter s R).constantCoeffReduction ⋯ ⋯ ⋯)

The reduced comparison is a quasi-isomorphism. The reduction of H_I^N modulo the variables induces a bijection from the homology of the reduced off-center complex to the homology of the reduced center complex.

instance TauCeti.GridDiagram.quasiIso_stabilizeXOffCenterToCenterHom {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] : QuasiIso (G.stabilizeXOffCenterToCenterHom s R)

H_I^N is a quasi-isomorphism. Together with the instance quasiIso_stabilizeXMap, the chain map GC⁻(G') ⟶ GC⁻(G) of the stabilization splitting the X-marking of column s is a quasi-isomorphism.