Documentation

TauCeti.KnotTheory.Grid.JFunction.Center

Pairing grid points against markings at the centers of their squares #

The J-function of JFunction/Basic.lean compares two sets of grid points with the strict southwest relation. The Maslov and Alexander gradings, however, pair a grid state, which occupies grid points, against the O- and X-markings, which sit at the centers of squares. In the planar realization of a grid, the marking of the square named by the grid point q sits at q + (1/2, 1/2): half a unit northeast of q, and never on a grid line. So a grid point p lies southwest of that marking exactly when p ≀ q in both coordinates, whereas the marking lies southwest of p exactly when q < p in both coordinates. Only the first of the two comparisons changes: this file records the weakened one and builds the state-against-markings pairing out of it.

Writing π’₯ for the resulting pairing, the gradings are M_O(x) = J(x, x) - 2 π’₯(x, 𝕆) + J(𝕆, 𝕆) + 1 and likewise for M_X, following OzsvΓ‘th--Stipsicz--SzabΓ³. Note that π’₯ is genuinely asymmetric in its two arguments: the left argument holds grid points and the right argument names squares, so there is no analogue of GridPoint.J_comm. Marking-against-marking and state-against-state pairings need no correction, since shifting both point sets by (1/2, 1/2) preserves every strict comparison; those keep using GridPoint.J.

The grid differential reads marking indices the same way: its marking-avoidance predicate GridRectangle.AvoidsMarkings tests the squares a rectangle covers, so a marking index names a square there too.

Main definitions #

Main results #

References #

This supplies a prerequisite for CombinatorialHeegaardFloer/README.md in TauCetiRoadmap, Lane G.2, "Gradings. The J-function, M_O, M_X, A; integer-valuedness of A; grading-change formulas across a rectangle." The convention that the markings sit at the centers of their squares while a grid state sits on the grid lines is that of 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 grading pairing.

