Documentation

TauCeti.KnotTheory.Grid.Stabilization.Reduction

Stabilization invariance reduced to a comparison modulo the variables #

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 S = R[V₀, …, V_n] for the coefficient ring of GC⁻(G'). By TauCeti.KnotTheory.Grid.Stabilization.Map.Basic, the comparison map GC⁻(G') ⟶ GC⁻(G) is a quasi-isomorphism as soon as the component H_I^N : N ⟶ I of the X₂-homotopy, from the off-center complex N to the center complex I, is one. This file reduces that remaining hypothesis to a statement in which every variable is set to zero.

Both N and I are free S-modules on finitely many grid states of G', and their differentials and H_I^N count empty rectangles weighted by the monomials V^{O(r)}. Giving each variable the weight -2, the matrix coefficient between two states x and y is weighted homogeneous of degree M_O(x) - 1 - M_O(y), for M_O the O-Maslov grading of G' (GridDiagram.isWeightedHomogeneous_sum_OMonomial). The graded Nakayama argument of TauCeti.Algebra.Homology.ReductionModVariables therefore applies: H_I^N is a quasi-isomorphism if its reduction modulo the variables V₀, …, V_n, LinearMap.constantCoeffReduction, induces a bijection between the homologies of the reductions of the two differentials (quasiIso_stabilizeXOffCenterToCenterHom_of_bijective).

The two reduced differentials give R-linear fully blocked rectangle-count complexes. The reduction of the center differential counts the fully blocked rectangles of G, so over R = ZMod 2 its complex agrees with the library's fully blocked complex of G (constantCoeffReduction_stabilizeXCenterDifferential_eq_fullyBlockedDifferential). The reduction of the off-center differential counts the fully blocked rectangles of G' between off-center states (constantCoeffReduction_stabilizeXOffCenterDifferential_single_apply). The reduction of H_I^N counts the empty rectangles from an off-center state to a center state with no O-marking and whose only X-marking is X₂ (constantCoeffReduction_stabilizeXOffCenterToCenter_single_apply). That this reduced comparison induces a bijection on homology is the combinatorial content of stabilization invariance, proved in TauCeti.KnotTheory.Grid.Stabilization.Comparison.

Main results #

References #

The fully blocked comparison map is the one of Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.2; the passage between the fully blocked and the unblocked theory is the graded algebra of its Appendix A.

The O-Maslov grading of the two blocks #

source
theorem TauCeti.GridDiagram.isWeightedHomogeneous_stabilizeXCenterDifferential_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x y : GridState n) :
MvPolynomial.IsWeightedHomogeneous (fun (x : Fin (n + 1)) => -2) (((G.stabilizeXCenterDifferential s R) (Finsupp.single x 1)) y) ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ (x.insertPoint s.succ (G.X.toPerm s).succ) - 1 - (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ (y.insertPoint s.succ (G.X.toPerm s).succ))

The center differential lowers the O-Maslov grading of the stabilization by one: with every variable of weight -2, its matrix coefficient from x to y is weighted homogeneous of degree M_O(x') - 1 - M_O(y'), for x' and y' the states of the stabilization containing the center of the new block.

source
theorem TauCeti.GridDiagram.isWeightedHomogeneous_stabilizeXOffCenterDifferential_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y z : G.StabilizeXOffCenterState s) :
MvPolynomial.IsWeightedHomogeneous (fun (x : Fin (n + 1)) => -2) (((G.stabilizeXOffCenterDifferential s R) (Finsupp.single y 1)) z) ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ ↑y - 1 - (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ ↑z)

The off-center differential lowers the O-Maslov grading of the stabilization by one.

