Unblocked grid homology as a module over R[U]

The unblocked grid homology GH⁻(G) of a grid diagram G of size n is the homology of the unblocked complex GC⁻(G), a module over R[V₀, …, V_{n-1}] (unblockedHomology). The X-marking homotopies show that two variables V_c, V_{c'} whose columns lie on the same link component act identically on it (X_smul_unblockedHomology_eq_of_sameCycle). Consequently every polynomial acts on GH⁻(G) as does its image under any renaming of the variables that keeps each column on its component (smul_unblockedHomology_eq_rename_smul).

For a knot grid all variables lie on one component, so the action of R[V₀, …, V_{n-1}] factors through the evaluation π : R[V₀, …, V_{n-1}] → R[U] sending every V_c to U: GH⁻(G) is annihilated by the kernel of π (IsKnot.isTorsionBySet_unblockedHomology). Since π is surjective, this makes GH⁻(G) a module over R[U] (IsKnot.unblockedHomologyModule), with π p acting as p (IsKnot.aeval_smul_unblockedHomology) and in particular U acting as any one of the variables V_c (IsKnot.X_smul_unblockedHomology). The construction involves no choice of a distinguished column. This is the 𝔽[U]-module structure on the grid homology of a knot through which the concordance invariant τ is defined.

Concretely, GH⁻(G) is the quotient ker ∂⁻ ⧸ im ∂⁻ of the cycles of GC⁻(G) by the boundaries (unblockedHomologyIso), so every class is the class of a cycle (unblockedHomologyClass), and a cycle has zero class exactly when it is a boundary. Structure on GC⁻(G) that the differential respects, such as the Alexander grading, descends to this quotient.

Main definitions

• TauCeti.GridDiagram.unblockedHomology: the unblocked grid homology GH⁻.
• TauCeti.GridDiagram.unblockedHomologyBaseModule: the coefficient-ring action obtained by restricting the polynomial action.
• TauCeti.GridDiagram.unblockedHomologyIso: GH⁻ is ker ∂⁻ ⧸ im ∂⁻.
• TauCeti.GridDiagram.unblockedHomologyClass: the class in GH⁻ of a cycle.
• TauCeti.GridDiagram.unblockedHomologyEquivOfIntertwining: the equivalence of unblocked grid homologies induced by a semilinear equivalence intertwining the differentials.
• TauCeti.GridDiagram.IsKnot.unblockedHomologyModule: the R[U]-module structure on the unblocked grid homology of a knot grid.

Main results

• TauCeti.GridDiagram.X_smul_unblockedHomology_eq_of_sameCycle: variables on the same component act identically on GH⁻.
• TauCeti.GridDiagram.smul_unblockedHomology_eq_rename_smul: renaming the variables within components does not change the action of a polynomial on GH⁻.
• TauCeti.GridDiagram.unblockedHomologyClass_surjective and TauCeti.GridDiagram.unblockedHomologyClass_eq_zero_iff: every class is the class of a cycle, and a cycle has zero class exactly when it is a boundary.
• TauCeti.GridDiagram.unblockedHomologyEquivOfIntertwining_unblockedHomologyClass: the equivalence induced by an intertwining map sends the class of a cycle z to the class of its image.
• TauCeti.GridDiagram.IsKnot.isTorsionBySet_unblockedHomology: for a knot grid, GH⁻ is annihilated by the kernel of R[V₀, …, V_{n-1}] → R[U].
• TauCeti.GridDiagram.IsKnot.aeval_smul_unblockedHomology and TauCeti.GridDiagram.IsKnot.X_smul_unblockedHomology: the action of R[U] on GH⁻ of a knot grid.
• TauCeti.GridDiagram.IsKnot.isScalarTower_unblockedHomology: the coefficient action agrees with the R[U]-module structure.

References

This is Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Section 4.6: by Lemma 4.6.9 the variables of a knot grid act identically on GH⁻, which is thereby regarded as a module over 𝔽[U].

@[reducible, inline]

noncomputable abbrev TauCeti.GridDiagram.unblockedHomology {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : ModuleCat (MvPolynomial (Fin n) R)

The unblocked grid homology GH⁻(G): the homology of the unblocked grid complex, a module over the polynomial ring R[V₀, …, V_{n-1}].

@[instance_reducible]

noncomputable instance TauCeti.GridDiagram.unblockedHomologyBaseModule {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : Module R ↑(G.unblockedHomology R)

Restriction of the polynomial action on grid homology along the coefficient embedding.

instance TauCeti.GridDiagram.unblockedHomologyBaseScalarTower {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : IsScalarTower R (MvPolynomial (Fin n) R) ↑(G.unblockedHomology R)

The coefficient action on grid homology agrees with the polynomial action through the coefficient embedding.

theorem TauCeti.GridDiagram.X_smul_unblockedHomology_eq_of_sameCycle {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] {c c' : Fin n} (h : G.componentPerm.SameCycle c c') (x : ↑(G.unblockedHomology R)) : MvPolynomial.X c • x = MvPolynomial.X c' • x

Two variables whose columns lie on the same link component act identically on the unblocked grid homology.

theorem TauCeti.GridDiagram.smul_unblockedHomology_eq_rename_smul {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (f : Fin n → Fin n) (hf : ∀ (c : Fin n), G.componentPerm.SameCycle c (f c)) (p : MvPolynomial (Fin n) R) (x : ↑(G.unblockedHomology R)) : p • x = (MvPolynomial.rename f) p • x

Every polynomial acts on the unblocked grid homology as its image under a renaming of the variables that keeps each column on its link component.

Cycles and boundaries

@[reducible, inline]

noncomputable abbrev TauCeti.GridDiagram.unblockedComplex' {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : HomologicalComplex (ModuleCat (MvPolynomial (Fin n) R)) (ComplexShape.refl Unit)

The unblocked complex with its unique object and differential spelled out, so that its homology is the homology of the unblocked grid differential in the sense of LinearMap.homology.

noncomputable def TauCeti.GridDiagram.unblockedComplexIso {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : G.unblockedComplex R ≅ G.unblockedComplex' R

The unblocked complex is isomorphic to its spelled-out form unblockedComplex'.

@[simp]

theorem TauCeti.GridDiagram.unblockedComplexIso_hom_f {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Unit) : (G.unblockedComplexIso R).hom.f i = CategoryTheory.eqToHom ⋯

The components of unblockedComplexIso are the identifications unblockedComplex_X of the unique object.

noncomputable def TauCeti.GridDiagram.unblockedHomologyIso {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : G.unblockedHomology R ≅ ↧((G.unblockedDifferential R).homology ⋯)

The unblocked grid homology GH⁻ is the homology ker ∂⁻ ⧸ im ∂⁻ of the unblocked grid differential: the cycles of GC⁻ modulo the boundaries.

noncomputable def TauCeti.GridDiagram.unblockedHomologyClass {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : ↥(G.unblockedDifferential R).ker →ₗ[MvPolynomial (Fin n) R] ↑(G.unblockedHomology R)

The linear map sending a cycle of GC⁻ to its class in GH⁻.

@[simp]

theorem TauCeti.GridDiagram.unblockedHomologyIso_hom_unblockedHomologyClass {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (z : ↥(G.unblockedDifferential R).ker) : (CategoryTheory.ConcreteCategory.hom (G.unblockedHomologyIso R).hom) ((G.unblockedHomologyClass R) z) = ((G.unblockedDifferential R).homologyπ ⋯) z

Under unblockedHomologyIso, the class of a cycle is its class modulo the boundaries.

theorem TauCeti.GridDiagram.unblockedHomologyClass_surjective {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : Function.Surjective ⇑(G.unblockedHomologyClass R)

Every class in GH⁻ is represented by a cycle.

@[simp]

theorem TauCeti.GridDiagram.unblockedHomologyClass_eq_zero_iff {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (z : ↥(G.unblockedDifferential R).ker) : (G.unblockedHomologyClass R) z = 0 ↔ ↑z ∈ (G.unblockedDifferential R).range

A cycle represents zero in GH⁻ exactly when it is a boundary.

The equivalence induced by an intertwining map

theorem TauCeti.GridDiagram.map_mem_ker_unblockedDifferential_of_intertwining {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] (G' : GridDiagram n) {σ σ' : MvPolynomial (Fin n) R →+* MvPolynomial (Fin n) R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : GridChainMinus R n ≃ₛₗ[σ] GridChainMinus R n) (he : ∀ (c : GridChainMinus R n), (G'.unblockedDifferential R) (e c) = e ((G.unblockedDifferential R) c)) {c : GridChainMinus R n} (hc : c ∈ (G.unblockedDifferential R).ker) : e c ∈ (G'.unblockedDifferential R).ker

A map intertwining two unblocked differentials sends cycles to cycles.

noncomputable def TauCeti.GridDiagram.unblockedHomologyEquivOfIntertwining {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (G' : GridDiagram n) {σ σ' : MvPolynomial (Fin n) R →+* MvPolynomial (Fin n) R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : GridChainMinus R n ≃ₛₗ[σ] GridChainMinus R n) (he : ∀ (c : GridChainMinus R n), (G'.unblockedDifferential R) (e c) = e ((G.unblockedDifferential R) c)) : ↑(G.unblockedHomology R) ≃ₛₗ[σ] ↑(G'.unblockedHomology R)

The equivalence of unblocked grid homologies induced by an intertwining map. A semilinear equivalence e of chain modules with ∂⁻' ∘ e = e ∘ ∂⁻ induces a semilinear equivalence GH⁻(G) ≃ GH⁻(G'), sending the class of a cycle z to the class of e z.

@[simp]

theorem TauCeti.GridDiagram.unblockedHomologyEquivOfIntertwining_unblockedHomologyClass {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (G' : GridDiagram n) {σ σ' : MvPolynomial (Fin n) R →+* MvPolynomial (Fin n) R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (e : GridChainMinus R n ≃ₛₗ[σ] GridChainMinus R n) (he : ∀ (c : GridChainMinus R n), (G'.unblockedDifferential R) (e c) = e ((G.unblockedDifferential R) c)) (z : ↥(G.unblockedDifferential R).ker) : (G.unblockedHomologyEquivOfIntertwining R G' e he) ((G.unblockedHomologyClass R) z) = (G'.unblockedHomologyClass R) ⟨e ↑z, ⋯⟩

unblockedHomologyEquivOfIntertwining sends the class of a cycle z to the class of its image.

theorem TauCeti.GridDiagram.IsKnot.isTorsionBySet_unblockedHomology {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) : Module.IsTorsionBySet (MvPolynomial (Fin n) R) ↑(G.unblockedHomology R) ↑(RingHom.ker (MvPolynomial.aeval fun (x : Fin n) => Polynomial.X))

On a knot grid the unblocked grid homology is annihilated by the kernel of the evaluation R[V₀, …, V_{n-1}] → R[U] sending every variable to U.

@[instance_reducible]

noncomputable def TauCeti.GridDiagram.IsKnot.unblockedHomologyModule {n : ℕ} {G : GridDiagram n} (R : Type u_1) [CommRing R] [CharP R 2] (hG : G.IsKnot) : Module (Polynomial R) ↑(G.unblockedHomology R)

The R[U]-module structure on the unblocked grid homology of a knot grid: a polynomial q acts as any p ∈ R[V₀, …, V_{n-1}] with p(U, …, U) = q, so U acts as each variable V_c.

@[simp]

theorem TauCeti.GridDiagram.IsKnot.aeval_smul_unblockedHomology {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) (p : MvPolynomial (Fin n) R) (x : ↑(G.unblockedHomology R)) : (MvPolynomial.aeval fun (x : Fin n) => Polynomial.X) p • x = p • x

On a knot grid, the evaluation p(U, …, U) of a polynomial acts on the unblocked grid homology as p does.

theorem TauCeti.GridDiagram.IsKnot.X_smul_unblockedHomology {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) (c : Fin n) (x : ↑(G.unblockedHomology R)) : Polynomial.X • x = MvPolynomial.X c • x

On a knot grid, U acts on the unblocked grid homology as each variable V_c.

theorem TauCeti.GridDiagram.IsKnot.isScalarTower_unblockedHomology {n : ℕ} {G : GridDiagram n} {R : Type u_1} [CommRing R] [CharP R 2] (hG : G.IsKnot) : IsScalarTower R (Polynomial R) ↑(G.unblockedHomology R)

The coefficient action on knot grid homology agrees with the constant polynomials in the R[U]-module structure.