The chain map of an X-stabilization

Let G be a grid diagram of size n, let s be a column, and let G' = G.stabilizeX s.castSucc (G.X s).castSucc s be the stabilization splitting the X-marking of column s. Write A = R[V₀, …, V_{n-1}] and S = R[V₀, …, V_n] for the coefficient rings of GC⁻(G) and GC⁻(G'), with S an A-algebra through the renaming of the columns of G into those of G'.

This file assembles the comparison map GC⁻(G') ⟶ GC⁻(G) of complexes of A-modules from the three pieces already available:

• GC⁻(G') is the mapping cone of the connecting map ∂_I^N from the center complex I to the off-center complex N (unblockedComplexStabilizeXIsoHomotopyCofiber);
• the component H_I^N : N ⟶ I of the X-marking homotopy satisfies ∂_I^N ≫ H_I^N = V_{s.succ} + V_{s.castSucc} (stabilizeXConnectingHom_comp_offCenterToCenterHom), so the pair (𝟙, H_I^N) is a morphism from the arrow ∂_I^N to the arrow given by multiplication by V_{s.succ} + V_{s.castSucc} on I, and induces a map of mapping cones (stabilizeXConeMap);
• after restricting scalars to A, the mapping cone of multiplication by V_{s.succ} + V_{s.castSucc} on I is homotopy equivalent to GC⁻(G) (stabilizeXCenterConeHomotopyEquiv).

On off-center chains the composite stabilizeXMap is H_I^N followed by the evaluation V_{s.castSucc} ↦ V_s that merges the two variables of the new block (map_offCenterInclusion_comp_stabilizeXMap). It vanishes on center chains (map_centerInclusion_comp_stabilizeXMap). Since maps of mapping cones induced by quasi-isomorphisms are quasi-isomorphisms (HomologicalComplex.homotopyCofiber.quasiIso_mapArrowHom), stabilizeXMap is a quasi-isomorphism as soon as H_I^N is (quasiIso_stabilizeXMap). This reduces the stabilization invariance of GH⁻ for this stabilization to the statement that H_I^N is a quasi-isomorphism, which is proved in TauCeti.KnotTheory.Grid.Stabilization.Comparison.

Main definitions

• TauCeti.GridDiagram.stabilizeXConeMap: the map of mapping cones induced by (𝟙, H_I^N).
• TauCeti.GridDiagram.stabilizeXMap: the chain map GC⁻(G') ⟶ GC⁻(G) of complexes of A-modules.

Main results

• TauCeti.GridDiagram.quasiIso_stabilizeXConeMap and TauCeti.GridDiagram.quasiIso_stabilizeXMap: both maps are quasi-isomorphisms if H_I^N is.
• TauCeti.GridDiagram.map_offCenterInclusion_comp_stabilizeXMap: on off-center chains, stabilizeXMap is H_I^N followed by evaluation at V_s.
• TauCeti.GridDiagram.stabilizeXMap_f_apply: on an arbitrary chain, stabilizeXMap is H_I^N of its off-center part with the coefficients renamed along s.predAbove.
• TauCeti.GridDiagram.inlX_stabilizeXConeMap and TauCeti.GridDiagram.map_centerInclusion_comp_stabilizeXMap: the cone map is the identity on the center summand, while stabilizeXMap vanishes there.

References

This is the comparison of the stabilized complex with the mapping cone of V₁ - V₂ in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.2.

noncomputable def TauCeti.GridDiagram.stabilizeXConeMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] : HomologicalComplex.homotopyCofiber (G.stabilizeXConnectingHom s R) ⟶ HomologicalComplex.homotopyCofiber ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R))

The map of mapping cones induced by H_I^N. The pair (𝟙, H_I^N) maps the connecting map ∂_I^N from the center complex to the off-center complex to multiplication by V_{s.succ} + V_{s.castSucc} on the center complex, and so induces a map from the mapping cone of ∂_I^N, which is GC⁻(G'), to the mapping cone of V_{s.succ} + V_{s.castSucc}.

@[simp]

theorem TauCeti.GridDiagram.inr_stabilizeXConeMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (G.stabilizeXConnectingHom s R)) (G.stabilizeXConeMap s R) = CategoryTheory.CategoryStruct.comp (G.stabilizeXOffCenterToCenterHom s R) (HomologicalComplex.homotopyCofiber.inr ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R)))

On the off-center summand of the cone, stabilizeXConeMap is H_I^N followed by the inclusion of the center complex into the cone of V_{s.succ} + V_{s.castSucc}.

@[simp]

theorem TauCeti.GridDiagram.inr_stabilizeXConeMap_assoc {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] {Z : HomologicalComplex (ModuleCat (MvPolynomial (Fin (n + 1)) R)) (ComplexShape.refl Unit)} (h : HomologicalComplex.homotopyCofiber ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr (G.stabilizeXConnectingHom s R)) (CategoryTheory.CategoryStruct.comp (G.stabilizeXConeMap s R) h) = CategoryTheory.CategoryStruct.comp (G.stabilizeXOffCenterToCenterHom s R) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inr ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R))) h)

