Non-torsion classes in unblocked grid homology from rectangle parity

The X-marking state G.X of a grid diagram, the grid state whose point in each column is the lower-left corner of the X-marked square, is a cycle of the unblocked grid complex GC⁻ (GridDiagram.unblockedDifferential_single_X). This file studies when its class XMarkingClass in GH⁻ is not torsion.

The tool is the evaluation of the coefficient ring R[V₀, …, V_{n-1}] at V₀ = ⋯ = V_{n-1} = 1. It sends the weight V^{O(r)} of every rectangle to 1, hence sends each matrix coefficient of ∂⁻ to the number of rectangles it counts (eval_one_unblockedCoefficient). If every grid state has an even number of counted rectangles ending at a state z, then in characteristic two the z-coefficient of every boundary evaluates to zero (eval_one_unblockedDifferential_apply_eq_zero), so p • z is a boundary only when p(1, …, 1) = 0 (eval_one_eq_zero_of_smul_single_mem_range), and no monomial multiple of z is a boundary. Applied to z = G.X, no power of U kills XMarkingClass (X_pow_smul_XMarkingClass_ne_zero).

For a knot grid the class is homogeneous of Alexander degree A(G.X) (IsKnot.XMarkingClass_mem_alexanderUnblockedHomologyGrading_piece), so over a field of characteristic two the parity hypothesis makes A(G.X) a non-torsion degree of the R[U]-module GH⁻ (IsKnot.alexanderℤ_X_mem_nonTorsionDegrees); in particular GH⁻ is not a torsion module. A degree bound on the grid states bounds the non-torsion degrees (IsKnot.nonTorsionDegrees_subset_Iic), so when G.X has the largest Alexander grading among the grid states, A(G.X) is the maximal non-torsion degree (IsKnot.supNonTorsionDegree_alexanderUnblockedHomologyGrading_eq). The standard torus knot grids satisfy both hypotheses; they are treated in TorusLink/Homology.lean.

Main definitions

• TauCeti.GridDiagram.XMarkingCycle: the X-marking state as a cycle of GC⁻.
• TauCeti.GridDiagram.XMarkingClass: its class in GH⁻.

Main results

• TauCeti.GridDiagram.eval_one_eq_zero_of_smul_single_mem_range: if every state has an even number of counted rectangles into z, a multiple p • z is a boundary only when p(1, …, 1) = 0.
• TauCeti.GridDiagram.X_pow_smul_XMarkingClass_ne_zero and TauCeti.GridDiagram.IsKnot.X_pow_smul_XMarkingClass_ne_zero: under that parity hypothesis at G.X, no power of a grid variable, or of U on a knot grid, kills XMarkingClass.
• TauCeti.GridDiagram.IsKnot.alexanderℤ_X_mem_nonTorsionDegrees and TauCeti.GridDiagram.IsKnot.supNonTorsionDegree_alexanderUnblockedHomologyGrading_eq: the Alexander grading of G.X is a non-torsion degree, and the maximal one when G.X has maximal Alexander grading among the grid states.

References

The class of the X-marking state is the canonical generator used by Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 6, to compute τ of torus knots; the argument through the evaluation at 1 is the observation that torsion in GH⁻ is invisible to the count of X-avoiding rectangles.

Evaluating the grid variables at one

@[simp]

theorem TauCeti.GridDiagram.eval_one_OMonomial {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (r : GridRectangle n) : (MvPolynomial.eval fun (x : Fin n) => 1) (G.OMonomial R r) = 1

Setting every grid variable to 1 sends the weight of a rectangle to 1.

@[simp]

theorem TauCeti.GridDiagram.eval_one_unblockedCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (x y : GridState n) : (MvPolynomial.eval fun (x : Fin n) => 1) (G.unblockedCoefficient R x y) = ↑(G.unblockedRectangles x y).card

Setting every grid variable to 1 sends a matrix coefficient of ∂⁻ to the number of rectangles it counts.

theorem TauCeti.GridDiagram.eval_one_unblockedDifferential_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (c : GridChainMinus R n) (z : GridState n) : (MvPolynomial.eval fun (x : Fin n) => 1) (((G.unblockedDifferential R) c) z) = Finsupp.sum c fun (x : GridState n) (a : MvPolynomial (Fin n) R) => (MvPolynomial.eval fun (x : Fin n) => 1) a * ↑(G.unblockedRectangles x z).card

Setting every grid variable to 1 in the z-coefficient of ∂⁻ c gives the sum, over the support of c, of the evaluated coefficients weighted by the numbers of counted rectangles.

theorem TauCeti.GridDiagram.eval_one_unblockedDifferential_apply_eq_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] {z : GridState n} (hz : ∀ (x : GridState n), Even (G.unblockedRectangles x z).card) (c : GridChainMinus R n) : (MvPolynomial.eval fun (x : Fin n) => 1) (((G.unblockedDifferential R) c) z) = 0

