Documentation

TauCeti.KnotTheory.Grid.Determinant

The grid determinant formula #

The alternating Alexander state sum of a grid diagram is

∑_{x ∈ S(G)} (-1)^{M_O(x)} T^{2 A(x)},

one term for each of the n! grid states. For odd-component diagrams, this corresponds to the graded Euler characteristic of the grid chain module after identifying T with a square root of the usual Alexander variable; that identification is TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_stateSum in Grid/EulerCharacteristic.lean. This file evaluates the state sum in closed form: it is a sign times a monomial times the determinant of an explicit n × n matrix of monomials read off the diagram. Two facts combine to produce the determinant.

The sign is the sign of a permutation. A grid state is a permutation of the columns, and GridDiagram.negOnePow_maslovOℤ says that (-1)^{M_O(x)} is that permutation's sign, up to a factor depending only on the diagram. So the alternating sum over states is an alternating sum over the symmetric group.

The Alexander grading is a sum of local weights. Twice the Alexander grading is 2 A(x) = M_O(x) - M_X(x) - (n - 1), in which the two J-self-pairings of x cancel and only the numerators of the two pairings of x against the markings survive. Each is a count of column pairs, so fibring it over the column of its grid-state entry writes it as a sum over the columns of x of a quantity GridState.JNumCenterAt depending only on the grid point occupied there. Twice the Alexander grading is therefore ∑_c w(c, x c) + K for the weight GridDiagram.alexanderTwoWeight and a constant GridDiagram.alexanderTwoShift.

Together these turn the state sum into ∑_σ sgn(σ) ∏_c T^{w(c, σ c)}, which is by definition the determinant of GridDiagram.weightMatrix, the weight matrix whose (c, r) entry is the monomial T^{w(c, r)}. That is GridDiagram.stateSum_eq_smul_T_mul_det_weightMatrix, the grid determinant formula.

The grading variable T is a square root of the Alexander variable: the exponents are values of GridDiagram.alexanderTwoℤ, which is twice the Alexander grading, because the Alexander grading itself is only a half-integer unless the diagram presents an odd number of components. Working with the doubled grading keeps every statement here free of that hypothesis; specialising to a knot grid, where 2 A(x) is even, costs nothing.

A first consequence, and a check that the formula is not vacuous: setting T = 1 makes every entry of the weight matrix equal to 1, so its determinant vanishes as soon as the grid has two columns. Hence ∑_x (-1)^{M_O(x)} = 0, that is, on any grid of size at least two exactly half of the states have even O-Maslov grading (GridDiagram.sum_negOnePow_maslovOℤ_eq_zero).

Main definitions #

Main results #

References #

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.4, "Euler characteristic = Alexander polynomial, via the grid determinant formula". The determinant formula is Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.3; identifying the determinant with the Alexander polynomial of the link the diagram presents is the remaining half of that milestone.

source
def TauCeti.GridDiagram.alexanderTwoWeight {n : ℕ} (G : GridDiagram n) (c r : Fin n) :
ℤ

The local weight of the grid point (c, r) in a grid diagram: the local X-marking-pairing numerator minus the local O-marking-pairing numerator.

Twice the Alexander grading of a grid state is the sum of these weights over the grid points the state occupies, up to the constant GridDiagram.alexanderTwoShift.

Instances For
    source
    theorem TauCeti.GridDiagram.alexanderTwoWeight_def {n : ℕ} (G : GridDiagram n) (c r : Fin n) :
    G.alexanderTwoWeight c r = ↑(G.X.JNumCenterAt c r) - ↑(G.O.JNumCenterAt c r)

    The local weight restated as its defining difference of marking-pairing numerators.

    source
    def TauCeti.GridDiagram.alexanderTwoShift {n : ℕ} (G : GridDiagram n) :
    ℤ

    The constant term in the decomposition of twice the Alexander grading: it involves only the markings of the diagram and the grid size, not the grid state.

    Instances For
      source
      theorem TauCeti.GridDiagram.alexanderTwoShift_def {n : ℕ} (G : GridDiagram n) :
      G.alexanderTwoShift = ↑(GridPoint.I G.OSet G.OSet) - ↑(GridPoint.I G.XSet G.XSet) - (↑n - 1)

      The constant term restated as its defining formula.

      source
      theorem TauCeti.GridDiagram.alexanderTwoℤ_eq_sum_alexanderTwoWeight_add_shift {n : ℕ} (G : GridDiagram n) (x : GridState n) :
      G.alexanderTwoℤ x = ∑ c : Fin n, G.alexanderTwoWeight c (x.toPerm c) + G.alexanderTwoShift

      Twice the Alexander grading of a grid state is the sum of the local weights of the grid points it occupies, plus a constant depending only on the diagram.

      The two J-self-pairings of the state cancel in 2 A = M_O - M_X - (n - 1), and each surviving marking-pairing numerator fibres over the columns.

      source
      noncomputable def TauCeti.GridDiagram.weightMatrix {n : ℕ} (G : GridDiagram n) :
      Matrix (Fin n) (Fin n) (LaurentPolynomial ℤ)

      The weight matrix of a grid diagram: the (c, r) entry is the monomial whose exponent is the local Alexander weight of the grid point in column c and row r.

      Instances For
        source
        @[simp]
        theorem TauCeti.GridDiagram.weightMatrix_apply {n : ℕ} (G : GridDiagram n) (c r : Fin n) :
        G.weightMatrix c r = LaurentPolynomial.T (G.alexanderTwoWeight c r)

        The entries of the weight matrix are the monomials of the local Alexander weights.

        source
        noncomputable def TauCeti.GridDiagram.stateSum {n : ℕ} (G : GridDiagram n) :
        LaurentPolynomial ℤ

        The alternating Alexander state sum over the n! grid states, with monomial exponents given by twice their Alexander gradings.

        The exponents are values of GridDiagram.alexanderTwoℤ, so the variable T is a square root of the usual Alexander variable. For odd-component diagrams, this state sum corresponds to the graded Euler characteristic of the grid chain module after that change of variable; this is TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_stateSum in Grid/EulerCharacteristic.lean.

        Instances For
          source
          theorem TauCeti.GridDiagram.stateSum_def {n : ℕ} (G : GridDiagram n) :
          G.stateSum = ∑ x : GridState n, (G.maslovOℤ x).negOnePow • LaurentPolynomial.T (G.alexanderTwoℤ x)

          The state sum restated as its defining alternating sum.

          source
          theorem TauCeti.GridDiagram.stateSum_eq_smul_T_mul_det_weightMatrix {n : ℕ} (G : GridDiagram n) :
          G.stateSum = (Equiv.Perm.sign G.O.toPerm * (↑n + 1).negOnePow) • (LaurentPolynomial.T G.alexanderTwoShift * G.weightMatrix.det)

          The grid determinant formula. The alternating Alexander state sum is a sign times a monomial times the determinant of the weight matrix.

          The sign and the monomial depend only on the markings and the grid size, so the determinant of GridDiagram.weightMatrix carries all of the state-sum information.

          source
          theorem TauCeti.GridDiagram.sum_negOnePow_maslovOℤ_eq_zero {n : ℕ} (G : GridDiagram n) (hn : 2 ≤ n) :
          ∑ x : GridState n, ↑(G.maslovOℤ x).negOnePow = 0

          The alternating sign sum over grid states vanishes on every grid of size at least two: exactly half of the n! grid states have even O-Maslov grading.

          This is the grid determinant formula evaluated at T = 1, where every entry of the weight matrix becomes 1 and the determinant has two equal rows.