Grading changes across grid commutation pentagons

Let C be a column turn (GridDiagram.ColumnTurn) of a grid diagram G, exchanging the column a = C.column with the next column b = finRotate n a and turning in the square row s = C.turnRow, and let G' be the diagram G.swapColumns a b. The pentagon map Φ : GC⁻(G) → GC⁻(G') (GridDiagram.pentagonMap) sends a state x to the sum, over the empty pentagons P from x carrying no X-marking and turning on their terminal side, of V^{𝕆 ∩ P} · y with y the target of P. This file proves the state-grading formulas for pentagons turning on either side. Grading/Map.lean uses them to prove that both parts and the full commutation map GridDiagram.commutationMap are homogeneous for the (O-Maslov, Alexander) bigrading of Grading/Unblocked/Chain.lean, of the bidegree GridDiagram.commutationBidegree C defined here.

The grid states of G and G' are the same permutations, and the comparison rests on two grading formulas.

• Changing the diagram. Exchanging the two markings of the adjacent columns a and b changes the O-Maslov grading of a fixed state x by ±1 (GridDiagram.maslovOℤ_swapColumns_finRotate). It rises by one exactly when the point of x on the grid line between the two columns lies on one of the lines G.O a + 1, …, G.O b, which the two O-markings pass when they trade columns.
• Following a pentagon. For every empty pentagon P from x to y, M_O'(y) = M_O(x) + 2 #(𝕆 ∩ P) (GridDiagram.maslovOℤ_swapColumns_of_isEmpty), and likewise M_X'(y) = M_X(x) + 2 #(𝕏 ∩ P) (GridDiagram.maslovXℤ_swapColumns_of_isEmpty), counting the markings of G that P carries and writing M_O', M_X' for the gradings of G', up to a correction -2 when s lies strictly between the two O-markings, respectively X-markings, of the columns b and a, going up.

The correction is the bookkeeping of the cut at the turn row: the pentagon carries a marking of column a exactly when it lies above s and one of column b exactly when it lies below s. For a column commutation, whose markings lie in the bigons below and above the turn, the corrections vanish (GridDiagram.ColumnCommutationData.commutationBidegree_eq_zero). When the two marking segments interleave they need not, which is the source of the nonzero bidegrees of the crossing change maps in TauCeti.KnotTheory.Grid.CrossingChange.Grading.

A counted pentagon carries no X-marking, so it changes M_X only by the correction and raises the Alexander grading by the number of O-markings it carries plus the Alexander component of GridDiagram.commutationBidegree C (GridDiagram.alexanderTwoℤ_swapColumns_of_mem_pentagons and OddComponentGridDiagram.alexanderℤ_swapColumns_of_mem_pentagons). Since every variable has bidegree (-2, -1), each term V^{𝕆 ∩ P} · y of Φ(x) has the bidegree of x plus GridDiagram.commutationBidegree C.

Main definitions

• TauCeti.GridDiagram.commutationBidegree: the bidegree of the pentagon maps of a column turn.
• TauCeti.OddComponentGridDiagram.swapColumns: the diagram with the two columns of a column turn exchanged, again with an odd number of components.

Main results

• TauCeti.GridDiagram.maslovOℤ_swapColumns_finRotate: the O-Maslov grading of a state under an exchange of two adjacent columns of the diagram.
• TauCeti.GridDiagram.ColumnCommutationData.commutationBidegree_eq_zero: the turn of a column commutation has bidegree zero.
• TauCeti.GridDiagram.maslovOℤ_swapColumns_of_isEmpty, TauCeti.GridDiagram.maslovXℤ_swapColumns_of_isEmpty: the two Maslov gradings across an empty pentagon.
• TauCeti.GridDiagram.maslovOℤ_swapColumns_initialPentagon_of_isEmpty, TauCeti.GridDiagram.maslovXℤ_swapColumns_initialPentagon_of_isEmpty: the Maslov grading changes across an empty initial-side pentagon.
• TauCeti.OddComponentGridDiagram.alexanderℤ_swapColumns_of_mem_initialPentagons: the Alexander grading change across a counted initial-side pentagon.
• TauCeti.OddComponentGridDiagram.alexanderℤ_swapColumns_of_mem_pentagons: the Alexander grading across a counted pentagon.