If every grid state has an even number of counted rectangles into z, then in characteristic two the z-coefficient of every boundary vanishes once the grid variables are set to 1.

theorem TauCeti.GridDiagram.eval_one_eq_zero_of_smul_single_mem_range {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] {z : GridState n} (hz : ∀ (x : GridState n), Even (G.unblockedRectangles x z).card) {p : MvPolynomial (Fin n) R} (hp : p • Finsupp.single z 1 ∈ (G.unblockedDifferential R).range) : (MvPolynomial.eval fun (x : Fin n) => 1) p = 0

If every grid state has an even number of counted rectangles into z, then a multiple p • z of the generator z is a boundary only when p(1, …, 1) = 0.

theorem TauCeti.GridDiagram.monomial_smul_single_notMem_range {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] {z : GridState n} (hz : ∀ (x : GridState n), Even (G.unblockedRectangles x z).card) (e : Fin n →₀ ℕ) : (MvPolynomial.monomial e) 1 • Finsupp.single z 1 ∉ (G.unblockedDifferential R).range

If every grid state has an even number of counted rectangles into z, then no monomial multiple of the generator z is a boundary.

The X-marking state as a cycle

noncomputable def TauCeti.GridDiagram.XMarkingCycle {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] : ↥(G.unblockedDifferential R).ker

The X-marking state, as a cycle of the unblocked grid complex GC⁻.

@[simp]

theorem TauCeti.GridDiagram.coe_XMarkingCycle {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] : ↑(G.XMarkingCycle R) = Finsupp.single G.X 1

The cycle XMarkingCycle is the generator of GC⁻ at the X-marking state.

