Documentation

TauCeti.KnotTheory.Grid.Stabilization.XHomotopy

The X-marking homotopy of a stabilized grid #

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. Its new 2 × 2 block is centered at c = (s.succ, (G.X s).succ): the two X-markings of the block lie northwest and southeast of c and the new O-marking southwest of it. Write X₂ for the southeast X-marking, the one in column s.succ, and S = R[V₀, …, V_n] for the coefficient ring of GC⁻(G'). The row of X₂ also carries the new O-marking, in column s.castSucc.

By TauCeti.KnotTheory.Grid.Stabilization.Cone, GC⁻(G') is the mapping cone of the connecting map ∂_I^N from the center complex I (states containing c) to the off-center complex N. This file studies the component H_I^N : N → I of the X-marking homotopy H_{X₂} of G', which counts the empty rectangles from an off-center state to a center state whose only covered X-marking is X₂.

The X-marking homotopy satisfies ∂⁻ ∘ H_{X₂} + H_{X₂} ∘ ∂⁻ = V_{s.succ} + V_{s.castSucc} on GC⁻(G') in characteristic two. The component of H_{X₂} between center states vanishes (XHomotopyCoefficient_stabilizeX_succ_insertPoint): a rectangle between states containing c that covers the square of X₂ also covers the square of the other X-marking of the block. Together with the vanishing of the N-to-I block of ∂⁻, reading off the two blocks of the homotopy identity with target I gives:

In characteristic two, V_{s.succ} + V_{s.castSucc} is the difference of the variable of the new O-marking and the variable of the old O-marking of column s. By the first identity, the pair (𝟙, H_I^N) maps the mapping cone of ∂_I^N, that is GC⁻(G'), to the mapping cone of multiplication by this difference on I; the latter is the cone that HomologicalComplex.polynomialExtensionMulXSubCHomotopyEquiv compares with GC⁻(G), once I is identified with the polynomial extension of GC⁻(G) in the new variable. The map of cones is a quasi-isomorphism when H_I^N is; both steps are carried out in TauCeti.KnotTheory.Grid.Stabilization.Map.Basic.

Main definitions #

Main results #

References #

In Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2, the fully blocked version of H_I^N, counting the rectangles from N to I whose only marking is X₂, compares the two halves of the mapping cone in the proof of stabilization invariance. The mapping cone of V₁ - V₂ is the one of Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.2.

source
@[simp]
theorem TauCeti.GridDiagram.XHomotopyCoefficient_stabilizeX_succ_insertPoint {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x y : GridState n) :
(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XHomotopyCoefficient R s.succ (x.insertPoint s.succ (G.X.toPerm s).succ) (y.insertPoint s.succ (G.X.toPerm s).succ) = 0

The center block of the X₂-homotopy vanishes. The X-marking homotopy of the southeast X-marking of the new block has no matrix coefficient between two grid states containing the center c = (s.succ, (G.X s).succ): such a rectangle is transported from a rectangle of G, and if it covers the square of that X-marking it also covers the square of the northwest one.

source
@[simp]
theorem TauCeti.GridDiagram.stabilizeXCenterProjection_XHomotopy_centerInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : GridState n →₀ MvPolynomial (Fin (n + 1)) R) :
(G.stabilizeXCenterProjection s R) (((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XHomotopy R s.succ) ((G.stabilizeXCenterInclusion s R) f)) = 0

The component of the X₂-homotopy from center states to center states vanishes.

source
noncomputable def TauCeti.GridDiagram.stabilizeXOffCenterToCenter {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :
(G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R) →ₗ[MvPolynomial (Fin (n + 1)) R] GridState n →₀ MvPolynomial (Fin (n + 1)) R

The component H_I^N of the X-marking homotopy of the southeast X-marking X₂ of the new block, from off-center states to center states. It counts the empty rectangles from a state not containing the center of the block to one containing it whose only covered X-marking is X₂.

Instances For
    source
    @[simp]
    theorem TauCeti.GridDiagram.stabilizeXOffCenterToCenter_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y : G.StabilizeXOffCenterState s) (x : GridState n) :
    ((G.stabilizeXOffCenterToCenter s R) (Finsupp.single y 1)) x = (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XHomotopyCoefficient R s.succ (↑y) (x.insertPoint s.succ (G.X.toPerm s).succ)

    The matrix coefficients of H_I^N are those of the X₂-homotopy of the stabilization, from an off-center state to a center state.

    source
    theorem TauCeti.GridDiagram.stabilizeXOffCenterToCenter_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (g : G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R) (x : GridState n) :
    ((G.stabilizeXOffCenterToCenter s R) g) x = g.sum fun (y : G.StabilizeXOffCenterState s) (a : MvPolynomial (Fin (n + 1)) R) => a * (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XHomotopyCoefficient R s.succ (↑y) (x.insertPoint s.succ (G.X.toPerm s).succ)

    The coefficient of a center state x in H_I^N g sums, over the off-center states y, the coefficient of y in g times the matrix coefficient of the X₂-homotopy from y to the state with the center inserted into x.

    source
    theorem TauCeti.GridDiagram.stabilizeXOffCenterToCenter_comp_connecting {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] [CharP R 2] :
    G.stabilizeXOffCenterToCenter s R ∘ₗ G.stabilizeXConnecting s R = (MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • LinearMap.id

    H_I^N inverts the connecting map up to V_{s.succ} + V_{s.castSucc}. Following the connecting map from center states to off-center states by H_I^N is multiplication by V_{s.succ} + V_{s.castSucc}, the sum of the variables of the old O-marking of column s and of the new O-marking.

    source
    theorem TauCeti.GridDiagram.stabilizeXOffCenterToCenter_comp_offCenterDifferential {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
    G.stabilizeXOffCenterToCenter s R ∘ₗ G.stabilizeXOffCenterDifferential s R = G.stabilizeXCenterDifferential s R ∘ₗ G.stabilizeXOffCenterToCenter s R

    H_I^N is a chain map. It intertwines the off-center differential with the center differential.

    The chain map #

    source
    noncomputable def TauCeti.GridDiagram.stabilizeXOffCenterToCenterHom {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
    G.stabilizeXOffCenterComplex s R ⟶ G.stabilizeXCenterComplex s R

    The component H_I^N of the X₂-homotopy, as a chain map from the off-center complex to the center complex.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridDiagram.stabilizeXOffCenterToCenterHom_f {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Unit) :
      (G.stabilizeXOffCenterToCenterHom s R).f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.stabilizeXOffCenterToCenter s R)) (CategoryTheory.eqToHom ⋯))

      The component of the chain map H_I^N is stabilizeXOffCenterToCenter.

      source
      theorem TauCeti.GridDiagram.stabilizeXConnectingHom_comp_offCenterToCenterHom {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :
      CategoryTheory.CategoryStruct.comp (G.stabilizeXConnectingHom s R) (G.stabilizeXOffCenterToCenterHom s R) = (MvPolynomial.X s.succ + MvPolynomial.X s.castSucc) • CategoryTheory.CategoryStruct.id (G.stabilizeXCenterComplex s R)

      The connecting chain map followed by H_I^N is multiplication by V_{s.succ} + V_{s.castSucc} on the center complex.