The pentagon map on unblocked grid homology

The pentagon-counting map of a column turn (GridDiagram.ColumnTurn) intertwines the unblocked differentials. It therefore induces a specified map on GH⁻, sending the class of a cycle to the class of its pentagon image. The map is semilinear along the transposition of the two coefficient variables. Over any commutative ring of characteristic two, for diagrams with an odd number of link components it raises the Maslov--Alexander bigrading by the bidegree GridDiagram.commutationBidegree of the turn, which vanishes for a column commutation. For knot grids it is linear over R[U] and homogeneous for the Alexander grading (GridDiagram.IsKnot.isHomogeneous_unblockedHomologyCommutationLinearMap).

The construction uses the concrete cycle quotient through unblockedHomologyIso and Mathlib's Submodule.mapQ. It supplies the homology map itself; invertibility requires the hexagon homotopy identities. In one direction this is recorded here: if the commutation map Φ of a column turn followed by a commutation map Ψ back at the same columns is chain homotopic to multiplication by a polynomial p, then ΨΦ acts on GH⁻ as p (GridDiagram.unblockedHomologyClass_commutationMap_withTurnRow_commutationMap).

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559).

theorem TauCeti.GridDiagram.commutationMap_mem_ker_unblockedDifferential {n : ℕ} (G : GridDiagram n) (R : Type u_1) (C : ColumnTurn n) [CommSemiring R] [CharP R 2] {z : GridChainMinus R n} (hz : z ∈ (G.unblockedDifferential R).ker) : (G.commutationMap R C) z ∈ ((swapColumns C.column ((finRotate n) C.column) G).unblockedDifferential R).ker

The pentagon map of a column turn sends cycles to cycles.

theorem TauCeti.GridDiagram.commutationMap_withTurnRow_commutationMap_mem_ker {n : ℕ} (G : GridDiagram n) (R : Type u_1) (C : ColumnTurn n) [CommSemiring R] [CharP R 2] (t : Fin n) {z : GridChainMinus R n} (hz : z ∈ (G.unblockedDifferential R).ker) : ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R (C.withTurnRow t)) ((G.commutationMap R C) z) ∈ (G.unblockedDifferential R).ker

The commutation map of a column turn followed by the commutation map back, turning at the same columns in any row t, sends cycles of GC⁻(G) to cycles of GC⁻(G).

noncomputable def TauCeti.GridDiagram.unblockedHomologyCommutationMap {n : ℕ} (G : GridDiagram n) (R : Type u_1) (C : ColumnTurn n) [CommRing R] [CharP R 2] : ↑(G.unblockedHomology R) →ₛₗ[↑(MvPolynomial.renameEquiv R (Equiv.swap C.column ((finRotate n) C.column))).toRingEquiv] ↑((swapColumns C.column ((finRotate n) C.column) G).unblockedHomology R)

The specified map on unblocked grid homology induced by the pentagon map of a column turn, for instance that of a column commutation. It is semilinear along the renaming that exchanges the two variables of the exchanged columns.

@[simp]

theorem TauCeti.GridDiagram.unblockedHomologyCommutationMap_unblockedHomologyClass {n : ℕ} (G : GridDiagram n) (R : Type u_1) (C : ColumnTurn n) [CommRing R] [CharP R 2] (z : ↥(G.unblockedDifferential R).ker) : (G.unblockedHomologyCommutationMap R C) ((G.unblockedHomologyClass R) z) = ((swapColumns C.column ((finRotate n) C.column) G).unblockedHomologyClass R) ⟨(G.commutationMap R C) ↑z, ⋯⟩

The commutation map sends a cycle class to the class of its pentagon image.

theorem TauCeti.GridDiagram.unblockedHomologyClass_commutationMap_withTurnRow_commutationMap {n : ℕ} (G : GridDiagram n) (R : Type u_1) (C : ColumnTurn n) [CommRing R] [CharP R 2] (t : Fin n) (H : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n) (p : MvPolynomial (Fin n) R) (hH : ∀ (c : GridChainMinus R n), (G.unblockedDifferential R) (H c) + H ((G.unblockedDifferential R) c) = p • c + ((swapColumns C.column ((finRotate n) C.column) G).commutationMap R (C.withTurnRow t)) ((G.commutationMap R C) c)) (z : ↥(G.unblockedDifferential R).ker) : (G.unblockedHomologyClass R) ⟨((swapColumns C.column ((finRotate n) C.column) G).commutationMap R (C.withTurnRow t)) ((G.commutationMap R C) ↑z), ⋯⟩ = p • (G.unblockedHomologyClass R) z

