Parity of the gradings, and integrality of the Alexander grading

The Maslov gradings of a grid diagram are integers, and the Alexander grading A = (M_O - M_X) / 2 - (n - 1) / 2 is a priori only a half-integer. This file computes the parity of both Maslov gradings and settles the parity-sensitive question: A is an integer exactly when the diagram presents an odd number of link components, in particular whenever it presents a knot.

The mechanism is that (-1)^{M_O(x)} is, up to a factor depending only on the diagram, the sign of the permutation underlying the grid state x. Writing 𝕆 for the O-marking state,

M_O(x) = I(x, x) - JNumCenter(x, 𝕆) + I(𝕆, 𝕆) + 1,

the two self-pairings are the non-inversion counts of x and of 𝕆, while the mixed term has the parity of the grid size. Fibring the mixed count over the columns of x, the fibre over c contributes n - x(c) + c up to an even correction. The sums ∑ x(c) and ∑ c agree because x is a permutation, so the whole count is n² up to an even correction.

Consequently (-1)^{M_O(x) - M_X(x)} is independent of x: it is the product of the signs of the two marking permutations, hence the sign of the component permutation 𝕏⁻¹ ∘ 𝕆, and equals (-1)^{n + ℓ} for ℓ link components. The normalization shift n - 1 leaves 2 A(x) ≡ ℓ - 1 (mod 2).

Main definitions

• TauCeti.OddComponentGridDiagram: a grid diagram with an odd number of link components.
• TauCeti.GridDiagram.IsKnot.toOddComponentGridDiagram: a knot grid has one, hence an odd number of components.
• TauCeti.OddComponentGridDiagram.relabelRows, TauCeti.OddComponentGridDiagram.relabelColumns: relabeling keeps the number of link components odd.
• TauCeti.OddComponentGridDiagram.alexanderℤ: the integer Alexander grading.
• TauCeti.OddComponentGridDiagram.bidegree: the (O-Maslov, Alexander) degree of a grid state.
• TauCeti.OddComponentGridDiagram.alexanderSupport: the Alexander degrees occupied by grid states.
• TauCeti.OddComponentGridDiagram.maslovSupport: the Maslov degrees occupied in a fixed Alexander degree.

Main results

• TauCeti.GridState.even_JNumCenter_pointSet_add: the marking-pairing numerator of two grid states has the parity of the grid size.
• TauCeti.GridDiagram.negOnePow_maslovOℤ, TauCeti.GridDiagram.negOnePow_maslovXℤ: the parity of a Maslov grading is the sign of the state times the sign of the marking permutation, corrected by the grid-size factor ((n : ℤ) + 1).negOnePow.
• TauCeti.GridDiagram.negOnePow_alexanderTwoℤ: twice the Alexander grading has the parity of the number of link components minus one.
• TauCeti.GridDiagram.even_alexanderTwoℤ_iff: the Alexander grading is an integer exactly when the number of link components is odd.
• TauCeti.GridDiagram.alexander_exists_int_iff: the direct integrality characterization.
• TauCeti.GridDiagram.alexander_exists_int_of_isKnot: the Alexander grading of a knot grid is an integer.

References

Integrality of A on a knot diagram, and the half-integer shift for an even number of components, are from Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.3. The Lean proof is adapted from Tau Ceti split-branch commit 05c2722248.

theorem TauCeti.GridState.even_JNumCenter_pointSet_add {n : ℕ} (x y : GridState n) : Even (↑(GridPoint.JNumCenter x.pointSet y.pointSet) + ↑n)

The marking-pairing numerator of two grid states has the parity of the grid size.

theorem TauCeti.GridDiagram.negOnePow_maslovOℤ {n : ℕ} (G : GridDiagram n) (x : GridState n) : (G.maslovOℤ x).negOnePow = Equiv.Perm.sign x.toPerm * Equiv.Perm.sign G.O.toPerm * (↑n + 1).negOnePow

The parity of the O-Maslov grading is the sign of the state permutation, corrected by the sign of the O-marking permutation and by the grid size.

theorem TauCeti.GridDiagram.negOnePow_maslovXℤ {n : ℕ} (G : GridDiagram n) (x : GridState n) : (G.maslovXℤ x).negOnePow = Equiv.Perm.sign x.toPerm * Equiv.Perm.sign G.X.toPerm * (↑n + 1).negOnePow

