An explicit basis for small-grid homology

The fully blocked differential vanishes on grids of size at most two. Consequently every grid state gives a cycle, no nonzero cycle is a boundary, and the corresponding homology classes form a basis. This file makes those generators explicit.

For a grid diagram G of size n ≤ 2, fullyBlockedCycleOfLeTwo G hn x is the cycle represented by the single grid state x, and fullyBlockedHomologyClassOfLeTwo G hn x is its homology class. The basis fullyBlockedHomologyBasisOfLeTwo G hn consists of exactly these classes. Its coordinate formula identifies the coefficient of a class at x with the coefficient of any cycle representative at x.

At size two, the basis has the two states GridState.twoByTwoId and GridState.twoByTwoSwap. For the standard two-by-two unknot diagram their already-computed (M_O, A) bigradings are (-1, -1) and (0, 0), respectively (maslovOℤ_twoByTwo_twoByTwoId, alexander_twoByTwo_twoByTwoId, maslovOℤ_twoByTwo_twoByTwoSwap, and alexander_twoByTwo_twoByTwoSwap). Thus the basis here turns the separate dimension and grading calculations into an explicit computation of the fully blocked homology.

Main definitions

• TauCeti.GridDiagram.fullyBlockedCycleOfLeTwo: the cycle supported on one grid state.
• TauCeti.GridDiagram.fullyBlockedHomologyClassOfLeTwo: its homology class.
• TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo: the basis of small-grid homology indexed by grid states.

Main results

• TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo_apply: every basis vector is the homology class of its indexing state.
• TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo_repr_mk: the coordinates of a homology class are the coefficients of any cycle representative.
• TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo_repr_class: a single-state class has the corresponding singleton coordinate vector.
• TauCeti.GridDiagram.fullyBlockedHomologyClassOfLeTwo_ne_zero and TauCeti.GridDiagram.fullyBlockedHomologyClassOfLeTwo_injective: the state classes are nonzero and pairwise distinct.

References

This advances the “Grid homology computes” acceptance criterion in TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, specifically the computation of the two-by-two unknot grid with its bigradings and the visible rank-two stabilization factor. The fully blocked complex and its grading conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 3 and 4.

noncomputable def TauCeti.GridDiagram.fullyBlockedCycleOfLeTwo {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : ↥G.fullyBlockedCycles

The fully blocked cycle supported on a single grid state when the grid size is at most two.

The size hypothesis makes the fully blocked differential zero, so the singleton chain is a cycle.

Equations

• G.fullyBlockedCycleOfLeTwo hn x = ⟨Finsupp.single x 1, ⋯⟩

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedCycleOfLeTwo_coe {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : ↑(G.fullyBlockedCycleOfLeTwo hn x) = Finsupp.single x 1

The chain underlying the small-grid cycle supported on x is the singleton chain at x.

noncomputable def TauCeti.GridDiagram.fullyBlockedHomologyClassOfLeTwo {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : G.fullyBlockedHomology

The fully blocked homology class represented by a single grid state in size at most two.

Equations

• G.fullyBlockedHomologyClassOfLeTwo hn x = Submodule.Quotient.mk (G.fullyBlockedCycleOfLeTwo hn x)

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedHomologyEquivChainOfLeTwo_class {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : (G.fullyBlockedHomologyEquivChainOfLeTwo hn) (G.fullyBlockedHomologyClassOfLeTwo hn x) = Finsupp.single x 1

Under the small-grid equivalence from homology to the chain module, the class represented by x becomes the singleton chain at x.

noncomputable def TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : Module.Basis (GridState n) (ZMod 2) G.fullyBlockedHomology

The basis of fully blocked homology in grid size at most two, indexed by grid states.

It is obtained by transporting the standard singleton basis of the grid chain module through the inverse of fullyBlockedHomologyEquivChainOfLeTwo.

Equations

• G.fullyBlockedHomologyBasisOfLeTwo hn = Finsupp.basisSingleOne.map (G.fullyBlockedHomologyEquivChainOfLeTwo hn).symm

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo_apply {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : (G.fullyBlockedHomologyBasisOfLeTwo hn) x = G.fullyBlockedHomologyClassOfLeTwo hn x

A vector of the small-grid homology basis is the class represented by its indexing grid state.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo_repr_mk {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (c : ↥G.fullyBlockedCycles) : (G.fullyBlockedHomologyBasisOfLeTwo hn).repr (Submodule.Quotient.mk c) = ↑c

The coordinates of the class of a small-grid cycle are its chain coefficients.

Since the differential and the boundary submodule both vanish, passing to homology does not change any coefficient.

@[simp]

theorem TauCeti.GridDiagram.fullyBlockedHomologyBasisOfLeTwo_repr_class {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : (G.fullyBlockedHomologyBasisOfLeTwo hn).repr (G.fullyBlockedHomologyClassOfLeTwo hn x) = Finsupp.single x 1

The coordinate vector of the homology class represented by x is the singleton vector at x.

theorem TauCeti.GridDiagram.fullyBlockedHomologyClassOfLeTwo_ne_zero {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) (x : GridState n) : G.fullyBlockedHomologyClassOfLeTwo hn x ≠ 0

Each single-state homology class is nonzero in grid size at most two.

theorem TauCeti.GridDiagram.fullyBlockedHomologyClassOfLeTwo_injective {n : ℕ} (G : GridDiagram n) (hn : n ≤ 2) : Function.Injective (G.fullyBlockedHomologyClassOfLeTwo hn)

Distinct grid states determine distinct fully blocked homology classes in size at most two.