Documentation

TauCeti.KnotTheory.Grid.Gradings

Maslov and Alexander gradings for grid states #

This file records the rational-valued grading formulas for the grid-combinatorial lane of the Heegaard Floer roadmap. The point-set J-function of a pair of grid states and the pairing of a grid state against a set of marked squares were developed separately; here we use them to define the O- and X-Maslov gradings and the Alexander grading of a grid state.

The O-Maslov grading is M_O(x) = J(x, x) - 2 J_O(x) + J(𝕆, 𝕆) + 1, and the X-Maslov grading is defined analogously. The middle term compares grid points against markings, so it uses the asymmetric marking pairing GridDiagram.JO or GridDiagram.JX from JFunction/Center.lean, which accounts for the markings sitting at the centres of their squares. The two outer terms compare like with like and use the ordinary J-pairing.

The definitions are intentionally formula-level. The later integer-valuedness and rectangle-change theorems can refer to these names without unfolding the point-pair count.

Main definitions #

Main results #

References #

This supplies the grading-definition part of TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.2, "Gradings. The J-function, M_O, M_X, A; integer-valuedness of A; grading-change formulas across a rectangle." The grading conventions follow OzsvΓ‘th--Stipsicz--SzabΓ³, Grid Homology for Knots and Links, Chapters 3.1--3.2 and 4.1 for the placement convention, and Chapter 4.3 for the bigrading. In particular, A(x) = (M_O(x) - M_X(x)) / 2 - (n - 1) / 2.

source
def TauCeti.GridDiagram.maslovO {n : β„•} (G : GridDiagram n) (x : GridState n) :
β„š

The O-Maslov grading of a grid state: the state and marking self-pairings, minus twice the asymmetric pairing of the state against the O-markings, plus the normalization constant.

Instances For
    source
    @[simp]
    theorem TauCeti.GridDiagram.maslovO_def {n : β„•} (G : GridDiagram n) (x : GridState n) :
    G.maslovO x = x.J x - 2 * G.JO x + G.O.J G.O + 1

    The O-Maslov grading as its defining formula.

    source
    def TauCeti.GridDiagram.maslovX {n : β„•} (G : GridDiagram n) (x : GridState n) :
    β„š

    The X-Maslov grading of a grid state: the state and marking self-pairings, minus twice the asymmetric pairing of the state against the X-markings, plus the normalization constant.

    Instances For
      source
      @[simp]
      theorem TauCeti.GridDiagram.maslovX_def {n : β„•} (G : GridDiagram n) (x : GridState n) :
      G.maslovX x = x.J x - 2 * G.JX x + G.X.J G.X + 1

      The X-Maslov grading as its defining formula.

      source
      def TauCeti.GridDiagram.alexander {n : β„•} (G : GridDiagram n) (x : GridState n) :
      β„š

      The Alexander grading of a grid state.

      This is the formula A(x) = (M_O(x) - M_X(x)) / 2 - (n - 1) / 2. The shift is cast through β„€, so the formula remains literal at n = 0; integer-valuedness is a later grading theorem.

      Instances For
        source
        @[simp]
        theorem TauCeti.GridDiagram.alexander_def {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.alexander x = (G.maslovO x - G.maslovX x) / 2 - ↑(↑n - 1) / 2

        The Alexander grading as the difference of the two Maslov gradings with the standard normalization shift.

        source
        theorem TauCeti.GridDiagram.alexander_eq {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.alexander x = (2 * (G.JX x - G.JO x) + (G.O.J G.O - G.X.J G.X) - ↑(↑n - 1)) / 2

        The Alexander grading with the two Maslov formulas expanded.

        source
        theorem TauCeti.GridDiagram.maslovO_sub_maslovX_eq {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.maslovO x - G.maslovX x = 2 * G.alexander x + ↑(↑n - 1)

        The difference of the two Maslov gradings is twice the Alexander grading plus the normalization shift.

        source
        theorem TauCeti.GridDiagram.alexander_eq_neg_shift_of_maslov_eq {n : β„•} (G : GridDiagram n) {x : GridState n} (h : G.maslovO x = G.maslovX x) :
        G.alexander x = -↑(↑n - 1) / 2

        Replacing the two Maslov gradings by the same value leaves only the normalization shift in the Alexander formula.

        source
        theorem TauCeti.GridDiagram.maslovO_transpose {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.transpose.maslovO x.transpose = G.maslovO x

        The O-Maslov grading is invariant under the diagonal reflection.

        source
        theorem TauCeti.GridDiagram.maslovX_transpose {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.transpose.maslovX x.transpose = G.maslovX x

        The X-Maslov grading is invariant under the diagonal reflection.

        source
        theorem TauCeti.GridDiagram.alexander_transpose {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.transpose.alexander x.transpose = G.alexander x

        The Alexander grading is invariant under the diagonal reflection. The normalization shift depends only on the common grid size, so it cancels between the two diagrams.

        source
        theorem TauCeti.GridDiagram.maslovO_swapMarkings {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.swapMarkings.maslovO x = G.maslovX x

        The marking swap exchanges the two Maslov gradings: M_O of the swap is M_X.

        source
        theorem TauCeti.GridDiagram.maslovX_swapMarkings {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.swapMarkings.maslovX x = G.maslovO x

        The marking swap exchanges the two Maslov gradings: M_X of the swap is M_O.

        source
        theorem TauCeti.GridDiagram.alexander_swapMarkings {n : β„•} (G : GridDiagram n) (x : GridState n) :
        G.swapMarkings.alexander x = -G.alexander x - ↑(↑n - 1)

        The marking swap negates the Alexander grading, up to the constant normalization shift: A_swap(x) = -A(x) - (n - 1). The grading is built antisymmetrically from the two Maslov gradings, which the swap exchanges, while the shift depends only on the grid size.