The parity of the X-Maslov grading is the analogous expression using the X markings.

theorem TauCeti.GridDiagram.sign_O_mul_sign_X {n : ℕ} (G : GridDiagram n) : Equiv.Perm.sign G.O.toPerm * Equiv.Perm.sign G.X.toPerm = (↑n + ↑G.componentCount).negOnePow

The signs of the marking permutations multiply to the sign of the component permutation, which is (-1) to the grid size plus the number of link components.

theorem TauCeti.GridDiagram.negOnePow_alexanderTwoℤ {n : ℕ} (G : GridDiagram n) (x : GridState n) : (G.alexanderTwoℤ x).negOnePow = (↑G.componentCount + 1).negOnePow

Twice the Alexander grading has the parity of the number of link components minus one.

theorem TauCeti.GridDiagram.even_alexanderTwoℤ_iff {n : ℕ} (G : GridDiagram n) (x : GridState n) : Even (G.alexanderTwoℤ x) ↔ Odd G.componentCount

The Alexander grading is integral exactly when the diagram has an odd number of components.

theorem TauCeti.GridDiagram.alexander_exists_int_iff {n : ℕ} (G : GridDiagram n) (x : GridState n) : (∃ (a : ℤ), G.alexander x = ↑a) ↔ Odd G.componentCount

The Alexander grading of a state is an integer exactly when the diagram has an odd number of link components. For an even number of components, every Alexander grading is a strict half-integer.

theorem TauCeti.GridDiagram.even_alexanderTwoℤ_sub {n : ℕ} (G : GridDiagram n) (x y : GridState n) : Even (G.alexanderTwoℤ x - G.alexanderTwoℤ y)

Twice the Alexander gradings of two states differ by an even integer.

theorem TauCeti.GridDiagram.even_alexanderTwoℤ_of_isKnot {n : ℕ} (G : GridDiagram n) (hG : G.IsKnot) (x : GridState n) : Even (G.alexanderTwoℤ x)

Twice the Alexander grading of a state in a knot grid is even.

theorem TauCeti.GridDiagram.alexander_exists_int_of_isKnot {n : ℕ} (G : GridDiagram n) (hG : G.IsKnot) (x : GridState n) : ∃ (a : ℤ), G.alexander x = ↑a

The Alexander grading of a knot grid diagram is an integer.

@[reducible, inline]

abbrev TauCeti.OddComponentGridDiagram (n : ℕ) : Type

A grid diagram with an odd number of link components.

@[reducible, inline]

abbrev TauCeti.GridDiagram.IsKnot.toOddComponentGridDiagram {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) : OddComponentGridDiagram n

A knot grid, viewed as a grid with an odd number of components.

def TauCeti.OddComponentGridDiagram.relabelRows {n : ℕ} (G : OddComponentGridDiagram n) (ρ : Equiv.Perm (Fin n)) : OddComponentGridDiagram n

Relabeling the rows of a grid diagram with an odd number of components.

@[simp]

theorem TauCeti.OddComponentGridDiagram.val_relabelRows {n : ℕ} (G : OddComponentGridDiagram n) (ρ : Equiv.Perm (Fin n)) : ↑(G.relabelRows ρ) = GridDiagram.relabelRows ρ ↑G

The underlying grid diagram of G.relabelRows ρ is the row-relabeled diagram.

def TauCeti.OddComponentGridDiagram.relabelColumns {n : ℕ} (G : OddComponentGridDiagram n) (κ : Equiv.Perm (Fin n)) : OddComponentGridDiagram n

Relabeling the columns of a grid diagram with an odd number of components.

@[simp]

theorem TauCeti.OddComponentGridDiagram.val_relabelColumns {n : ℕ} (G : OddComponentGridDiagram n) (κ : Equiv.Perm (Fin n)) : ↑(G.relabelColumns κ) = GridDiagram.relabelColumns κ ↑G

The underlying grid diagram of G.relabelColumns κ is the column-relabeled diagram.

@[reducible, inline]

abbrev TauCeti.OddComponentGridDiagram.rotate {n : ℕ} (G : OddComponentGridDiagram n) : OddComponentGridDiagram n

The half-turn of the marking squares of a diagram with an odd number of components.

@[simp]

