Documentation

TauCeti.KnotTheory.Grid.Stabilization.Cone

The unblocked complex of a stabilized grid as a mapping cone #

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, whose new 2 × 2 block is centered at the grid point c = (s.succ, (G.X s).succ) (see TauCeti.KnotTheory.Grid.Stabilization.Unblocked). Write S = R[V₀, …, V_n] for the coefficient ring of GC⁻(G').

The grid states of G' split into the center states, those containing c, and the off-center states (the sets I and N of Ozsváth--Stipsicz--Szabó). The center states are the states x.insertPoint s.succ (G.X s).succ for x a grid state of G, so as an S-module

GC⁻(G') = (GridState n →₀ S) ⊕ (off-center states →₀ S).

The unblocked differential has no component from off-center states to center states (unblockedCoefficient_stabilizeX_eq_zero), so the off-center states span a subcomplex, and in characteristic two GC⁻(G') is the mapping cone of the component of ∂⁻ from the center block to the off-center block. This file packages that statement with Mathlib's homotopyCofiber.

The center complex has the grid states of G as generators and, by unblockedCoefficient_stabilizeX_insertPoint, the differential of GC⁻(G) with its variables renamed into S (stabilizeXCenterDifferential_single_apply). The variable of the new O-marking never occurs, so this is GC⁻(G) with one free variable adjoined.
The off-center complex is the subcomplex spanned by the off-center states.
The connecting map is the component of ∂⁻ from center states to off-center states.

The stabilization invariance of GH⁻ then reduces to comparing the off-center complex and the connecting map with GC⁻(G) and multiplication by V₁ - V₂; that comparison is not made here.

Main definitions #

TauCeti.GridDiagram.stabilizeXConeStateEquiv: identifies the off-center states together with the grid states of G (the center states) with all grid states of G'.
TauCeti.GridDiagram.stabilizeXCenterComplex: the complex of center states.
TauCeti.GridDiagram.stabilizeXOffCenterComplex: the complex of off-center states.
TauCeti.GridDiagram.stabilizeXConnectingHom: the connecting chain map between them.
TauCeti.GridDiagram.unblockedComplexStabilizeXIsoHomotopyCofiber: the isomorphism of GC⁻(G') with the mapping cone of the connecting chain map.

Main results #

TauCeti.GridDiagram.unblockedDifferential_comp_stabilizeXCenterInclusion and TauCeti.GridDiagram.unblockedDifferential_comp_stabilizeXOffCenterInclusion: the block lower-triangular form of ∂⁻ on GC⁻(G').

References #

This is the decomposition of the stabilized complex as a mapping cone in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2.

@[reducible, inline]

abbrev TauCeti.GridDiagram.StabilizeXOffCenterState {n : ℕ} (G : GridDiagram n) (s : Fin n) :

The grid states of the X-stabilization G.stabilizeX s.castSucc (G.X s).castSucc s that do not contain the center (s.succ, (G.X s).succ) of its new block.

Instances For

noncomputable def TauCeti.GridDiagram.stabilizeXConeStateEquiv {n : ℕ} (G : GridDiagram n) (s : Fin n) :

G.StabilizeXOffCenterState s ⊕ GridState n ≃ GridState (n + 1)

Mapping-cone generators for the fully blocked X-stabilization comparison are naturally the grid states of the stabilized diagram. The left summand consists of off-center states; the right summand consists of states obtained by inserting the center of the new block.

Instances For

@[simp]

theorem TauCeti.GridDiagram.stabilizeXConeStateEquiv_apply_inl {n : ℕ} (G : GridDiagram n) (s : Fin n) (y : G.StabilizeXOffCenterState s) :

(G.stabilizeXConeStateEquiv s) (Sum.inl y) = ↑y

The cone-state equivalence sends an off-center generator to its underlying stabilized state.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXConeStateEquiv_apply_inr {n : ℕ} (G : GridDiagram n) (s : Fin n) (x : GridState n) :

(G.stabilizeXConeStateEquiv s) (Sum.inr x) = x.insertPoint s.succ (G.X.toPerm s).succ

The cone-state equivalence sends a center generator to the state with the center inserted.

noncomputable def TauCeti.GridDiagram.stabilizeXCenterInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

(GridState n →₀ MvPolynomial (Fin (n + 1)) R) →ₗ[MvPolynomial (Fin (n + 1)) R] GridChainMinus R (n + 1)

The inclusion of the center block: a grid state x of G goes to the state of the stabilization obtained by inserting the center of the new block.

Instances For

noncomputable def TauCeti.GridDiagram.stabilizeXCenterProjection {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

GridChainMinus R (n + 1) →ₗ[MvPolynomial (Fin (n + 1)) R] GridState n →₀ MvPolynomial (Fin (n + 1)) R

The projection onto the center block, reading off the coefficients of the states containing the center of the new block.

Instances For

noncomputable def TauCeti.GridDiagram.stabilizeXOffCenterInclusion {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] GridChainMinus R (n + 1)

The inclusion of the off-center block.

Instances For

noncomputable def TauCeti.GridDiagram.stabilizeXOffCenterProjection {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

GridChainMinus R (n + 1) →ₗ[MvPolynomial (Fin (n + 1)) R] G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R

The projection onto the off-center block.

Instances For

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterInclusion_single {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x : GridState n) (a : MvPolynomial (Fin (n + 1)) R) :

(G.stabilizeXCenterInclusion s R) (Finsupp.single x a) = Finsupp.single (x.insertPoint s.succ (G.X.toPerm s).succ) a

The center inclusion inserts the center of the new block into a generator.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterProjection_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : GridChainMinus R (n + 1)) (x : GridState n) :

((G.stabilizeXCenterProjection s R) f) x = f (x.insertPoint s.succ (G.X.toPerm s).succ)

The center projection reads off the coefficient of the state with the center inserted.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterInclusion_single {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y : G.StabilizeXOffCenterState s) (a : MvPolynomial (Fin (n + 1)) R) :

(G.stabilizeXOffCenterInclusion s R) (Finsupp.single y a) = Finsupp.single (↑y) a

The off-center inclusion sends a generator to the same grid state.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterProjection_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : GridChainMinus R (n + 1)) (y : G.StabilizeXOffCenterState s) :

((G.stabilizeXOffCenterProjection s R) f) y = f ↑y

The off-center projection restricts a chain to the off-center states.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterInclusion_projection_add_offCenter {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : GridChainMinus R (n + 1)) :

(G.stabilizeXCenterInclusion s R) ((G.stabilizeXCenterProjection s R) f) + (G.stabilizeXOffCenterInclusion s R) ((G.stabilizeXOffCenterProjection s R) f) = f

Every chain of the stabilization is the sum of its center and off-center parts.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterProjection_inclusion {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.stabilizeXCenterInclusion s R) f) = f

The center projection is a retraction of the center inclusion.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterProjection_inclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R) :

(G.stabilizeXOffCenterProjection s R) ((G.stabilizeXOffCenterInclusion s R) f) = f

The off-center projection is a retraction of the off-center inclusion.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterProjection_offCenterInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R) :

(G.stabilizeXCenterProjection s R) ((G.stabilizeXOffCenterInclusion s R) f) = 0

An off-center chain has no center part.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterProjection_centerInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : GridState n →₀ MvPolynomial (Fin (n + 1)) R) :

(G.stabilizeXOffCenterProjection s R) ((G.stabilizeXCenterInclusion s R) f) = 0

A center chain has no off-center part.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterProjection_unblockedDifferential_offCenterInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R) :

