The invariant τ of a knot grid diagram

For a knot grid G over a commutative ring K of characteristic two, the unblocked grid homology GH⁻(G) is a K[U]-module graded by the Alexander grading, on which U lowers the degree by one. Its invariant τ(G) is minus the largest Alexander degree of a homogeneous element that is not K[U]-torsion (GridDiagram.IsKnot.tau). This is the definition of the concordance invariant τ of Ozsváth--Stipsicz--Szabó, read on a single grid diagram. Its independence of the diagram presenting a knot follows from the invariance of GH⁻ under grid moves (GridDiagram.IsKnot.unblockedHomologyIsomorphic_of_movesTo), which is not part of this file.

The definition is through InternalGrading.supNonTorsionDegree, the supremum of the non-torsion degrees. When GH⁻(G) is not a torsion module that supremum is attained (GridDiagram.IsKnot.isGreatest_nonTorsionDegrees_neg_tau), so -τ(G) is the Alexander degree of a homogeneous non-torsion class and every such class has degree at most -τ(G) (GridDiagram.IsKnot.le_neg_tau). If GH⁻(G) were torsion the supremum would be that of the empty set, which Mathlib takes to be 0 (GridDiagram.IsKnot.tau_eq_zero_of_isTorsion).

Two transfer principles are recorded, which are the algebraic content of the inequalities satisfied by τ under chain maps between grid complexes. Knot grids whose homologies are isomorphic as Alexander-graded K[U]-modules have the same invariant (GridDiagram.IsKnot.UnblockedHomologyIsomorphic.tau_eq); this is how the invariance of GH⁻ descends to τ. A homogeneous K[U]-linear map of Alexander degree δ from GH⁻(G) to GH⁻(G') with a left inverse up to multiplication by a power of U satisfies τ(G') ≤ τ(G) - δ, provided GH⁻(G) is not torsion (GridDiagram.IsKnot.tau_le_tau_sub_of_comp_eq_X_pow_smul); the crossing change maps of Ozsváth--Stipsicz--Szabó, Chapter 6, supply such pairs of maps in degrees 0 and -1, and the resulting two inequalities bound the change of τ under a crossing change.

Finally, over a field, when the X-marking state G.X receives an even number of counted rectangles from every grid state and has the largest Alexander grading of any grid state, τ(G) = -A(G.X) (GridDiagram.IsKnot.tau_eq_neg_alexanderℤ_X). The standard torus knot grids satisfy both hypotheses; their values of τ are in TorusLink/Tau.lean.

Main definitions

• TauCeti.GridDiagram.IsKnot.tau: minus the maximal Alexander degree of a homogeneous non-torsion element of GH⁻(G).

Main results

