The fully blocked commutation homotopy

Setting every marking variable to zero in the hexagon-counting commutation homotopy H of a validated column commutation C retains exactly the empty hexagons avoiding every O- and X-marking. The result is the hexagon map H~ of the fully blocked complex GC~(G), which is the reduction of H modulo the variables (LinearMap.constantCoeffReduction).

Reducing the two homotopy equations of the unblocked complex modulo the variables gives their fully blocked versions. Write Φ~ : GC~(G) → GC~(G') and Ψ~ : GC~(G') → GC~(G) for the fully blocked pentagon maps of C and of its reverse, where G' is the commuted diagram, and H~' for the fully blocked hexagon map of the reverse commutation. Then

∂~ ∘ H~ + H~ ∘ ∂~ = 1 + Ψ~ ∘ Φ~ and ∂~' ∘ H~' + H~' ∘ ∂~' = 1 + Φ~ ∘ Ψ~,

so Φ~ and Ψ~ are mutually inverse chain homotopy equivalences of the fully blocked complexes. Reduction modulo the variables needs no identification of the chain modules of G and of the doubly commuted diagram, since the fully blocked chain module GridChain (ZMod 2) n does not depend on the diagram.

Main definitions

• TauCeti.GridDiagram.fullyBlockedCommutationHomotopy: the fully blocked hexagon map.

Main results

• TauCeti.GridDiagram.fullyBlockedCommutationHomotopy_mapRange_constantCoeff: the fully blocked hexagon map is the reduction of the unblocked one.
• TauCeti.GridDiagram.fullyBlockedDifferential_fullyBlockedCommutationHomotopy_add_eq: the homotopy equation ∂~ ∘ H~ + H~ ∘ ∂~ = 1 + Ψ~ ∘ Φ~.
• TauCeti.GridDiagram.fullyBlockedDifferential_fullyBlockedCommutationHomotopy_reverse_add_eq: the homotopy equation ∂~' ∘ H~' + H~' ∘ ∂~' = 1 + Φ~ ∘ Ψ~ on the commuted diagram.

References

Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Sections 4.4 and 5.1, and Manolescu--Ozsváth--Szabó--Thurston, On combinatorial link Floer homology, Section 3.1 (arXiv:math/0610559). The construction reduces the existing GridDiagram.commutationHomotopy modulo the variables, as GridDiagram.fullyBlockedCommutationMap reduces the pentagon map.

noncomputable def TauCeti.GridDiagram.fullyBlockedCommutationHomotopy {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) : GridChain R n →ₗ[R] GridChain R n

The fully blocked commutation homotopy: its matrix entries are the constant coefficients of the hexagon coefficients of the commutation homotopy. It counts the empty hexagons carrying neither X- nor O-markings, over any commutative coefficient semiring.

theorem TauCeti.GridDiagram.fullyBlockedCommutationHomotopy_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) (r : R) : ((G.fullyBlockedCommutationHomotopy R C) (Finsupp.single x r)) y = r * MvPolynomial.constantCoeff (G.commutationHexagonCoefficient R C x y)

On a single generator, the fully blocked homotopy reads the constant hexagon coefficient.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedCommutationHomotopy_mapRange_constantCoeff {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChainMinus R n) : (G.fullyBlockedCommutationHomotopy R C) (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ c) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ ((G.commutationHomotopy R C) c)

Taking constant coefficients commutes with the commutation homotopy.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_fullyBlockedCommutationHomotopy_add_eq {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (c : GridChain (ZMod 2) n) : G.fullyBlockedDifferential ((G.fullyBlockedCommutationHomotopy (ZMod 2) C) c) + (G.fullyBlockedCommutationHomotopy (ZMod 2) C) (G.fullyBlockedDifferential c) = c + ((swapColumns C.column ((finRotate n) C.column) G).fullyBlockedCommutationMap (ZMod 2) C.reverse) ((G.fullyBlockedCommutationMap (ZMod 2) C) c)

The fully blocked homotopy equation. The fully blocked hexagon map H~ is a chain homotopy between the identity of GC~(G) and the round trip Ψ~ ∘ Φ~ through the commuted diagram: ∂~ ∘ H~ + H~ ∘ ∂~ = 1 + Ψ~ ∘ Φ~.

theorem TauCeti.GridDiagram.fullyBlockedDifferential_fullyBlockedCommutationHomotopy_reverse_add_eq {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) (c : GridChain (ZMod 2) n) : (swapColumns C.column ((finRotate n) C.column) G).fullyBlockedDifferential (((swapColumns C.column ((finRotate n) C.column) G).fullyBlockedCommutationHomotopy (ZMod 2) C.reverse) c) + ((swapColumns C.column ((finRotate n) C.column) G).fullyBlockedCommutationHomotopy (ZMod 2) C.reverse) ((swapColumns C.column ((finRotate n) C.column) G).fullyBlockedDifferential c) = c + (G.fullyBlockedCommutationMap (ZMod 2) C) (((swapColumns C.column ((finRotate n) C.column) G).fullyBlockedCommutationMap (ZMod 2) C.reverse) c)

The fully blocked homotopy equation on the commuted diagram. The fully blocked hexagon map H~' of the reverse commutation is a chain homotopy between the identity of GC~(G') and the round trip Φ~ ∘ Ψ~ through G: ∂~' ∘ H~' + H~' ∘ ∂~' = 1 + Φ~ ∘ Ψ~.