Grid differentials as homological complexes

This file packages the three grid chain modules and their square-zero differentials as homological complexes in Mathlib's sense. Each uses the one-object circular shape ComplexShape.refl Unit: its sole object is the total chain module and its sole differential is the corresponding grid differential. This is the ungraded complex underlying the separate bigraded decompositions of the fully blocked and unblocked chain modules.

The one-object form retains exactly the algebra needed for cycles, boundaries, chain maps, and homology while applying to every grid diagram. In particular it does not require the odd-component hypothesis used to make the Alexander grading integral. Later graded constructions can refine these complexes by restricting the differential to their homogeneous pieces. Here simplyBlockedComplex denotes the algebraic specialization obtained by setting one selected O-variable to zero. This has the standard simply blocked interpretation for knot grids; for a multi-component link, that interpretation instead requires one blocked O-marking on each component.

The fully blocked complex is over ZMod 2. The unblocked complex and the one-variable specialization are defined over an arbitrary commutative coefficient ring of characteristic two. Their coefficient rings are, respectively, the polynomial ring on all columns and the polynomial ring on the columns other than the selected blocked column.

Main definitions

• TauCeti.GridDiagram.fullyBlockedComplex: the fully blocked grid complex.
• TauCeti.GridDiagram.unblockedComplex: the unblocked grid complex GC⁻.
• TauCeti.GridDiagram.simplyBlockedComplex: the one-variable specialization obtained by setting one selected O-variable to zero.

References

The three grid complexes and their coefficient conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3--4.

Fully blocked complex

noncomputable def TauCeti.GridDiagram.fullyBlockedComplex {n : ℕ} (G : GridDiagram n) : HomologicalComplex (ModuleCat (ZMod 2)) (ComplexShape.refl Unit)

The fully blocked grid chain module and differential as a one-object homological complex over ZMod 2.

The unique differential counts empty rectangles avoiding every marking and squares to zero.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedComplex_X {n : ℕ} (G : GridDiagram n) (i : Unit) : G.fullyBlockedComplex.X i = ↧(GridChain (ZMod 2) n)

The unique object of the fully blocked complex is the fully blocked grid chain module.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedComplex_d {n : ℕ} (G : GridDiagram n) : G.fullyBlockedComplex.d () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom G.fullyBlockedDifferential) (CategoryTheory.eqToHom ⋯))

The unique differential of the fully blocked complex is the fully blocked grid differential.

Unblocked complex

noncomputable def 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 grid chain module GC⁻ and its differential as a one-object homological complex over the polynomial ring R[V₀, ..., V_{n-1}].

The unique differential counts empty rectangles avoiding the X-markings and weights each rectangle by the monomial of the O-markings it covers.

@[simp]

theorem TauCeti.GridDiagram.unblockedComplex_X {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Unit) : (G.unblockedComplex R).X i = ↧(GridChainMinus R n)

The unique object of the unblocked complex is the unblocked grid chain module.

@[simp]

theorem TauCeti.GridDiagram.unblockedComplex_d {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] : (G.unblockedComplex R).d () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.unblockedDifferential R)) (CategoryTheory.eqToHom ⋯))

The unique differential of the unblocked complex is the unblocked grid differential.

One-variable specialization

noncomputable def TauCeti.GridDiagram.simplyBlockedComplex {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Fin n) : HomologicalComplex (ModuleCat (MvPolynomial { c : Fin n // c ≠ i } R)) (ComplexShape.refl Unit)

The one-variable specialization of the grid chain module and differential as a one-object homological complex over the polynomial ring on the columns other than i.

The unique differential is obtained from the unblocked differential by setting the selected variable V_i to zero. For a knot grid this is the standard simply blocked complex; for a link, the standard simply blocked theory sets one variable on each component to zero.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedComplex_X {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Fin n) (j : Unit) : (G.simplyBlockedComplex R i).X j = ↧(GridChainHat R n i)

The unique object of the one-variable specialization is its specialized grid chain module.

@[simp]

theorem TauCeti.GridDiagram.simplyBlockedComplex_d {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Fin n) : (G.simplyBlockedComplex R i).d () () = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (G.simplyBlockedDifferential R i)) (CategoryTheory.eqToHom ⋯))

The unique differential of the one-variable specialization is its specialized grid differential.

noncomputable def TauCeti.GridDiagram.simplyBlockedChainEquiv {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Fin n) : ↑((G.simplyBlockedComplex R i).X ()) ≃ₗ[MvPolynomial { c : Fin n // c ≠ i } R] GridChainHat R n i

Identify the object of the specialized complex with its explicit chain module.

theorem TauCeti.GridDiagram.simplyBlockedChainEquiv_d {n : ℕ} (G : GridDiagram n) (R : Type u_1) [CommRing R] [CharP R 2] (i : Fin n) (c : ↑((G.simplyBlockedComplex R i).X ())) : (G.simplyBlockedChainEquiv R i) ((CategoryTheory.ConcreteCategory.hom ((G.simplyBlockedComplex R i).d () ())) c) = (G.simplyBlockedDifferential R i) ((G.simplyBlockedChainEquiv R i) c)

The explicit chain identification intertwines the categorical and grid differentials.