• TauCeti.GridDiagram.IsKnot.isGreatest_nonTorsionDegrees_neg_tau and TauCeti.GridDiagram.IsKnot.le_neg_tau: -τ(G) is the greatest non-torsion Alexander degree when GH⁻(G) is not torsion, and an upper bound for the non-torsion degrees without that hypothesis.
• TauCeti.GridDiagram.IsKnot.tau_eq_zero_of_isTorsion: τ(G) = 0 when GH⁻(G) is torsion.
• TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic.tau_eq: isomorphic Alexander-graded unblocked homologies have the same invariant.
• TauCeti.GridDiagram.IsKnot.tau_le_tau_sub_of_comp_eq_X_pow_smul: a homogeneous map of degree δ out of a non-torsion GH⁻(G) with a left inverse up to a power of U gives τ(G') ≤ τ(G) - δ.
• TauCeti.GridDiagram.IsKnot.tau_eq_neg_alexanderℤ_X: τ(G) from the X-marking state when that state is a parity-protected cycle of maximal Alexander grading.

References

• P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, AMS Mathematical Surveys and Monographs 208, 2015, Chapter 6, for the definition of τ as minus the maximal Alexander grading of a homogeneous non-torsion element of GH⁻, and for the crossing change maps whose composites are multiplication by U.

noncomputable def TauCeti.GridDiagram.IsKnot.tau {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [CommRing K] [CharP K 2] : ℤ

The invariant τ of a knot grid diagram: minus the largest Alexander degree of a homogeneous element of the unblocked grid homology GH⁻(G) that is not K[U]-torsion.

The supremum is attained as soon as GH⁻(G) is not a torsion module (isGreatest_nonTorsionDegrees_neg_tau); if GH⁻(G) is torsion the value is 0, the supremum of the empty set. It is an invariant of the presented knot: knot grids connected by grid moves have the same τ (tau_eq_of_movesTo, in Homology/Invariance.lean). This is the grid definition of the concordance invariant τ of Ozsváth--Stipsicz--Szabó.

theorem TauCeti.GridDiagram.IsKnot.tau_def {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [CommRing K] [CharP K 2] : hG.tau K = -(hG.alexanderUnblockedHomologyGrading K).supNonTorsionDegree

τ(G) is minus the supremal non-torsion Alexander degree of GH⁻(G).

theorem TauCeti.GridDiagram.IsKnot.tau_eq_zero_of_isTorsion {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [CommRing K] [CharP K 2] : Module.IsTorsion (Polynomial K) ↑(G.unblockedHomology K) → hG.tau K = 0

If GH⁻(G) is a torsion K[U]-module, then τ(G) = 0: there is no homogeneous non-torsion class, and the supremum of the empty set of degrees is 0.

theorem TauCeti.GridDiagram.IsKnot.UnblockedHomologyIsomorphic.tau_eq {n : ℕ} {G : GridDiagram n} {hG : G.IsKnot} {K : Type u_1} [CommRing K] [CharP K 2] {m : ℕ} {G' : GridDiagram m} {hG' : G'.IsKnot} (h : hG.UnblockedHomologyIsomorphic hG' K) : hG.tau K = hG'.tau K

Knot grids whose unblocked homologies are isomorphic as Alexander-graded K[U]-modules have the same invariant τ.

theorem TauCeti.GridDiagram.IsKnot.tau_le_tau_sub_of_comp_eq_X_pow_smul {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [CommRing K] [CharP K 2] {m : ℕ} {G' : GridDiagram m} (hG' : G'.IsKnot) {δ : ℤ} (k : ℕ) (f : ↑(G.unblockedHomology K) →ₗ[Polynomial K] ↑(G'.unblockedHomology K)) (g : ↑(G'.unblockedHomology K) →ₗ[Polynomial K] ↑(G.unblockedHomology K)) : LinearMap.IsHomogeneous f ((hG.alexanderUnblockedHomologyGrading K).piece ℤ) ((hG'.alexanderUnblockedHomologyGrading K).piece ℤ) δ → (∀ (y : ↑(G.unblockedHomology K)), g (f y) = Polynomial.X ^ k • y) → ¬Module.IsTorsion (Polynomial K) ↑(G.unblockedHomology K) → hG'.tau K ≤ hG.tau K - δ

Comparison of τ along a map with a left inverse up to a power of U. Let f be a K[U]-linear map from GH⁻(G) to GH⁻(G'), homogeneous of Alexander degree δ, and let g be a K[U]-linear map back with g ∘ f = U ^ k. If GH⁻(G) is not torsion, then τ(G') ≤ τ(G) - δ: the image of a homogeneous non-torsion class of degree -τ(G) is a homogeneous non-torsion class of degree -τ(G) + δ.

theorem TauCeti.GridDiagram.IsKnot.le_neg_tau {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [CommRing K] [CharP K 2] {a : ℤ} : a ∈ (hG.alexanderUnblockedHomologyGrading K).nonTorsionDegrees → a ≤ -hG.tau K

Every Alexander degree of a homogeneous non-torsion class of GH⁻(G) is at most -τ(G).

theorem TauCeti.GridDiagram.IsKnot.isGreatest_nonTorsionDegrees_neg_tau {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [CommRing K] [CharP K 2] : ¬Module.IsTorsion (Polynomial K) ↑(G.unblockedHomology K) → IsGreatest (hG.alexanderUnblockedHomologyGrading K).nonTorsionDegrees (-hG.tau K)

When GH⁻(G) is not a torsion K[U]-module, -τ(G) is the greatest Alexander degree of a homogeneous non-torsion class: there is such a class in degree -τ(G), and none in any higher degree.

theorem TauCeti.GridDiagram.IsKnot.tau_eq_neg_alexanderℤ_X {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (K : Type u_1) [Field K] [CharP K 2] (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.tau K = -hG.toOddComponentGridDiagram.alexanderℤ G.X

τ from the X-marking state. Over a field, if every grid state has an even number of counted rectangles into the X-marking state G.X, and G.X has the largest Alexander grading of any grid state, then τ(G) = -A(G.X).