Documentation

TauCeti.KnotTheory.Grid.XHomotopy.Complex

Multiplication by the grid variables is homotopic along a link component #

Let X_k be the X-marking of column k of a grid diagram, and let O_j be the O-marking in the row of X_k. In characteristic two, the X-marking homotopy H_k satisfies

∂⁻ ∘ H_k + H_k ∘ ∂⁻ = V_k + V_j

on the unblocked grid complex GC⁻ (unblockedDifferential_comp_XHomotopy_add_XHomotopy_comp): the off-diagonal matrix entries cancel in pairs and each diagonal entry is the sum of the weights of the two thin annuli through X_k. Hence multiplication by V_k and multiplication by V_j are chain homotopic (unblockedComplexXHomotopy), and so induce the same map on homology.

Walking from O_j along its row to X_k and then along column k to O_k is one step of the component permutation, so k = componentPerm j. Consequently the multiplications by any two variables belonging to the same link component are chain homotopic (nonempty_homotopy_X_smul_of_pow_componentPerm_apply) and act identically on the homology of GC⁻ (homologyMap_X_smul_eq_of_pow_componentPerm_apply). For a knot grid there is a single component, so the action of V_c on the homology of GC⁻ is independent of the choice of c (IsKnot.homologyMap_X_smul_eq).

Main definitions #

Main results #

References #

This is Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Lemma 4.6.9 and its consequence that the variables of one component act identically on unblocked grid homology.

