The bidegree of the grid commutation map

The commutation map of a column turn C counts both terminal-side and initial-side pentagons. The grading-change formulas of Grading/Basic.lean imply that both contributions raise the bidegree of every monomial generator of GC⁻ by the same amount, the bidegree GridDiagram.commutationBidegree C of the turn: an O-marking raises the target state's Maslov and Alexander gradings by (2, 1), its renamed variable contributes (-2, -1), and what remains is the position of the turn row relative to the markings of the two exchanged columns.

For a column commutation the bidegree of the turn vanishes, so the terminal-side and initial-side pentagon maps and their sum GridDiagram.commutationMap preserve the bigraded and the Alexander-homogeneous chain pieces. For a turn exchanging two columns whose marking segments interleave, the same maps are homogeneous of a possibly nonzero bidegree; these are the maps attached to a crossing change in TauCeti.KnotTheory.Grid.CrossingChange.Grading. Taking constant terms, the fully blocked pentagon map GridDiagram.fullyBlockedCommutationMap of a column commutation preserves the bidegree of every state.

These are grading statements over arbitrary commutative semirings, not chain-map or homotopy-equivalence assertions. The integer Alexander grading requires an odd number of link components, as in the existing unblocked bigrading API.

Main results

• TauCeti.OddComponentGridDiagram.pentagonMap_mem_bigradedChainMinusPiece_add, TauCeti.OddComponentGridDiagram.initialPentagonMap_mem_bigradedChainMinusPiece_add and TauCeti.OddComponentGridDiagram.commutationMap_mem_bigradedChainMinusPiece_add: the pentagon maps of a column turn raise the bidegree by the bidegree of the turn.
• TauCeti.OddComponentGridDiagram.pentagonMap_mem_alexanderChainMinusPiece_add, TauCeti.OddComponentGridDiagram.initialPentagonMap_mem_alexanderChainMinusPiece_add and TauCeti.OddComponentGridDiagram.commutationMap_mem_alexanderChainMinusPiece_add: likewise for the Alexander grading alone.
• TauCeti.OddComponentGridDiagram.commutationMap_mem_bigradedChainMinusPiece and TauCeti.OddComponentGridDiagram.commutationMap_mem_alexanderChainMinusPiece, with their terminal-side and initial-side parts: for a column commutation these maps preserve the gradings.
• TauCeti.OddComponentGridDiagram.fullyBlockedCommutationMap_single_apply_eq_zero_of_bidegree_ne: the fully blocked pentagon map of a column commutation has no matrix entries between states of different bidegrees.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Sections 5.1 and 6.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559). The argument uses the state-grading formulas in TauCeti.KnotTheory.Grid.Commutation.Grading.Basic and the polynomial-support API.

theorem TauCeti.OddComponentGridDiagram.pentagonMap_mem_bigradedChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (C : GridDiagram.ColumnTurn n) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).pentagonMap R C) c ∈ (G.swapColumns C).bigradedChainMinusPiece R (g + (↑G).commutationBidegree C)

The bidegree of the pentagon map. The pentagon map of a column turn C sends a chain of GC⁻(G) that is homogeneous of bidegree g to a chain of GC⁻ of the diagram with the two columns of C exchanged that is homogeneous of bidegree g + G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.pentagonMap_mem_alexanderChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (C : GridDiagram.ColumnTurn n) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).pentagonMap R C) c ∈ (G.swapColumns C).alexanderChainMinusPiece R (a + ((↑G).commutationBidegree C).2)

The pentagon map of a column turn C sends a chain of GC⁻(G) of Alexander degree a to a chain of Alexander degree a plus the Alexander component of G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.initialPentagonMap_mem_bigradedChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (C : GridDiagram.ColumnTurn n) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).initialPentagonMap R C) c ∈ (G.swapColumns C).bigradedChainMinusPiece R (g + (↑G).commutationBidegree C)

The initial-side pentagon map of a column turn C raises the bidegree of homogeneous chains by G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.initialPentagonMap_mem_alexanderChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (C : GridDiagram.ColumnTurn n) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).initialPentagonMap R C) c ∈ (G.swapColumns C).alexanderChainMinusPiece R (a + ((↑G).commutationBidegree C).2)