References

• P. Ozsváth, A. Stipsicz, Z. Szabó, Grid Homology for Knots and Links, AMS Mathematical Surveys and Monographs 208, 2015, Section 5.1, where the pentagon map of a commutation is shown to preserve the Maslov and Alexander gradings, and Section 6.1 for the crossing change maps.
• C. Manolescu, P. Ozsváth, Z. Szabó, D. Thurston, On combinatorial link Floer homology, Geom. Topol. 11 (2007), Section 3.1 (arXiv:math/0610559).

The O-Maslov grading under an adjacent column swap

theorem TauCeti.GridDiagram.maslovOℤ_swapColumns_finRotate {n : ℕ} (G : GridDiagram n) {a : Fin n} (ha : a ≠ (finRotate n) a) (x : GridState n) : (swapColumns a ((finRotate n) a) G).maslovOℤ x = G.maslovOℤ x + if x.toPerm ((finRotate n) a) ∈ Grid.cIco ((finRotate n) (G.O.toPerm a)) ((finRotate n) (G.O.toPerm ((finRotate n) a))) then 1 else -1

The O-Maslov grading under an adjacent column swap. Exchanging two cyclically adjacent columns a and b = finRotate n a of a grid diagram changes the O-Maslov grading of a grid state x by ±1: it rises by one exactly when the point of x on the grid line between the two columns, in row x b, lies strictly above the O-marking of column a and weakly below that of column b, cyclically. Those are the lines G.O a + 1, …, G.O b, which the two markings pass when they trade columns.

The bidegree of a column turn

noncomputable def TauCeti.GridDiagram.commutationBidegree {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) : ℤ × ℤ

The bidegree of the pentagon maps of the column turn C of G, for the (O-Maslov, Alexander) bigrading. Write a = C.column, b = finRotate n a and s = C.turnRow. The O-markings of the two columns contribute (-2, -1) when s lies strictly between G.O b and G.O a going up, that is, outside the closed arc from G.O a up to G.O b. The X-markings contribute (0, 1) when s lies strictly between G.X b and G.X a. For the turn of a column commutation both contributions vanish (GridDiagram.ColumnCommutationData.commutationBidegree_eq_zero); when the two marking segments interleave they need not.

@[simp]

theorem TauCeti.GridDiagram.commutationBidegree_fst {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) : (G.commutationBidegree C).1 = if C.turnRow ∈ Grid.cIoo (G.O.toPerm ((finRotate n) C.column)) (G.O.toPerm C.column) then -2 else 0

The O-Maslov component of the bidegree of a column turn.

@[simp]

theorem TauCeti.GridDiagram.commutationBidegree_snd {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) : (G.commutationBidegree C).2 = (if C.turnRow ∈ Grid.cIoo (G.X.toPerm ((finRotate n) C.column)) (G.X.toPerm C.column) then 1 else 0) - if C.turnRow ∈ Grid.cIoo (G.O.toPerm ((finRotate n) C.column)) (G.O.toPerm C.column) then 1 else 0

The Alexander component of the bidegree of a column turn.

@[simp]

theorem TauCeti.GridDiagram.ColumnCommutationData.commutationBidegree_eq_zero {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) : G.commutationBidegree C.toColumnTurn = 0

The turn of a column commutation has bidegree zero: the markings of its first column lie in the bigon below the turn and those of the next column in the bigon above it.

The gradings across a pentagon

