The Euler characteristic of fully blocked grid homology

The fully blocked grid differential preserves the Alexander grading and lowers the Maslov grading. For a fixed Alexander degree, this file regards its graded complex as a bounded complex of finite-dimensional ZMod 2-vector spaces. Reindexing Maslov degree m as cohomological degree -m puts the complex in the cochain convention used by the finite-dimensional Euler--Poincaré theorem.

The resulting homology Euler characteristic agrees with the alternating count of grid states in each Alexander degree. Summing these coefficients identifies the graded Euler characteristic of fully blocked grid homology with the existing grid-determinant expression.

Main definitions

• TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar: the alternating dimension of the homology in one Alexander degree.
• TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar: these characteristics assembled as a Laurent polynomial in the Alexander variable.

Main results

• TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_finsum_finrank: the coefficient is the alternating dimension of the homology groups of the public graded complex.
• TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_alexanderEulerChar: the coefficientwise Euler--Poincaré identity.
• TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar_eq_smul_T_mul_det_weightMatrix: the graded homology Euler characteristic is the normalized grid determinant.

References

The Euler--Poincaré comparison is the algebraic step in Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Sections 4.3--4.4, that identifies the graded Euler characteristic computed from grid states with the one computed from grid homology.

theorem TauCeti.OddComponentGridDiagram.instFactPrimeOfNatNat : Fact (Nat.Prime 2)

noncomputable def TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : ℤ

The Euler characteristic of fully blocked grid homology in Alexander degree a.

The homology is taken after forgetting the finite-dimensionality witness from the bounded cochain complex whose cohomological degree is the negative Maslov degree.

theorem TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_finsum_finrank {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : G.alexanderHomologyEulerChar a = ∑ᶠ (m : ℤ), ↑m.negOnePow * ↑(Module.finrank (ZMod 2) ↑(HomologicalComplex.homology (G.gradedFullyBlockedComplex a) m))

The Euler characteristic in Alexander degree a is the alternating finsum of the dimensions of the homology groups of the public Maslov-graded fully blocked complex.

@[simp]

theorem TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_alexanderEulerChar {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : G.alexanderHomologyEulerChar a = G.alexanderEulerChar (ZMod 2) a

Euler--Poincaré in one Alexander degree. The alternating dimension of fully blocked grid homology equals the alternating count of grid states.

theorem TauCeti.OddComponentGridDiagram.alexanderHomologyEulerChar_eq_zero_of_notMem {n : ℕ} (G : OddComponentGridDiagram n) {a : ℤ} (ha : a ∉ G.alexanderSupport) : G.alexanderHomologyEulerChar a = 0

Fully blocked grid homology has zero Euler characteristic in an Alexander degree containing no grid state.

noncomputable def TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar {n : ℕ} (G : OddComponentGridDiagram n) : LaurentPolynomial ℤ

The graded Euler characteristic of fully blocked grid homology, assembled from its Alexander degrees. The variable T is a square root of the usual Alexander variable, so degree a appears with exponent 2a.

@[simp]

theorem TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar_eq_gradedEulerChar {n : ℕ} (G : OddComponentGridDiagram n) : G.gradedHomologyEulerChar = G.gradedEulerChar (ZMod 2)

The graded Euler characteristic computed from fully blocked grid homology equals the one computed from grid states.

theorem TauCeti.OddComponentGridDiagram.gradedHomologyEulerChar_eq_smul_T_mul_det_weightMatrix {n : ℕ} (G : OddComponentGridDiagram n) : G.gradedHomologyEulerChar = (Equiv.Perm.sign (↑G).O.toPerm * (↑n + 1).negOnePow) • (LaurentPolynomial.T (↑G).alexanderTwoShift * (↑G).weightMatrix.det)

The graded Euler characteristic of fully blocked grid homology is the normalized grid determinant.