theorem TauCeti.OddComponentGridDiagram.val_rotate {n : ℕ} (G : OddComponentGridDiagram n) : ↑G.rotate = (↑G).rotate

The underlying diagram of the half-turn is the half-turned underlying diagram.

@[simp]

theorem TauCeti.OddComponentGridDiagram.rotate_rotate {n : ℕ} (G : OddComponentGridDiagram n) : G.rotate.rotate = G

The half-turn is an involution on diagrams with an odd number of components.

@[reducible, inline]

abbrev TauCeti.OddComponentGridDiagram.transpose {n : ℕ} (G : OddComponentGridDiagram n) : OddComponentGridDiagram n

The diagonal reflection of a diagram with an odd number of components.

@[simp]

theorem TauCeti.OddComponentGridDiagram.val_transpose {n : ℕ} (G : OddComponentGridDiagram n) : ↑G.transpose = (↑G).transpose

The underlying diagram of the diagonal reflection is the reflected underlying diagram.

@[simp]

theorem TauCeti.OddComponentGridDiagram.transpose_transpose {n : ℕ} (G : OddComponentGridDiagram n) : G.transpose.transpose = G

The diagonal reflection is an involution on diagrams with an odd number of components.

def TauCeti.OddComponentGridDiagram.alexanderℤ {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : ℤ

The integer Alexander grading of a grid state.

theorem TauCeti.OddComponentGridDiagram.two_mul_alexanderℤ {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : 2 * G.alexanderℤ x = (↑G).alexanderTwoℤ x

The integer Alexander grading is half of its numerator.

@[simp]

theorem TauCeti.OddComponentGridDiagram.alexanderℤ_transpose {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : G.transpose.alexanderℤ x.transpose = G.alexanderℤ x

The diagonal reflection of a diagram and a grid state preserves the integer Alexander grading.

theorem TauCeti.OddComponentGridDiagram.alexander_eq_intCast {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : (↑G).alexander x = ↑(G.alexanderℤ x)

The integer Alexander grading agrees with the original rational-valued Alexander grading.

def TauCeti.OddComponentGridDiagram.bidegree {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : ℤ × ℤ

The (O-Maslov, Alexander) bidegree of a grid state.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bidegree_fst {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : (G.bidegree x).1 = (↑G).maslovOℤ x

The first component of the grid bidegree is the integer O-Maslov grading.

@[simp]

theorem TauCeti.OddComponentGridDiagram.bidegree_snd {n : ℕ} (G : OddComponentGridDiagram n) (x : GridState n) : (G.bidegree x).2 = G.alexanderℤ x

The second component of the grid bidegree is the integer Alexander grading.

noncomputable def TauCeti.OddComponentGridDiagram.bidegreeSupport {n : ℕ} (G : OddComponentGridDiagram n) : Finset (ℤ × ℤ)

The finite set of bidegrees occupied by grid states.

@[simp]

theorem TauCeti.OddComponentGridDiagram.mem_bidegreeSupport_iff {n : ℕ} (G : OddComponentGridDiagram n) (g : ℤ × ℤ) : g ∈ G.bidegreeSupport ↔ ∃ (x : GridState n), G.bidegree x = g

A bidegree is occupied exactly when some grid state has that bidegree.

noncomputable def TauCeti.OddComponentGridDiagram.alexanderSupport {n : ℕ} (G : OddComponentGridDiagram n) : Finset ℤ

The Alexander degrees occupied by the grid states of a diagram.

@[simp]

theorem TauCeti.OddComponentGridDiagram.mem_alexanderSupport_iff {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : a ∈ G.alexanderSupport ↔ ∃ (x : GridState n), G.alexanderℤ x = a

An Alexander degree is occupied exactly when some grid state has it.

noncomputable def TauCeti.OddComponentGridDiagram.maslovSupport {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : Finset ℤ

The O-Maslov degrees occupied by the grid states of a fixed Alexander degree.

@[simp]

theorem TauCeti.OddComponentGridDiagram.mem_maslovSupport_iff {n : ℕ} (G : OddComponentGridDiagram n) (a m : ℤ) : m ∈ G.maslovSupport a ↔ ∃ (x : GridState n), G.bidegree x = (m, a)

A Maslov degree is occupied in Alexander degree a exactly when some grid state has bidegree (m, a).