noncomputable def TauCeti.GridDiagram.XMarkingClass {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : ↑(G.unblockedHomology R)

The class of the X-marking state in the unblocked grid homology GH⁻.

theorem TauCeti.GridDiagram.XMarkingClass_def {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : G.XMarkingClass R = (G.unblockedHomologyClass R) (G.XMarkingCycle R)

The class of the X-marking state is the class of its cycle.

theorem TauCeti.GridDiagram.monomial_smul_XMarkingClass_ne_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (hX : ∀ (x : GridState n), Even (G.unblockedRectangles x G.X).card) (e : Fin n →₀ ℕ) : (MvPolynomial.monomial e) 1 • G.XMarkingClass R ≠ 0

If every grid state has an even number of counted rectangles into the X-marking state, then no monomial in the grid variables kills its class in GH⁻.

theorem TauCeti.GridDiagram.X_pow_smul_XMarkingClass_ne_zero {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (hX : ∀ (x : GridState n), Even (G.unblockedRectangles x G.X).card) (i : Fin n) (k : ℕ) : MvPolynomial.X i ^ k • G.XMarkingClass R ≠ 0

If every grid state has an even number of counted rectangles into the X-marking state, then no power of a grid variable kills its class in GH⁻.

Knot grids

theorem TauCeti.GridDiagram.IsKnot.X_pow_smul_XMarkingClass_ne_zero {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) (hX : ∀ (x : GridState n), Even (G.unblockedRectangles x G.X).card) (k : ℕ) : Polynomial.X ^ k • G.XMarkingClass R ≠ 0

On a knot grid whose X-marking state receives an even number of counted rectangles from every grid state, no power of U kills the class of the X-marking state in GH⁻.

theorem TauCeti.GridDiagram.IsKnot.XMarkingClass_mem_alexanderUnblockedHomologyGrading_piece {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) : G.XMarkingClass R ∈ (hG.alexanderUnblockedHomologyGrading R).piece ℤ (hG.toOddComponentGridDiagram.alexanderℤ G.X)

On a knot grid the class of the X-marking state is homogeneous of Alexander degree A(G.X).

theorem TauCeti.GridDiagram.IsKnot.le_of_mem_alexanderChainMinusPiece_of_ne_zero {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] (hG : G.IsKnot) {a₀ : ℤ} (h : ∀ (x : GridState n), hG.toOddComponentGridDiagram.alexanderℤ x ≤ a₀) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ hG.toOddComponentGridDiagram.alexanderChainMinusPiece R a) (hc0 : c ≠ 0) : a ≤ a₀

A homogeneous nonzero chain of GC⁻ has Alexander degree at most the Alexander grading of some grid state, so at most any common upper bound of the Alexander gradings of the grid states.

theorem TauCeti.GridDiagram.IsKnot.nonTorsionDegrees_subset_Iic {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) {a₀ : ℤ} (h : ∀ (x : GridState n), hG.toOddComponentGridDiagram.alexanderℤ x ≤ a₀) : (hG.alexanderUnblockedHomologyGrading R).nonTorsionDegrees ⊆ Set.Iic a₀

On a knot grid, an upper bound for the Alexander gradings of the grid states bounds the non-torsion degrees of GH⁻.

theorem TauCeti.GridDiagram.IsKnot.bddAbove_nonTorsionDegrees_alexanderUnblockedHomologyGrading {n : ℕ} {G : GridDiagram n} (R : Type u_1) [CommRing R] [CharP R 2] (hG : G.IsKnot) : BddAbove (hG.alexanderUnblockedHomologyGrading R).nonTorsionDegrees

The Alexander degrees containing a non-torsion class of GH⁻ are bounded above.

theorem TauCeti.GridDiagram.IsKnot.alexanderℤ_X_mem_nonTorsionDegrees {n : ℕ} {K : Type u_1} [Field K] [CharP K 2] {G : GridDiagram n} (hG : G.IsKnot) (hX : ∀ (x : GridState n), Even (G.unblockedRectangles x G.X).card) : hG.toOddComponentGridDiagram.alexanderℤ G.X ∈ (hG.alexanderUnblockedHomologyGrading K).nonTorsionDegrees

On a knot grid whose X-marking state receives an even number of counted rectangles from every grid state, the Alexander grading of the X-marking state is a non-torsion degree of the K[U]-module GH⁻: the class of that state is homogeneous and not torsion.

theorem TauCeti.GridDiagram.IsKnot.not_isTorsion_unblockedHomology {n : ℕ} {K : Type u_1} [Field K] [CharP K 2] {G : GridDiagram n} (hG : G.IsKnot) (hX : ∀ (x : GridState n), Even (G.unblockedRectangles x G.X).card) : ¬Module.IsTorsion (Polynomial K) ↑(G.unblockedHomology K)

On a knot grid whose X-marking state receives an even number of counted rectangles from every grid state, GH⁻ is not a torsion K[U]-module.

theorem TauCeti.GridDiagram.IsKnot.supNonTorsionDegree_alexanderUnblockedHomologyGrading_eq {n : ℕ} {K : Type u_1} [Field K] [CharP K 2] {G : GridDiagram n} (hG : G.IsKnot) (hX : ∀ (x : GridState n), Even (G.unblockedRectangles x G.X).card) (h : ∀ (x : GridState n), hG.toOddComponentGridDiagram.alexanderℤ x ≤ hG.toOddComponentGridDiagram.alexanderℤ G.X) : (hG.alexanderUnblockedHomologyGrading K).supNonTorsionDegree = hG.toOddComponentGridDiagram.alexanderℤ G.X

On a knot grid whose X-marking state receives an even number of counted rectangles from every grid state and has the largest Alexander grading among the grid states, that grading is the maximal non-torsion degree of the K[U]-module GH⁻.