theorem TauCeti.GridDiagram.maslovOℤ_swapColumns_of_isEmpty {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridPentagonBetween C.column C.turnRow x y} (hP : P.IsEmpty) : (swapColumns C.column ((finRotate n) C.column) G).maslovOℤ y = G.maslovOℤ x + 2 * ↑(G.pentagonOColumns C P).card + (G.commutationBidegree C).1

The O-Maslov grading across a pentagon. If P is an empty pentagon of the column turn C from a state x of G to a state y of the diagram with the two columns of C exchanged, then M_O(y) = M_O(x) + 2 #(𝕆 ∩ P) + δ, counting the O-markings of G that P carries, where δ is the Maslov component of G.commutationBidegree C. With every variable of weight -2, the term V^{𝕆 ∩ P} · y of the pentagon map has the O-Maslov grading of x shifted by δ, which vanishes for a column commutation.

theorem TauCeti.GridDiagram.maslovXℤ_swapColumns_of_isEmpty {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridPentagonBetween C.column C.turnRow x y} (hP : P.IsEmpty) : (swapColumns C.column ((finRotate n) C.column) G).maslovXℤ y = G.maslovXℤ x + 2 * ↑(G.XSet ∩ P.coveredSquares).card - 2 * if C.turnRow ∈ Grid.cIoo (G.X.toPerm ((finRotate n) C.column)) (G.X.toPerm C.column) then 1 else 0

The X-Maslov grading across a pentagon. If P is an empty pentagon of the column turn C from x to y, then M_X(y) = M_X(x) + 2 #(𝕏 ∩ P), corrected by -2 when the turn row lies strictly between the X-markings of the second and the first column of C, going up.

theorem TauCeti.GridDiagram.maslovXℤ_swapColumns_of_mem_pentagons {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridPentagonBetween C.column C.turnRow x y} (hP : P ∈ G.pentagons C x y) : (swapColumns C.column ((finRotate n) C.column) G).maslovXℤ y = G.maslovXℤ x - 2 * if C.turnRow ∈ Grid.cIoo (G.X.toPerm ((finRotate n) C.column)) (G.X.toPerm C.column) then 1 else 0

A pentagon counted by the pentagon map carries no X-marking, so it changes the X-Maslov grading only by the correction of maslovXℤ_swapColumns_of_isEmpty; in particular it preserves the X-Maslov grading for a column commutation.

theorem TauCeti.GridDiagram.alexanderTwoℤ_swapColumns_of_mem_pentagons {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridPentagonBetween C.column C.turnRow x y} (hP : P ∈ G.pentagons C x y) : (swapColumns C.column ((finRotate n) C.column) G).alexanderTwoℤ y = G.alexanderTwoℤ x + 2 * ↑(G.pentagonOColumns C P).card + 2 * (G.commutationBidegree C).2

The Alexander grading across a counted pentagon, in its doubled integer form: a pentagon counted by the pentagon map from x to y raises it by twice the number of O-markings it carries, shifted by twice the Alexander component of G.commutationBidegree C.

theorem TauCeti.GridDiagram.maslovOℤ_swapColumns_initialPentagon_of_isEmpty {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridInitialPentagonBetween C.column C.turnRow x y} (hP : P.IsEmpty) : (swapColumns C.column ((finRotate n) C.column) G).maslovOℤ y = G.maslovOℤ x + 2 * ↑(G.OColumnsOfSquares P.coveredSquares).card + (G.commutationBidegree C).1

An empty pentagon turning on its initial side raises the target O-Maslov grading by twice its number of covered O-markings, shifted by the Maslov component of G.commutationBidegree C.

theorem TauCeti.GridDiagram.maslovXℤ_swapColumns_initialPentagon_of_isEmpty {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridInitialPentagonBetween C.column C.turnRow x y} (hP : P.IsEmpty) : (swapColumns C.column ((finRotate n) C.column) G).maslovXℤ y = G.maslovXℤ x + 2 * ↑(G.XSet ∩ P.coveredSquares).card - 2 * if C.turnRow ∈ Grid.cIoo (G.X.toPerm ((finRotate n) C.column)) (G.X.toPerm C.column) then 1 else 0