The initial-side pentagon map of a column turn C raises the Alexander degree of homogeneous chains by the Alexander component of G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.commutationMap_mem_bigradedChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (C : GridDiagram.ColumnTurn n) {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).commutationMap R C) c ∈ (G.swapColumns C).bigradedChainMinusPiece R (g + (↑G).commutationBidegree C)

The bidegree of the commutation map. The commutation map of a column turn C, counting both kinds of pentagon, sends a chain of GC⁻(G) homogeneous of bidegree g to a chain of GC⁻ of the diagram with the two columns of C exchanged of bidegree g + G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.commutationMap_mem_alexanderChainMinusPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommSemiring R] (C : GridDiagram.ColumnTurn n) {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).commutationMap R C) c ∈ (G.swapColumns C).alexanderChainMinusPiece R (a + ((↑G).commutationBidegree C).2)

The commutation map of a column turn C raises the Alexander degree of homogeneous chains by the Alexander component of G.commutationBidegree C.

Column commutations

theorem TauCeti.OddComponentGridDiagram.pentagonMap_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).pentagonMap R C.toColumnTurn) c ∈ (G.swapColumns C.toColumnTurn).bigradedChainMinusPiece R g

The pentagon map preserves the bigrading. The pentagon map of a validated column commutation C sends a chain of GC⁻(G) that is homogeneous of bidegree g to a chain of GC⁻ of the commuted diagram that is homogeneous of the same bidegree.

theorem TauCeti.OddComponentGridDiagram.pentagonMap_mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).pentagonMap R C.toColumnTurn) c ∈ (G.swapColumns C.toColumnTurn).alexanderChainMinusPiece R a

The pentagon map preserves the Alexander grading. The pentagon map of a validated column commutation C sends a chain of GC⁻(G) of Alexander degree a to a chain of GC⁻ of the commuted diagram of the same Alexander degree.

theorem TauCeti.OddComponentGridDiagram.initialPentagonMap_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).initialPentagonMap R C.toColumnTurn) c ∈ (G.swapColumns C.toColumnTurn).bigradedChainMinusPiece R g

The initial-side pentagon map sends a chain of GC⁻(G) homogeneous of bidegree g to a chain of GC⁻ of the commuted diagram homogeneous of the same bidegree.

theorem TauCeti.OddComponentGridDiagram.initialPentagonMap_mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).initialPentagonMap R C.toColumnTurn) c ∈ (G.swapColumns C.toColumnTurn).alexanderChainMinusPiece R a

The initial-side pentagon map sends a chain of GC⁻(G) of Alexander degree a to a chain of GC⁻ of the commuted diagram of the same Alexander degree.

theorem TauCeti.OddComponentGridDiagram.commutationMap_mem_bigradedChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {g : ℤ × ℤ} {c : GridChainMinus R n} (hc : c ∈ G.bigradedChainMinusPiece R g) : ((↑G).commutationMap R C.toColumnTurn) c ∈ (G.swapColumns C.toColumnTurn).bigradedChainMinusPiece R g

The full commutation map, counting both kinds of pentagon, sends a chain of GC⁻(G) homogeneous of bidegree g to a chain of GC⁻ of the commuted diagram of the same bidegree.

theorem TauCeti.OddComponentGridDiagram.commutationMap_mem_alexanderChainMinusPiece {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {a : ℤ} {c : GridChainMinus R n} (hc : c ∈ G.alexanderChainMinusPiece R a) : ((↑G).commutationMap R C.toColumnTurn) c ∈ (G.swapColumns C.toColumnTurn).alexanderChainMinusPiece R a

The full commutation map, counting both kinds of pentagon, sends a chain of GC⁻(G) of Alexander degree a to a chain of GC⁻ of the commuted diagram of the same Alexander degree.

theorem TauCeti.OddComponentGridDiagram.fullyBlockedCommutationMap_single_apply_eq_zero_of_bidegree_ne {n : ℕ} (G : OddComponentGridDiagram n) (C : (↑G).ColumnCommutationData) (R : Type u_2) [CommSemiring R] {x y : GridState n} (h : (G.swapColumns C.toColumnTurn).bidegree y ≠ G.bidegree x) : (((↑G).fullyBlockedCommutationMap R C) (Finsupp.single x 1)) y = 0

The fully blocked pentagon map has no matrix entries between states of different bidegrees: a pentagon carrying no markings preserves both the O-Maslov and the Alexander grading.