The return composite on homology. Let Φ be the commutation map of the column turn C and Ψ the commutation map back, turning at the same columns in row t. If ΨΦ is chain homotopic to multiplication by a polynomial p, that is ∂H + H∂ = p + ΨΦ over a ring of characteristic two, then ΨΦ sends the class in GH⁻(G) of every cycle z to p times that class.

theorem TauCeti.OddComponentGridDiagram.unblockedHomologyCommutationMap_mem_bigradedUnblockedHomologyPiece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (C : GridDiagram.ColumnTurn n) {g : ℤ × ℤ} {y : ↑((↑G).unblockedHomology R)} (hy : y ∈ G.bigradedUnblockedHomologyPiece R g) : ((↑G).unblockedHomologyCommutationMap R C) y ∈ (G.swapColumns C).bigradedUnblockedHomologyPiece R (g + (↑G).commutationBidegree C)

The commutation map of a column turn C on GH⁻ raises the full Maslov--Alexander bidegree by G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.unblockedHomologyCommutationMap_mem_alexanderUnblockedHomologyGrading_piece_add {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (C : GridDiagram.ColumnTurn n) {a : ℤ} {y : ↑((↑G).unblockedHomology R)} (hy : y ∈ (G.alexanderUnblockedHomologyGrading R).piece ℤ a) : ((↑G).unblockedHomologyCommutationMap R C) y ∈ ((G.swapColumns C).alexanderUnblockedHomologyGrading R).piece ℤ (a + ((↑G).commutationBidegree C).2)

The commutation map of a column turn C on GH⁻ raises the Alexander grading by the Alexander component of G.commutationBidegree C.

theorem TauCeti.OddComponentGridDiagram.unblockedHomologyCommutationMap_mem_bigradedUnblockedHomologyPiece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (C : (↑G).ColumnCommutationData) {g : ℤ × ℤ} {y : ↑((↑G).unblockedHomology R)} (hy : y ∈ G.bigradedUnblockedHomologyPiece R g) : ((↑G).unblockedHomologyCommutationMap R C.toColumnTurn) y ∈ (G.swapColumns C.toColumnTurn).bigradedUnblockedHomologyPiece R g

The commutation map on GH⁻ preserves the full Maslov--Alexander bigrading.

theorem TauCeti.OddComponentGridDiagram.unblockedHomologyCommutationMap_mem_alexanderUnblockedHomologyGrading_piece {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (C : (↑G).ColumnCommutationData) {a : ℤ} {y : ↑((↑G).unblockedHomology R)} (hy : y ∈ (G.alexanderUnblockedHomologyGrading R).piece ℤ a) : ((↑G).unblockedHomologyCommutationMap R C.toColumnTurn) y ∈ ((G.swapColumns C.toColumnTurn).alexanderUnblockedHomologyGrading R).piece ℤ a

The commutation map on GH⁻ preserves the Alexander grading.

noncomputable def TauCeti.GridDiagram.IsKnot.unblockedHomologyCommutationLinearMap {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] (C : ColumnTurn n) : ↑(G.unblockedHomology R) →ₗ[Polynomial R] ↑((GridDiagram.swapColumns C.column ((finRotate n) C.column) G).unblockedHomology R)

For a knot grid, the specified commutation map of a column turn is linear over R[U], since renaming the grid variables commutes with their common specialization to U.

@[simp]

theorem TauCeti.GridDiagram.IsKnot.unblockedHomologyCommutationLinearMap_apply {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] (C : ColumnTurn n) (y : ↑(G.unblockedHomology R)) : (hG.unblockedHomologyCommutationLinearMap R C) y = (G.unblockedHomologyCommutationMap R C) y

The R[U]-linear map acts by the specified semilinear commutation map.

theorem TauCeti.GridDiagram.IsKnot.isHomogeneous_unblockedHomologyCommutationLinearMap {n : ℕ} {G : GridDiagram n} (hG : G.IsKnot) (R : Type u_1) [CommRing R] [CharP R 2] (C : ColumnTurn n) : LinearMap.IsHomogeneous (hG.unblockedHomologyCommutationLinearMap R C) ((hG.alexanderUnblockedHomologyGrading R).piece ℤ) ((⋯.alexanderUnblockedHomologyGrading R).piece ℤ) (G.commutationBidegree C).2

For a knot grid, the R[U]-linear commutation map of a column turn C is homogeneous for the Alexander gradings, of degree the Alexander component of G.commutationBidegree C.