source
theorem TauCeti.GridDiagram.isWeightedHomogeneous_stabilizeXOffCenterToCenter_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y : G.StabilizeXOffCenterState s) (x : GridState n) :
MvPolynomial.IsWeightedHomogeneous (fun (x : Fin (n + 1)) => -2) (((G.stabilizeXOffCenterToCenter s R) (Finsupp.single y 1)) x) ((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ ↑y - 1 - (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).maslovOℤ (x.insertPoint s.succ (G.X.toPerm s).succ))

The component H_I^N of the X₂-homotopy lowers the O-Maslov grading of the stabilization by one: like the differential, it counts empty rectangles weighted by their O-markings.

The reductions modulo the variables #

source
@[simp]
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXCenterProjection_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (c : GridChain R (n + 1)) (x : GridState n) :
((G.stabilizeXCenterProjection s R).constantCoeffReduction c) x = c (x.insertPoint s.succ (G.X.toPerm s).succ)

Setting the variables to zero leaves the center projection as coefficient restriction.

source
@[simp]
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXOffCenterProjection_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (c : GridChain R (n + 1)) (y : G.StabilizeXOffCenterState s) :
((G.stabilizeXOffCenterProjection s R).constantCoeffReduction c) y = c ↑y

Setting the variables to zero leaves the off-center projection as coefficient restriction.

source
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXCenterDifferential_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (x y : GridState n) (c : R) :
((G.stabilizeXCenterDifferential s R).constantCoeffReduction (Finsupp.single x c)) y = c * ↑(G.fullyBlockedRectangles x y).card

The reduction of the center differential modulo the variables counts the fully blocked rectangles of G: over ZMod 2 it is the fully blocked differential of G.

source
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXOffCenterDifferential_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y z : G.StabilizeXOffCenterState s) (c : R) :
((G.stabilizeXOffCenterDifferential s R).constantCoeffReduction (Finsupp.single y c)) z = c * ↑((G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).fullyBlockedRectangles ↑y ↑z).card

The reduction of the off-center differential modulo the variables counts the fully blocked rectangles of the stabilization between off-center states.

source
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXOffCenterToCenter_single_apply {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] (y : G.StabilizeXOffCenterState s) (x : GridState n) (c : R) :
((G.stabilizeXOffCenterToCenter s R).constantCoeffReduction (Finsupp.single y c)) x = c * ↑{r ∈ (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).XHomotopyRectangles s.succ (↑y) (x.insertPoint s.succ (G.X.toPerm s).succ) | (G.stabilizeX s.castSucc (G.X.toPerm s).castSucc s).OColumns r.toGridRectangle = ∅}.card

The reduction of H_I^N modulo the variables counts the empty rectangles of the stabilization from an off-center state to a center state that carry no O-marking and whose only X-marking is the southeast X-marking X₂ of the new block.

source
@[simp]
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXCenterDifferential_eq_fullyBlockedDifferential {n : ℕ} (G : GridDiagram n) (s : Fin n) :
(G.stabilizeXCenterDifferential s (ZMod 2)).constantCoeffReduction = G.fullyBlockedDifferential

Over ZMod 2, the reduced center differential is the fully blocked differential of G.

source
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXCenterDifferential_comp_self {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] [CharP R 2] :
(G.stabilizeXCenterDifferential s R).constantCoeffReduction ∘ₗ (G.stabilizeXCenterDifferential s R).constantCoeffReduction = 0

The reduction of the center differential squares to zero.

source
theorem TauCeti.GridDiagram.constantCoeffReduction_stabilizeXOffCenterDifferential_comp_self {n : ℕ} (G : GridDiagram n) (s : Fin n) (R : Type u_1) [CommSemiring R] [CharP R 2] :
(G.stabilizeXOffCenterDifferential s R).constantCoeffReduction ∘ₗ (G.stabilizeXOffCenterDifferential s R).constantCoeffReduction = 0

The reduction of the off-center differential squares to zero.

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

The reduction of H_I^N is a chain map between the reductions of the two differentials.

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

H_I^N is a quasi-isomorphism if its reduced comparison is. If 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, the R-linear fully blocked rectangle-count homology of G (the library's fully blocked homology when R = ZMod 2), then H_I^N is a quasi-isomorphism of complexes over R[V₀, …, V_n].