On the off-center summand of the cone, stabilizeXConeMap is H_I^N followed by the inclusion of the center complex into the cone of V_{s.succ} + V_{s.castSucc}.

@[simp]

theorem TauCeti.GridDiagram.inlX_stabilizeXConeMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (G.stabilizeXConnectingHom s R) () () ⋯) ((G.stabilizeXConeMap s R).f ()) = HomologicalComplex.homotopyCofiber.inlX ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R)) () () ⋯

On the center summand, stabilizeXConeMap is the identity into the center summand of the target cone.

@[simp]

theorem TauCeti.GridDiagram.inlX_stabilizeXConeMap_assoc {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] {Z : ModuleCat (MvPolynomial (Fin (n + 1)) R)} (h : (HomologicalComplex.homotopyCofiber ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R))).X () ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX (G.stabilizeXConnectingHom s R) () () ⋯) (CategoryTheory.CategoryStruct.comp ((G.stabilizeXConeMap s R).f ()) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX ((MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R)) () () ⋯) h

On the center summand, stabilizeXConeMap is the identity into the center summand of the target cone.

theorem TauCeti.GridDiagram.quasiIso_stabilizeXConeMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] [QuasiIso (G.stabilizeXOffCenterToCenterHom s R)] : QuasiIso (G.stabilizeXConeMap s R)

The map of cones stabilizeXConeMap is a quasi-isomorphism if H_I^N is.

noncomputable def TauCeti.GridDiagram.stabilizeXMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] : ((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).mapHomologicalComplex (ComplexShape.refl Unit)).obj ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedComplex R) ⟶ G.unblockedComplex R

The chain map of an X-stabilization. The map GC⁻(G') ⟶ GC⁻(G) of complexes of A-modules obtained by presenting GC⁻(G') as the mapping cone of ∂_I^N, applying the map of cones induced by (𝟙, H_I^N), and comparing the mapping cone of V_{s.succ} + V_{s.castSucc} on the center complex with GC⁻(G). The source is GC⁻(G') with scalars restricted to A.

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

Stabilization invariance reduces to H_I^N. The chain map GC⁻(G') ⟶ GC⁻(G) of an X-stabilization is a quasi-isomorphism if the component H_I^N of the X-marking homotopy from off-center states to center states is.

@[simp]

theorem TauCeti.GridDiagram.map_offCenterInclusion_comp_stabilizeXMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] : CategoryTheory.CategoryStruct.comp (((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).mapHomologicalComplex (ComplexShape.refl Unit)).map (HomologicalComplex.homotopyCofiber.inr (G.stabilizeXConnectingHom s R))) (CategoryTheory.CategoryStruct.comp (((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).mapHomologicalComplex (ComplexShape.refl Unit)).map (G.unblockedComplexStabilizeXIsoHomotopyCofiber s R).inv) (G.stabilizeXMap s R)) = CategoryTheory.CategoryStruct.comp (((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).mapHomologicalComplex (ComplexShape.refl Unit)).map (G.stabilizeXOffCenterToCenterHom s R)) (CategoryTheory.CategoryStruct.comp (G.polynomialExtensionIsoStabilizeXCenter s R).inv ((G.unblockedComplex R).polynomialExtensionEval (MvPolynomial.X s)))

On off-center chains, the chain map of an X-stabilization is H_I^N followed by the evaluation V_{s.castSucc} ↦ V_s of the polynomial extension of GC⁻(G). Here homotopyCofiber.inr _ ≫ (unblockedComplexStabilizeXIsoHomotopyCofiber G s R).inv is the inclusion of the off-center complex into GC⁻(G').

@[simp]

theorem TauCeti.GridDiagram.map_centerInclusion_comp_stabilizeXMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] : CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).map (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).map (ModuleCat.ofHom (G.stabilizeXCenterInclusion s R))) (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).map (CategoryTheory.eqToHom ⋯)) ((G.stabilizeXMap s R).f ()))) = 0

On center states, stabilizeXMap vanishes. The first factor includes the center summand of the cone into GC⁻(G'), with scalars restricted to A.

theorem TauCeti.GridDiagram.stabilizeXMap_f_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u) [CommRing R] [CharP R 2] (c : GridChainMinus R (n + 1)) : (ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars ↑(MvPolynomial.rename s.castSucc.succAbove)).map (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp ((G.stabilizeXMap s R).f ()) (CategoryTheory.eqToHom ⋯)))) c = Finsupp.mapRange ⇑(MvPolynomial.rename s.predAbove) ⋯ ((G.stabilizeXOffCenterToCenter s R) ((G.stabilizeXOffCenterProjection s R) c))

The chain map of an X-stabilization on chains. On a chain c of GC⁻(G'), stabilizeXMap is H_I^N applied to the off-center part of c, followed by renaming every coefficient along s.predAbove, which sends both variables V_{s.castSucc} and V_{s.succ} of the new block to V_s and every other variable V_{s.castSucc.succAbove j} to V_j. The eqToHoms identify the chain modules with the underlying free modules.