Documentation

TauCeti.KnotTheory.Grid.Commutation.FullyBlocked

The fully blocked commutation chain map #

Setting every marking variable to zero in the pentagon-counting map retains exactly the empty pentagons avoiding both kinds of markings. Both terminal-side and initial-side pentagons contribute. The resulting map is linear over the coefficient semiring: the variable permutation in the unblocked map disappears under constant coefficients.

GridDiagram.fullyBlockedCommutationMap_mapRange_constantCoeff expresses this specialization on arbitrary chains. Over ZMod 2, GridDiagram.fullyBlockedCommutationMap_comp_fullyBlockedDifferential proves that it is a chain map between the fully blocked complexes, and GridDiagram.fullyBlockedCommutationMap_reverse_comp_fullyBlockedDifferential does the same for the reverse commutation. The hexagon homotopies relating the two maps are in TauCeti.KnotTheory.Grid.Commutation.Homotopy.FullyBlocked.

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).

source
@[simp]
theorem TauCeti.GridDiagram.constantCoeff_pentagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) {x y : GridState n} (P : GridPentagonBetween C.column C.turnRow x y) :
MvPolynomial.constantCoeff (G.pentagonWeight R C.toColumnTurn P) = if G.pentagonOColumns C.toColumnTurn P = ∅ then 1 else 0

A terminal-side pentagon contributes a constant term precisely when it covers no O-marking. Its X-avoidance is imposed separately by membership in pentagons.

source
@[simp]
theorem TauCeti.GridDiagram.constantCoeff_initialPentagonWeight {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) {x y : GridState n} (P : GridInitialPentagonBetween C.column C.turnRow x y) :
MvPolynomial.constantCoeff (G.initialPentagonWeight R C.toColumnTurn P) = if G.OColumnsOfSquares P.coveredSquares = ∅ then 1 else 0

An initial-side pentagon contributes a constant term precisely when it covers no O-marking.

source
@[simp]
theorem TauCeti.GridDiagram.constantCoeff_commutationPentagonCoefficient {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) :
MvPolynomial.constantCoeff (G.commutationPentagonCoefficient R C.toColumnTurn x y) = ↑{P ∈ G.pentagons C.toColumnTurn x y | G.pentagonOColumns C.toColumnTurn P = ∅}.card + ↑{P ∈ G.initialPentagons C.toColumnTurn x y | G.OColumnsOfSquares P.coveredSquares = ∅}.card

The constant coefficient counts the pentagons of both kinds which also avoid every O-marking. The counted sets already impose emptiness and avoidance of all X-markings.

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

The fully blocked commutation map: its matrix entries are the constant coefficients of the unblocked pentagon coefficients. It counts empty pentagons carrying neither X nor O markings, over any commutative coefficient semiring.

Instances For
    source
    theorem TauCeti.GridDiagram.fullyBlockedCommutationMap_single_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (x y : GridState n) (r : R) :
    ((G.fullyBlockedCommutationMap R C) (Finsupp.single x r)) y = r * MvPolynomial.constantCoeff (G.commutationPentagonCoefficient R C.toColumnTurn x y)

    On a single generator, the fully blocked map reads the constant pentagon coefficient.

    source
    @[simp]
    theorem TauCeti.GridDiagram.fullyBlockedCommutationMap_apply_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChain R n) (y : GridState n) :
    ((G.fullyBlockedCommutationMap R C) c) y = Finsupp.sum c fun (x : GridState n) (r : R) => r * MvPolynomial.constantCoeff (G.commutationPentagonCoefficient R C.toColumnTurn x y)

    On an arbitrary chain, the fully blocked map multiplies by the matrix of constant pentagon coefficients.

    source
    @[simp]
    theorem TauCeti.GridDiagram.fullyBlockedCommutationMap_mapRange_constantCoeff {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] (C : G.ColumnCommutationData) (c : GridChainMinus R n) :
    (G.fullyBlockedCommutationMap R C) (Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ c) = Finsupp.mapRange ⇑MvPolynomial.constantCoeff ⋯ ((G.commutationMap R C.toColumnTurn) c)

    Taking constant coefficients commutes with the commutation map. In particular, the semilinear variable swap of the unblocked map becomes an ordinary linear map after blocking.

    source
    theorem TauCeti.GridDiagram.fullyBlockedCommutationMap_comp_fullyBlockedDifferential {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) :
    G.fullyBlockedCommutationMap (ZMod 2) C ∘ₗ G.fullyBlockedDifferential = (swapColumns C.column ((finRotate n) C.column) G).fullyBlockedDifferential ∘ₗ G.fullyBlockedCommutationMap (ZMod 2) C

    The pentagon map after blocking all marking variables intertwines the fully blocked differentials.

    source
    theorem TauCeti.GridDiagram.fullyBlockedCommutationMap_reverse_comp_fullyBlockedDifferential {n : ℕ} (G : GridDiagram n) (C : G.ColumnCommutationData) :
    (swapColumns C.column ((finRotate n) C.column) G).fullyBlockedCommutationMap (ZMod 2) C.reverse ∘ₗ (swapColumns C.column ((finRotate n) C.column) G).fullyBlockedDifferential = G.fullyBlockedDifferential ∘ₗ (swapColumns C.column ((finRotate n) C.column) G).fullyBlockedCommutationMap (ZMod 2) C.reverse

    The fully blocked pentagon map of the reverse commutation intertwines the fully blocked differentials of the commuted diagram and of G.