Documentation

TauCeti.KnotTheory.Grid.Stabilization.Homology

Stabilization invariance of GH⁻ #

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'), and σ : S → A for the renaming of variables along s.predAbove, which merges the two variables V_{s.castSucc} and V_{s.succ} of the new block into V_s.

The stabilization chain map GC⁻(G') ⟶ GC⁻(G) (GridDiagram.stabilizeXMap) is a quasi-isomorphism of complexes of A-modules (GridDiagram.quasiIso_stabilizeXMap, with GridDiagram.quasiIso_stabilizeXOffCenterToCenterHom). On chains it is H_I^N of the off-center part followed by σ on coefficients, so it is even σ-semilinear over S (GridDiagram.stabilizeXChainMap). This file descends it to a σ-semilinear map GH⁻(G') → GH⁻(G) on unblocked grid homology (GridDiagram.stabilizeXHomologyMap), sending the class of a cycle z to the class of its image, and shows that this map is bijective and, for a diagram with an odd number of components, preserves the Alexander grading.

For a knot grid G, the diagram G' is again a knot grid, and U acts on both homologies as any one variable. Since σ commutes with the evaluation V_j ↦ U, the map on homology is an isomorphism of graded R[U]-modules of Alexander degree zero (GridDiagram.IsKnot.unblockedHomologyIsomorphic_stabilizeX). Only this one stabilization type is treated here; the other stabilization types and commutation moves are not.

Main definitions #

Main results #

References #

This is stabilization invariance of GH⁻ for this stabilization type in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2; see also Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Geom. Topol. 11 (2007), Section 3.2.

The chain map as a semilinear map #

source
noncomputable def TauCeti.GridDiagram.stabilizeXChainMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] :
GridChainMinus R (n + 1) →ₛₗ[↑(MvPolynomial.rename s.predAbove)] GridChainMinus R n

The chain map of an X-stabilization, as a semilinear map. On a chain c of GC⁻(G') it is H_I^N of the off-center part of c, followed by renaming every coefficient along s.predAbove. It is semilinear along that renaming S → A, and its underlying function is the unique component of stabilizeXMap (stabilizeXMap_f_apply).

Instances For
    source
    theorem TauCeti.GridDiagram.stabilizeXChainMap_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] (c : GridChainMinus R (n + 1)) :
    (G.stabilizeXChainMap s R) c = Finsupp.mapRange ⇑(MvPolynomial.rename s.predAbove) ⋯ ((G.stabilizeXOffCenterToCenter s R) ((G.stabilizeXOffCenterProjection s R) c))

    stabilizeXChainMap renames the coefficients of H_I^N of the off-center part.

    source
    theorem TauCeti.GridDiagram.stabilizeXChainMap_unblockedDifferential {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (c : GridChainMinus R (n + 1)) :
    (G.stabilizeXChainMap s R) (((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R) c) = (G.unblockedDifferential R) ((G.stabilizeXChainMap s R) c)

    stabilizeXChainMap is a chain map: it intertwines the unblocked differentials of G' and G.

    source
    theorem TauCeti.GridDiagram.stabilizeXChainMap_mem_ker {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] {c : GridChainMinus R (n + 1)} (hc : c ∈ ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R).ker) :
    (G.stabilizeXChainMap s R) c ∈ (G.unblockedDifferential R).ker

    stabilizeXChainMap sends cycles of GC⁻(G') to cycles of GC⁻(G).

    source
    theorem TauCeti.GridDiagram.exists_sub_stabilizeXChainMap_mem_range {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] {c : GridChainMinus R n} (hc : c ∈ (G.unblockedDifferential R).ker) :
    ∃ m ∈ ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R).ker, c - (G.stabilizeXChainMap s R) m ∈ (G.unblockedDifferential R).range

    Every cycle of GC⁻(G) differs from the image of a cycle of GC⁻(G') by a boundary.

    source
    theorem TauCeti.GridDiagram.mem_range_of_stabilizeXChainMap_mem_range {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] {m : GridChainMinus R (n + 1)} (hm : m ∈ ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R).ker) (h : (G.stabilizeXChainMap s R) m ∈ (G.unblockedDifferential R).range) :
    m ∈ ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R).range

    A cycle of GC⁻(G') whose image in GC⁻(G) is a boundary is itself a boundary.

    The map on homology #

    source
    noncomputable def TauCeti.GridDiagram.stabilizeXHomologyMap {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
    ↑((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedHomology R) →ₛₗ[↑(MvPolynomial.rename s.predAbove)] ↑(G.unblockedHomology R)

    The map of an X-stabilization on unblocked grid homology, GH⁻(G') → GH⁻(G): the class of a cycle z goes to the class of stabilizeXChainMap z. It is semilinear along the renaming S → A along s.predAbove.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridDiagram.stabilizeXHomologyMap_unblockedHomologyClass {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (z : ↥((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R).ker) :
      (G.stabilizeXHomologyMap s R) (((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedHomologyClass R) z) = (G.unblockedHomologyClass R) ⟨(G.stabilizeXChainMap s R) ↑z, ⋯⟩

      stabilizeXHomologyMap sends the class of a cycle z to the class of stabilizeXChainMap z.

      source
      theorem TauCeti.GridDiagram.stabilizeXHomologyMap_bijective {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
      Function.Bijective ⇑(G.stabilizeXHomologyMap s R)

      Stabilization invariance of GH⁻. The map GH⁻(G') → GH⁻(G) induced by the stabilization chain map is bijective.

      source
      noncomputable def TauCeti.GridDiagram.stabilizeXHomologyEquiv {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
      ↑((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedHomology R) ≃ₗ[R] ↑(G.unblockedHomology R)

      The specified X-stabilization comparison on GH⁻, as an equivalence over the ground ring. Its forward map is the existing semilinear stabilization homology map.

      Instances For
        source
        @[simp]
        theorem TauCeti.GridDiagram.stabilizeXHomologyEquiv_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (y : ↑((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedHomology R)) :
        (G.stabilizeXHomologyEquiv s R) y = (G.stabilizeXHomologyMap s R) y

        The forward equivalence is the semilinear homology comparison.

        source
        theorem TauCeti.OddComponentGridDiagram.stabilizeXHomologyMap_mem_alexanderUnblockedHomologyGrading_piece {n : ℕ} (G : OddComponentGridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] {a : ℤ} {y : ↑(((↑G).stabilizeX s.castSucc ((↑G).X.toPerm s).castSucc s).unblockedHomology R)} (hy : y ∈ (alexanderUnblockedHomologyGrading ⟨(↑G).stabilizeX s.castSucc ((↑G).X.toPerm s).castSucc s, ⋯⟩ R).piece ℤ a) :
        ((↑G).stabilizeXHomologyMap s R) y ∈ (G.alexanderUnblockedHomologyGrading R).piece ℤ a

        The map of an X-stabilization on GH⁻ preserves the Alexander grading. The stabilization G' of G again has an odd number of components, and a class of GH⁻(G') of Alexander degree a goes to a class of GH⁻(G) of Alexander degree a.

        source
        theorem TauCeti.GridDiagram.IsKnot.unblockedHomologyIsomorphic_stabilizeX {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (s : Fin n) (K : Type u_1) [CommRing K] [CharP K 2] :
        hG.UnblockedHomologyIsomorphic ⋯ K

        GH⁻ is invariant under X-stabilization. The stabilization of a knot grid G splitting the X-marking of column s is a knot grid whose GH⁻ is isomorphic to GH⁻(G) as an Alexander-graded K[U]-module.