(G.stabilizeXCenterProjection s R) (((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R) ((G.stabilizeXOffCenterInclusion s R) f)) = 0

The unblocked differential of the stabilization has no component from off-center states to center states.

noncomputable def TauCeti.GridDiagram.stabilizeXCenterDifferential {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

(GridState n →₀ MvPolynomial (Fin (n + 1)) R) →ₗ[MvPolynomial (Fin (n + 1)) R] GridState n →₀ MvPolynomial (Fin (n + 1)) R

The center block of the unblocked differential of the stabilization.

Instances For

noncomputable def TauCeti.GridDiagram.stabilizeXOffCenterDifferential {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] G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R

The off-center block of the unblocked differential of the stabilization.

Instances For

noncomputable def TauCeti.GridDiagram.stabilizeXConnecting {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

(GridState n →₀ MvPolynomial (Fin (n + 1)) R) →ₗ[MvPolynomial (Fin (n + 1)) R] G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R

The connecting map: the component of the unblocked differential of the stabilization from center states to off-center states.

Instances For

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterDifferential_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x y : GridState n) :

((G.stabilizeXCenterDifferential s R) (Finsupp.single x 1)) y = (MvPolynomial.rename s.castSucc.succAbove) (G.unblockedCoefficient R x y)

The center block is GC⁻(G) over one more variable. The matrix coefficients of the center differential are those of the unblocked differential of G, with the variable of each column renamed to the variable of the corresponding column of the stabilization.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterDifferential_mapRange_rename {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (f : GridChainMinus R n) :

(G.stabilizeXCenterDifferential s R) (Finsupp.mapRange ⇑(MvPolynomial.rename s.castSucc.succAbove) ⋯ f) = Finsupp.mapRange ⇑(MvPolynomial.rename s.castSucc.succAbove) ⋯ ((G.unblockedDifferential R) f)

On chains with coefficients renamed from R[V₀, …, V_{n-1}], the center differential is the unblocked differential of G followed by the renaming of the coefficients.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterDifferential_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y z : G.StabilizeXOffCenterState s) :

((G.stabilizeXOffCenterDifferential s R) (Finsupp.single y 1)) z = (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedCoefficient R ↑y ↑z

The matrix coefficients of the off-center differential are those of the unblocked differential of the stabilization.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXConnecting_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x : GridState n) (z : G.StabilizeXOffCenterState s) :

((G.stabilizeXConnecting s R) (Finsupp.single x 1)) z = (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedCoefficient R (x.insertPoint s.succ (G.X.toPerm s).succ) ↑z

The matrix coefficients of the connecting map are those of the unblocked differential of the stabilization, from a center state to an off-center state.

theorem TauCeti.GridDiagram.unblockedDifferential_comp_stabilizeXCenterInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R ∘ₗ G.stabilizeXCenterInclusion s R = G.stabilizeXCenterInclusion s R ∘ₗ G.stabilizeXCenterDifferential s R + G.stabilizeXOffCenterInclusion s R ∘ₗ G.stabilizeXConnecting s R

The block form of ∂⁻ on center states. On the center block, the unblocked differential of the stabilization is the center differential plus the connecting map.

theorem TauCeti.GridDiagram.unblockedDifferential_comp_stabilizeXOffCenterInclusion {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] :

(G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).unblockedDifferential R ∘ₗ G.stabilizeXOffCenterInclusion s R = G.stabilizeXOffCenterInclusion s R ∘ₗ G.stabilizeXOffCenterDifferential s R

The off-center states span a subcomplex. On the off-center block, the unblocked differential of the stabilization is the off-center differential.

theorem TauCeti.GridDiagram.stabilizeXCenterDifferential_comp_self_eq_zero {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] [CharP R 2] :

G.stabilizeXCenterDifferential s R ∘ₗ G.stabilizeXCenterDifferential s R = 0

The center differential squares to zero.

theorem TauCeti.GridDiagram.stabilizeXOffCenterDifferential_comp_self_eq_zero {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] [CharP R 2] :

G.stabilizeXOffCenterDifferential s R ∘ₗ G.stabilizeXOffCenterDifferential s R = 0

The off-center differential squares to zero.

theorem TauCeti.GridDiagram.stabilizeXConnecting_comp_centerDifferential {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :

G.stabilizeXConnecting s R ∘ₗ G.stabilizeXCenterDifferential s R = G.stabilizeXOffCenterDifferential s R ∘ₗ G.stabilizeXConnecting s R

The connecting map intertwines the center and off-center differentials.

The mapping cone #

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

HomologicalComplex (ModuleCat (MvPolynomial (Fin (n + 1)) R)) (ComplexShape.refl Unit)

The complex of center states: the center block of the unblocked complex of the stabilization, as a one-object complex over R[V₀, …, V_n]. Its generators are the grid states of G, and its differential is that of GC⁻(G) with the variables renamed (stabilizeXCenterDifferential_single_apply).

Instances For

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterComplex_X {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Unit) :

(G.stabilizeXCenterComplex s R).X i = ↧(GridState n →₀ MvPolynomial (Fin (n + 1)) R)

The unique object of the center complex is the free module on the grid states of G.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXCenterComplex_d {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :

(G.stabilizeXCenterComplex s R).d () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.stabilizeXCenterDifferential s R)) (CategoryTheory.eqToHom ⋯))

The unique differential of the center complex is the center differential.

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

HomologicalComplex (ModuleCat (MvPolynomial (Fin (n + 1)) R)) (ComplexShape.refl Unit)

The complex of off-center states: the subcomplex of the unblocked complex of the stabilization spanned by the grid states not containing the center of the new block.

Instances For

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterComplex_X {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Unit) :

(G.stabilizeXOffCenterComplex s R).X i = ↧(G.StabilizeXOffCenterState s →₀ MvPolynomial (Fin (n + 1)) R)

The unique object of the off-center complex is the free module on the off-center states.

@[simp]

theorem TauCeti.GridDiagram.stabilizeXOffCenterComplex_d {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :

(G.stabilizeXOffCenterComplex s R).d () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.stabilizeXOffCenterDifferential s R)) (CategoryTheory.eqToHom ⋯))