An empty pentagon turning on its initial side raises the target X-Maslov grading by twice its number of covered X-markings, corrected by -2 when the turn row lies strictly between the X-markings of the second and the first column of C, going up.

theorem TauCeti.GridDiagram.maslovXℤ_swapColumns_of_mem_initialPentagons {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridInitialPentagonBetween C.column C.turnRow x y} (hP : P ∈ G.initialPentagons C x y) : (swapColumns C.column ((finRotate n) C.column) G).maslovXℤ y = G.maslovXℤ x - 2 * if C.turnRow ∈ Grid.cIoo (G.X.toPerm ((finRotate n) C.column)) (G.X.toPerm C.column) then 1 else 0

A counted initial-side pentagon avoids every X-marking, so it changes the X-Maslov grading only by the correction of maslovXℤ_swapColumns_initialPentagon_of_isEmpty.

theorem TauCeti.GridDiagram.alexanderTwoℤ_swapColumns_of_mem_initialPentagons {n : ℕ} (G : GridDiagram n) (C : ColumnTurn n) {x y : GridState n} {P : GridInitialPentagonBetween C.column C.turnRow x y} (hP : P ∈ G.initialPentagons C x y) : (swapColumns C.column ((finRotate n) C.column) G).alexanderTwoℤ y = G.alexanderTwoℤ x + 2 * ↑(G.OColumnsOfSquares P.coveredSquares).card + 2 * (G.commutationBidegree C).2

A counted initial-side pentagon raises the doubled Alexander grading by twice its number of covered O-markings, shifted by twice the Alexander component of G.commutationBidegree C.

@[reducible, inline]

abbrev TauCeti.OddComponentGridDiagram.swapColumns {n : ℕ} (G : OddComponentGridDiagram n) (C : GridDiagram.ColumnTurn n) : OddComponentGridDiagram n

The diagram obtained from a grid diagram with an odd number of components by exchanging the two columns of a column turn: relabeling columns does not change the number of components.

theorem TauCeti.OddComponentGridDiagram.val_swapColumns {n : ℕ} (G : OddComponentGridDiagram n) (C : GridDiagram.ColumnTurn n) : ↑(G.swapColumns C) = GridDiagram.swapColumns C.column ((finRotate n) C.column) ↑G

The underlying grid diagram of G.swapColumns C exchanges the two columns of C.

theorem TauCeti.OddComponentGridDiagram.alexanderℤ_swapColumns_of_mem_pentagons {n : ℕ} (G : OddComponentGridDiagram n) (C : GridDiagram.ColumnTurn n) {x y : GridState n} {P : GridPentagonBetween C.column C.turnRow x y} (hP : P ∈ (↑G).pentagons C x y) : (G.swapColumns C).alexanderℤ y = G.alexanderℤ x + ↑((↑G).pentagonOColumns C P).card + ((↑G).commutationBidegree C).2

The Alexander grading across a counted pentagon: a pentagon counted by the pentagon map from x to y raises the Alexander grading by the number of O-markings it carries, shifted by the Alexander component of G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.alexanderℤ_swapColumns_of_mem_initialPentagons {n : ℕ} (G : OddComponentGridDiagram n) (C : GridDiagram.ColumnTurn n) {x y : GridState n} {P : GridInitialPentagonBetween C.column C.turnRow x y} (hP : P ∈ (↑G).initialPentagons C x y) : (G.swapColumns C).alexanderℤ y = G.alexanderℤ x + ↑((↑G).OColumnsOfSquares P.coveredSquares).card + ((↑G).commutationBidegree C).2

A counted initial-side pentagon raises the integer Alexander grading by its number of covered O-markings, shifted by the Alexander component of G.commutationBidegree C.