Documentation

TauCeti.KnotTheory.Grid.Grading.Southwest

The Alexander grading as a sum of southwest marking counts #

The pairing of a grid point (c, r) against the squares occupied by a grid state m (GridState.JNumCenterAt) counts the points of m weakly northeast of (c, r) together with those strictly southwest of it. Since m occupies one point in every column and every row, the northeast count is determined by the southwest count: writing southwestCount m c r for the number of columns d < c with m d < r,

JNumCenterAt m c r + c + r = n + 2 · southwestCount m c r (GridState.JNumCenterAt_add_add).

Substituting this into the two marking pairings of the Alexander grading formula, the terms that do not involve the markings cancel between the O- and X-pairings, and the doubled integer Alexander grading of a grid state x becomes a sum over its columns (GridDiagram.alexanderTwoℤ_eq_sum_southwestCount):

`2 A(x) = 2 ∑_c (southwestCount 𝕏 c (x c) - southwestCount 𝕆 c (x c))

The summands southwestCount 𝕏 c (x c) - southwestCount 𝕆 c (x c) are, up to sign, the winding numbers of the link diagram around the points of x; the two remaining sums are the numbers of non-inversions of the marking permutations (GridState.I_self_pointSet_eq_sum_southwestCount). This is the form in which the Alexander grading of a grid state is compared with that of a distinguished state, since each summand is bounded by min c (x c) (GridState.southwestCount_le_min), with equality for the identity state (GridState.southwestCount_of_apply_eq).

Main definitions #

Main results #

References #

The winding-number form of the Alexander grading is Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 4.7, Proposition 4.7.2. The column-sum form above is that formula with each winding number written as a difference of southwest counts and with the constant term kept as the non-inversion counts of the marking permutations.

source
def TauCeti.GridState.southwestCount {n : ℕ} (m : GridState n) (c r : Fin n) :
ℕ

The number of points of the grid state m strictly southwest of the grid point (c, r): the columns d < c whose point lies in a row below r.

Instances For
    source
    theorem TauCeti.GridState.southwestCount_def {n : ℕ} (m : GridState n) (c r : Fin n) :
    m.southwestCount c r = {d : Fin n | d < c ∧ m.toPerm d < r}.card

    The southwest count as the cardinality of the set of columns it counts.

    source
    theorem TauCeti.GridState.southwestCount_le_left {n : ℕ} (m : GridState n) (c r : Fin n) :
    m.southwestCount c r ≤ ↑c

    The southwest count of (c, r) is at most the number c of columns to the left of c.

    source
    theorem TauCeti.GridState.card_filter_apply_lt {n : ℕ} (m : GridState n) (r : Fin n) :
    {d : Fin n | m.toPerm d < r}.card = ↑r

    A grid state has exactly r points in the rows below r.

    source
    theorem TauCeti.GridState.southwestCount_le_right {n : ℕ} (m : GridState n) (c r : Fin n) :
    m.southwestCount c r ≤ ↑r

    The southwest count of (c, r) is at most the number r of rows below r.

    source
    theorem TauCeti.GridState.southwestCount_le_min {n : ℕ} (m : GridState n) (c r : Fin n) :
    m.southwestCount c r ≤ min ↑c ↑r

    The southwest count of (c, r) is at most min c r.

    source
    theorem TauCeti.GridState.southwestCount_of_apply_eq {n : ℕ} (m : GridState n) (c r : Fin n) (hm : ∀ (d : Fin n), m.toPerm d = d) :
    m.southwestCount c r = min ↑c ↑r

    The southwest counts of the identity state, whose points lie on the diagonal, are min c r.

    source
    theorem TauCeti.GridState.JNumCenterAt_add_add {n : ℕ} (m : GridState n) (c r : Fin n) :
    m.JNumCenterAt c r + ↑c + ↑r = n + 2 * m.southwestCount c r

    The marking pairing of the grid point (c, r) against the squares of m is determined by the southwest count: JNumCenterAt m c r + c + r = n + 2 · southwestCount m c r. The northeast count is the n - c columns from c on, minus those whose point lies below r, and the latter are the r points below r minus the southwest count.

    source
    theorem TauCeti.GridState.I_self_pointSet_eq_sum_southwestCount {n : ℕ} (m : GridState n) :
    GridPoint.I m.pointSet m.pointSet = ∑ c : Fin n, m.southwestCount c (m.toPerm c)

    The number of non-inversions of a grid state is the sum over its columns of the southwest counts at its own points.

    source
    theorem TauCeti.GridState.JNumCenter_pointSet_eq_sum_southwestCount {n : ℕ} (x m : GridState n) :
    ↑(GridPoint.JNumCenter x.pointSet m.pointSet) = ∑ c : Fin n, (↑n + 2 * ↑(m.southwestCount c (x.toPerm c)) - ↑↑c - ↑↑(x.toPerm c))

    The marking pairing of a grid state against a marking state, as a sum of southwest counts: the terms not involving the markings are the same for every marking state.

    source
    theorem TauCeti.GridDiagram.alexanderTwoℤ_eq_sum_southwestCount {n : ℕ} (G : GridDiagram n) (x : GridState n) :
    G.alexanderTwoℤ x = 2 * ∑ c : Fin n, (↑(G.X.southwestCount c (x.toPerm c)) - ↑(G.O.southwestCount c (x.toPerm c))) + ∑ c : Fin n, ↑(G.O.southwestCount c (G.O.toPerm c)) - ∑ c : Fin n, ↑(G.X.southwestCount c (G.X.toPerm c)) - (↑n - 1)

    The Alexander grading as a sum over columns. Twice the integer Alexander grading of a grid state x is twice the sum over the columns c of the differences of the southwest counts of (c, x c) for the X- and the O-markings, corrected by the non-inversion counts of the two marking states and the normalization shift.