source
theorem TauCeti.GridDiagram.sum_unblockedCoefficient_mul_XHomotopyCoefficient_add {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (k : Fin n) (x z : GridState n) :
∑ y : GridState n, (G.unblockedCoefficient R x y * G.XHomotopyCoefficient R k y z + G.XHomotopyCoefficient R k x y * G.unblockedCoefficient R y z) = if x = z then MvPolynomial.X k + MvPolynomial.X (G.O.transpose.toPerm (G.X.toPerm k)) else 0

In characteristic two the matrix entries of ∂⁻ ∘ H_k + H_k ∘ ∂⁻ vanish off the diagonal and equal V_k + V_j on it, where O_j is the O-marking in the row of X_k.

source
theorem TauCeti.GridDiagram.unblockedDifferential_comp_XHomotopy_add_XHomotopy_comp {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] (k : Fin n) :
G.unblockedDifferential R ∘ₗ G.XHomotopy R k + G.XHomotopy R k ∘ₗ G.unblockedDifferential R = (MvPolynomial.X k + MvPolynomial.X (G.O.transpose.toPerm (G.X.toPerm k))) • LinearMap.id

The homotopy identity ∂⁻ ∘ H_k + H_k ∘ ∂⁻ = V_k + V_j on the unblocked grid complex in characteristic two, where O_j is the O-marking in the row of X_k.

source
theorem TauCeti.GridDiagram.exists_unblockedDifferential_comp_add_comp_eq_of_pow_componentPerm_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommSemiring R] [CharP R 2] {c c' : Fin n} (i : ℕ) (h : (G.componentPerm ^ i) c = c') :
∃ (H : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n), G.unblockedDifferential R ∘ₗ H + H ∘ₗ G.unblockedDifferential R = (MvPolynomial.X c + MvPolynomial.X c') • LinearMap.id

The variables of two columns on one link component are chain homotopic on GC⁻: there is a map H with ∂⁻ H + H ∂⁻ = V_c + V_c', a sum of X-marking homotopies.

source
theorem TauCeti.GridDiagram.IsKnot.exists_unblockedDifferential_comp_add_comp_eq {n : ℕ} (R : Type u_1) [CommSemiring R] [CharP R 2] {G : GridDiagram n} (hG : G.IsKnot) (c c' : Fin n) :
∃ (H : GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n), G.unblockedDifferential R ∘ₗ H + H ∘ₗ G.unblockedDifferential R = (MvPolynomial.X c + MvPolynomial.X c') • LinearMap.id

On a knot grid, multiplication by V_c + V_c' is null-homotopic on GC⁻ for any two columns c and c'.

source
noncomputable def TauCeti.GridDiagram.IsKnot.XSmulHomotopy {n : ℕ} (R : Type u_1) [CommSemiring R] [CharP R 2] {G : GridDiagram n} (hG : G.IsKnot) (c c' : Fin n) :
GridChainMinus R n →ₗ[MvPolynomial (Fin n) R] GridChainMinus R n

On a knot grid, a chosen map H on GC⁻ with ∂⁻ H + H ∂⁻ = V_c + V_c', a null-homotopy of multiplication by V_c + V_c' (IsKnot.unblockedDifferential_comp_XSmulHomotopy_add_XSmulHomotopy_comp).

Instances For
    source
    theorem TauCeti.GridDiagram.IsKnot.unblockedDifferential_comp_XSmulHomotopy_add_XSmulHomotopy_comp {n : ℕ} (R : Type u_1) [CommSemiring R] [CharP R 2] {G : GridDiagram n} (hG : G.IsKnot) (c c' : Fin n) :
    G.unblockedDifferential R ∘ₗ XSmulHomotopy R hG c c' + XSmulHomotopy R hG c c' ∘ₗ G.unblockedDifferential R = (MvPolynomial.X c + MvPolynomial.X c') • LinearMap.id

    The homotopy identity ∂⁻ H + H ∂⁻ = V_c + V_c' for H = hG.XSmulHomotopy R c c'.

    Chain homotopies #

    source
    noncomputable def TauCeti.GridDiagram.unblockedComplexXHomotopy {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (k : Fin n) :
    Homotopy (MvPolynomial.X k • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) (MvPolynomial.X (G.O.transpose.toPerm (G.X.toPerm k)) • CategoryTheory.CategoryStruct.id (G.unblockedComplex R))

    The X-marking homotopy H_k as a chain homotopy on the unblocked grid complex, from multiplication by V_k to multiplication by V_j, where O_j is the O-marking in the row of X_k.

    Instances For
      source
      noncomputable def TauCeti.GridDiagram.unblockedComplexComponentHomotopy {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (c : Fin n) :
      Homotopy (MvPolynomial.X (G.componentPerm c) • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) (MvPolynomial.X c • CategoryTheory.CategoryStruct.id (G.unblockedComplex R))

      The chain homotopy from multiplication by V_{componentPerm c} to multiplication by V_c: the two O-markings are consecutive on a link component.

      Instances For
        source
        theorem TauCeti.GridDiagram.nonempty_homotopy_X_smul_of_pow_componentPerm_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] {c c' : Fin n} (i : ℕ) (h : (G.componentPerm ^ i) c = c') :
        Nonempty (Homotopy (MvPolynomial.X c • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) (MvPolynomial.X c' • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)))

        Multiplication by the variables of two columns on the same link component is chain homotopic on the unblocked grid complex.

        source
        theorem TauCeti.GridDiagram.homologyMap_X_smul_eq_of_pow_componentPerm_apply {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] {c c' : Fin n} (i : ℕ) (h : (G.componentPerm ^ i) c = c') :
        HomologicalComplex.homologyMap (MvPolynomial.X c • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) () = HomologicalComplex.homologyMap (MvPolynomial.X c' • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) ()

        The variables of two columns on the same link component act identically on the homology of the unblocked grid complex.

        source
        theorem TauCeti.GridDiagram.IsKnot.nonempty_homotopy_X_smul {n : ℕ} (R : Type u_1) [CommRing R] [CharP R 2] {G : GridDiagram n} (hG : G.IsKnot) (c c' : Fin n) :
        Nonempty (Homotopy (MvPolynomial.X c • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) (MvPolynomial.X c' • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)))

        On a knot grid, multiplication by any two variables is chain homotopic on the unblocked grid complex.

        source
        theorem TauCeti.GridDiagram.IsKnot.homologyMap_X_smul_eq {n : ℕ} (R : Type u_1) [CommRing R] [CharP R 2] {G : GridDiagram n} (hG : G.IsKnot) (c c' : Fin n) :
        HomologicalComplex.homologyMap (MvPolynomial.X c • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) () = HomologicalComplex.homologyMap (MvPolynomial.X c' • CategoryTheory.CategoryStruct.id (G.unblockedComplex R)) ()

        On a knot grid, all the variables V_c act identically on the homology of the unblocked grid complex.