source
def TauCeti.GridPoint.ICenter {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
β„•

The ordered count of pairs (p, q) ∈ s Γ—Λ’ t with p southwest of the center of the square q. The left argument holds grid points and the right argument names marked squares; the marking of the square named by q sits at q + (1/2, 1/2), so a strict comparison against the marking is the weak comparison p ≀ q of the product order.

Instances For
    source
    theorem TauCeti.GridPoint.ICenter_eq_ICount {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
    ICenter s t = ICount (fun (x1 x2 : Fin n Γ— Fin n) => x1 ≀ x2) s t

    The southwest-of-center count is the relation-parametric ordered count at the weak product order.

    source
    theorem TauCeti.GridPoint.ICenter_singleton_left {n : β„•} (p : Fin n Γ— Fin n) (t : Finset (Fin n Γ— Fin n)) :
    ICenter {p} t = {q ∈ t | p ≀ q}.card

    The southwest-of-center count of one grid point is its weakly northeast fiber.

    source
    theorem TauCeti.GridPoint.ICenter_singleton_right {n : β„•} (s : Finset (Fin n Γ— Fin n)) (p : Fin n Γ— Fin n) :
    ICenter s {p} = {q ∈ s | q ≀ p}.card

    The southwest-of-center count against one marked square is its weakly southwest fiber.

    source
    theorem TauCeti.GridPoint.ICenter_graph_eq_card {n : β„•} (f g : Fin n β†’ Fin n) :
    ICenter (Finset.image (fun (c : Fin n) => (c, f c)) Finset.univ) (Finset.image (fun (c : Fin n) => (c, g c)) Finset.univ) = {p : Fin n Γ— Fin n | p.1 ≀ p.2 ∧ f p.1 ≀ g p.2}.card

    The southwest-of-center count of two graph point sets is the number of column pairs c ≀ d whose rows compare the same way. This graph-level statement does not require either row assignment to be a permutation.

    source
    theorem TauCeti.card_filter_le_eq_card_filter_lt_add_card_of_injective {n : β„•} {f : Fin n β†’ Fin n} (hf : Function.Injective f) :
    {p : Fin n Γ— Fin n | p.1 ≀ p.2 ∧ f p.1 ≀ f p.2}.card = {p : Fin n Γ— Fin n | p.1 < p.2 ∧ f p.1 < f p.2}.card + n

    Weakening both comparisons of a column-pair count along an injective row assignment adds exactly the n diagonal pairs: a pair c < d contributes to both counts or to neither, and each of the n columns contributes its own diagonal pair.

    source
    def TauCeti.GridPoint.JNumCenter {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
    β„•

    The numerator of the pairing of a set of grid points against a set of marked squares: the grid points southwest of a marking, plus the markings southwest of a grid point.

    Instances For
      source
      theorem TauCeti.GridPoint.JNumCenter_eq_JNumMixed {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
      JNumCenter s t = JNumMixed (fun (x1 x2 : Fin n Γ— Fin n) => x1 ≀ x2) s t

      The numerator of the marking pairing is the relation-parametric numerator at the weak product order.

      source
      theorem TauCeti.GridPoint.JNumCenter_def {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
      JNumCenter s t = ICenter s t + I t s

      The numerator of the marking pairing as a sum of its two directed counts.

      source
      theorem TauCeti.GridPoint.JNumCenter_eq_sum_singleton_left {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
      JNumCenter s t = βˆ‘ p ∈ s, JNumCenter {p} t

      The numerator of the marking pairing is the sum, over the left point set, of its singleton-left contributions.

      source
      theorem TauCeti.GridPoint.JNumCenter_singleton_left {n : β„•} (p : Fin n Γ— Fin n) (t : Finset (Fin n Γ— Fin n)) :
      JNumCenter {p} t = {q ∈ t | p ≀ q}.card + {q ∈ t | IsSouthWest q p}.card

      The numerator of the marking pairing of a single grid point against marked squares is the sum of the numbers of markings weakly northeast and strictly southwest of the point.

      source
      theorem TauCeti.GridPoint.JNumCenter_singleton_left_eq_card {n : β„•} (p : Fin n Γ— Fin n) (t : Finset (Fin n Γ— Fin n)) :
      JNumCenter {p} t = {q ∈ t | p ≀ q ∨ IsSouthWest q p}.card

      The numerator of the singleton marking pairing counts the marked squares weakly northeast or strictly southwest of the grid point.

      source
      theorem TauCeti.GridPoint.JNumCenter_singleton_right {n : β„•} (s : Finset (Fin n Γ— Fin n)) (p : Fin n Γ— Fin n) :
      JNumCenter s {p} = {q ∈ s | q ≀ p}.card + {q ∈ s | IsSouthWest p q}.card

      The numerator of the marking pairing against a single marked square is the sum of the numbers of grid points weakly southwest and strictly northeast of the marking.

      source
      @[simp]
      theorem TauCeti.GridPoint.JNumCenter_singleton_singleton {n : β„•} (p q : Fin n Γ— Fin n) :
      JNumCenter {p} {q} = (if p ≀ q then 1 else 0) + if IsSouthWest q p then 1 else 0

      The numerator of the marking pairing on singleton sets records its two comparisons.

      source
      theorem TauCeti.GridPoint.JNumCenter_image_swap {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
      JNumCenter (Finset.image Prod.swap s) (Finset.image Prod.swap t) = JNumCenter s t

      The numerator of the marking pairing is invariant under reflecting both point sets across the diagonal.

      source
      def TauCeti.GridPoint.JCenter {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
      β„š

      The rational-valued pairing of a set of grid points against a set of marked squares. This is the J-function of the grid, corrected for the half-unit offset of the markings.

      Instances For
        source
        theorem TauCeti.GridPoint.JCenter_eq_JMixed {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
        JCenter s t = JMixed (fun (x1 x2 : Fin n Γ— Fin n) => x1 ≀ x2) s t

        The marking pairing is the relation-parametric rational pairing at the weak product order.

        source
        theorem TauCeti.GridPoint.JCenter_def {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
        JCenter s t = ↑(JNumCenter s t) / 2

        The marking pairing is half its numerator.

        source
        theorem TauCeti.GridPoint.two_mul_JCenter {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
        2 * JCenter s t = ↑(JNumCenter s t)

        Twice the marking pairing is its integer numerator.

        source
        theorem TauCeti.GridPoint.JCenter_singleton_left {n : β„•} (p : Fin n Γ— Fin n) (t : Finset (Fin n Γ— Fin n)) :
        JCenter {p} t = ↑{q ∈ t | p ≀ q ∨ IsSouthWest q p}.card / 2

        The marking pairing of a single grid point against marked squares is half the number of markings weakly northeast or strictly southwest of the point.

        source
        theorem TauCeti.GridPoint.two_mul_JCenter_singleton_left {n : β„•} (p : Fin n Γ— Fin n) (t : Finset (Fin n Γ— Fin n)) :
        2 * JCenter {p} t = ↑{q ∈ t | p ≀ q ∨ IsSouthWest q p}.card

        Twice the singleton marking pairing is the number of marked squares weakly northeast or strictly southwest of the grid point.

        source
        theorem TauCeti.GridPoint.JCenter_singleton_right {n : β„•} (s : Finset (Fin n Γ— Fin n)) (p : Fin n Γ— Fin n) :
        JCenter s {p} = ↑({q ∈ s | q ≀ p}.card + {q ∈ s | IsSouthWest p q}.card) / 2

        The marking pairing against a single marked square is half the sum of the numbers of grid points weakly southwest and strictly northeast of the marking.

        source
        @[simp]
        theorem TauCeti.GridPoint.JCenter_singleton_singleton {n : β„•} (p q : Fin n Γ— Fin n) :
        JCenter {p} {q} = ↑((if p ≀ q then 1 else 0) + if IsSouthWest q p then 1 else 0) / 2

        The marking pairing on singleton sets is half its two-comparison numerator.

        source
        theorem TauCeti.GridPoint.JCenter_insert_pair_left {n : β„•} {S P : Finset (Fin n Γ— Fin n)} {a b : Fin n Γ— Fin n} (hab : a βˆ‰ insert b S) (hb : b βˆ‰ S) :
        JCenter (insert a (insert b S)) P = JCenter {a} P + JCenter {b} P + JCenter S P

        Splitting a two-point insertion out of the grid points of the marking pairing.

        source
        theorem TauCeti.GridPoint.JCenter_image_swap {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
        JCenter (Finset.image Prod.swap s) (Finset.image Prod.swap t) = JCenter s t

        The marking pairing is invariant under reflecting both point sets across the diagonal.

        source
        theorem TauCeti.GridPoint.J_sub_two_mul_JCenter_add_J_eq_intCast {n : β„•} (s t : Finset (Fin n Γ— Fin n)) :
        J s s - 2 * JCenter s t + J t t = ↑(↑(I s s) - ↑(JNumCenter s t) + ↑(I t t))

        The combination of the strict self-pairings and the doubled marking pairing is the cast of an integer expression on arbitrary point sets.

        source
        def TauCeti.GridState.JNumCenterAt {n : β„•} (m : GridState n) (c r : Fin n) :
        β„•

        The contribution of the grid point (c, r) to the numerator of the marking pairing against the squares occupied by m.

        Instances For
          source
          theorem TauCeti.GridState.JNumCenterAt_def {n : β„•} (m : GridState n) (c r : Fin n) :
          m.JNumCenterAt c r = GridPoint.JNumCenter {(c, r)} m.pointSet

          The local marking-pairing numerator as the existing singleton JNumCenter pairing.

          source
          theorem TauCeti.GridState.JNumCenterAt_eq_card {n : β„•} (m : GridState n) (c r : Fin n) :
          m.JNumCenterAt c r = {d : Fin n | c ≀ d ∧ r ≀ m.toPerm d}.card + {d : Fin n | d < c ∧ m.toPerm d < r}.card

          The local marking-pairing numerator as the sum of the numbers of markings weakly northeast and strictly southwest of the grid point.

          source
          theorem TauCeti.GridState.JNumCenter_pointSet_eq_sum {n : β„•} (x m : GridState n) :
          GridPoint.JNumCenter x.pointSet m.pointSet = βˆ‘ c : Fin n, m.JNumCenterAt c (x.toPerm c)

          The marking-pairing numerator of a grid state against marked squares is the sum, over its columns, of the local numerators contributed by the occupied grid points.

          source
          theorem TauCeti.GridState.ICenter_pointSet_eq_card {n : β„•} (x y : GridState n) :
          GridPoint.ICenter x.pointSet y.pointSet = {p : Fin n Γ— Fin n | p.1 ≀ p.2 ∧ x.toPerm p.1 ≀ y.toPerm p.2}.card

          The southwest-of-center count of the point sets of two grid states, as a column-pair count.

          source
          theorem TauCeti.GridState.JNumCenter_pointSet_eq_card {n : β„•} (x y : GridState n) :
          GridPoint.JNumCenter x.pointSet y.pointSet = {p : Fin n Γ— Fin n | p.1 ≀ p.2 ∧ x.toPerm p.1 ≀ y.toPerm p.2}.card + {p : Fin n Γ— Fin n | p.1 < p.2 ∧ y.toPerm p.1 < x.toPerm p.2}.card

          The numerator of the marking pairing on two state point sets, as a sum of two column-index counts.

          source
          theorem TauCeti.GridState.ICenter_self_pointSet_eq_I_add_card {n : β„•} (x : GridState n) :
          GridPoint.ICenter x.pointSet x.pointSet = GridPoint.I x.pointSet x.pointSet + n

          Pairing a grid state against the squares it occupies adds exactly the n diagonal pairs to the strict southwest count: the row assignment of a grid state is injective, so this is the column-pair count TauCeti.card_filter_le_eq_card_filter_lt_add_card_of_injective.

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

          The pairing of a grid state against the O-markings of a grid diagram.

          Instances For
            source
            @[simp]
            theorem TauCeti.GridDiagram.JO_def {n : β„•} (G : GridDiagram n) (x : GridState n) :
            G.JO x = GridPoint.JCenter x.pointSet G.OSet

            JO is the marking pairing of a state against the O-markings.

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

            The pairing of a grid state against the X-markings of a grid diagram.

            Instances For
              source
              @[simp]
              theorem TauCeti.GridDiagram.JX_def {n : β„•} (G : GridDiagram n) (x : GridState n) :
              G.JX x = GridPoint.JCenter x.pointSet G.XSet

              JX is the marking pairing of a state against the X-markings.

              source
              theorem TauCeti.GridDiagram.JO_eq_card {n : β„•} (G : GridDiagram n) (x : GridState n) :
              G.JO x = ↑({p : Fin n Γ— Fin n | p.1 ≀ p.2 ∧ x.toPerm p.1 ≀ G.O.toPerm p.2}.card + {p : Fin n Γ— Fin n | p.1 < p.2 ∧ G.O.toPerm p.1 < x.toPerm p.2}.card) / 2

              The O-marking pairing as a column-index count.

              source
              theorem TauCeti.GridDiagram.JX_eq_card {n : β„•} (G : GridDiagram n) (x : GridState n) :
              G.JX x = ↑({p : Fin n Γ— Fin n | p.1 ≀ p.2 ∧ x.toPerm p.1 ≀ G.X.toPerm p.2}.card + {p : Fin n Γ— Fin n | p.1 < p.2 ∧ G.X.toPerm p.1 < x.toPerm p.2}.card) / 2

              The X-marking pairing as a column-index count.

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

              JO is invariant under reflecting the diagram and state across the diagonal.

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

              JX is invariant under reflecting the diagram and state across the diagonal.

              source
              theorem TauCeti.GridDiagram.JO_swapMarkings {n : β„•} (G : GridDiagram n) (x : GridState n) :
              G.swapMarkings.JO x = G.JX x

              The marking swap exchanges the O-marking pairing with the X-marking pairing.

              source
              theorem TauCeti.GridDiagram.JX_swapMarkings {n : β„•} (G : GridDiagram n) (x : GridState n) :
              G.swapMarkings.JX x = G.JO x

              The marking swap exchanges the X-marking pairing with the O-marking pairing.