The unique differential of the off-center complex is the off-center differential.

noncomputable def TauCeti.GridDiagram.stabilizeXConnectingHom {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :

G.stabilizeXCenterComplex s R ⟶ G.stabilizeXOffCenterComplex s R

The connecting map as a chain map from the center complex to the off-center complex.

Instances For

@[simp]

theorem TauCeti.GridDiagram.stabilizeXConnectingHom_f {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Unit) :

(G.stabilizeXConnectingHom s R).f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.stabilizeXConnecting s R)) (CategoryTheory.eqToHom ⋯))

The component of the connecting chain map is the connecting map.

noncomputable def TauCeti.GridDiagram.unblockedComplexStabilizeXIsoHomotopyCofiber {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).unblockedComplex R ≅ HomologicalComplex.homotopyCofiber (G.stabilizeXConnectingHom s R)

The unblocked complex of an X-stabilization is a mapping cone. The unblocked complex GC⁻ of the stabilization G.stabilizeX s.castSucc (G.X s).castSucc s is isomorphic to the mapping cone of the connecting chain map from the center complex (the states containing the center of the new block) to the off-center complex (the other states).

Instances For

@[simp]

theorem TauCeti.GridDiagram.unblockedComplexStabilizeXIsoHomotopyCofiber_hom_f {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :

The isomorphism with the mapping cone sends a chain to its center part in the first summand of the cone and to its off-center part in the second.

@[simp]

theorem TauCeti.GridDiagram.unblockedComplexStabilizeXIsoHomotopyCofiber_inv_f {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommRing R] [CharP R 2] :

The inverse isomorphism includes the first summand of the cone as the center states and the second as the off-center states.