The graded Euler characteristic of the grid chain module

Grading/Chain.lean decomposes the grid chain module of a diagram with an odd number of link components into its homogeneous pieces, one for each pair (O-Maslov grading, Alexander grading), and Determinant.lean evaluates the alternating Alexander state sum of a grid diagram as a determinant. This file joins the two: the graded Euler characteristic of the bigraded grid chain module is the state sum, hence is a normalized grid-determinant expression.

Freezing one Alexander degree a leaves a module graded by the O-Maslov degree alone, and its Euler characteristic is Mathlib's GradedObject.eulerChar for the complex shape ComplexShape.down ℤ, the shape of a differential dropping the Maslov grading by one. That integer, OddComponentGridDiagram.alexanderEulerChar, is the alternating count of grid states in Alexander degree a weighted by the parity of their Maslov grading. Applying the generic Bigraded.euler map to the rank Poincaré series and then doubling its Alexander exponents gives OddComponentGridDiagram.gradedEulerChar.

Two conventions are inherited rather than reinvented. The grading variable T is a square root of the usual Alexander variable, exactly as in Determinant.lean: the summand in bidegree (m, a) contributes (-1)^m T^{2a}, so that the graded Euler characteristic lives in the same ring as the state sum and compares with the determinant on the nose. The Maslov grading is the one that the grid differential drops, which is why the alternating signs are read off ComplexShape.down ℤ.

The graded-object Euler characteristic is defined by ranks alone. Over ZMod 2, it is also the Euler characteristic of OddComponentGridDiagram.gradedFullyBlockedComplex, whose differential lowers the Maslov degree and preserves the Alexander degree. The comparison with the Euler characteristic of its homology remains a separate step.

Main definitions

• TauCeti.OddComponentGridDiagram.alexanderGradedObject: the Maslov-graded object of a fixed Alexander degree.
• TauCeti.OddComponentGridDiagram.alexanderEulerChar: its Euler characteristic.
• TauCeti.OddComponentGridDiagram.bigradedPoincareSeries: the Poincaré series of the grid chain module in its (O-Maslov, Alexander) bidegrees.
• TauCeti.OddComponentGridDiagram.gradedEulerChar: the graded Euler characteristic of the bigraded grid chain module, as a Laurent polynomial in the square root of the Alexander variable.

Main results

• TauCeti.OddComponentGridDiagram.eulerChar_gradedFullyBlockedComplex: the graded complex has Euler characteristic alexanderEulerChar (ZMod 2) a in Alexander degree a.
• TauCeti.OddComponentGridDiagram.alexanderEulerChar_eq_sum_states: the Euler characteristic in one Alexander degree is the alternating count of the grid states of that degree.
• TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_stateSum: the graded Euler characteristic is the alternating Alexander state sum.
• TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_smul_T_mul_det_weightMatrix: the graded Euler characteristic is a sign times a monomial times the grid determinant.
• TauCeti.OddComponentGridDiagram.sum_alexanderEulerChar_eq_zero: the ungraded Euler characteristic of a grid chain module of size at least two vanishes.
• TauCeti.OddComponentGridDiagram.alexanderEulerChar_eq_coeff_smul_T_mul_det_weightMatrix: the Euler characteristic of an Alexander degree is the corresponding coefficient of the normalized grid determinant expression.

References

This advances TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane G.4, "Euler characteristic = Alexander polynomial, via the grid determinant formula", by supplying the Euler characteristic side of that equation; the grid determinant side is Determinant.lean. The conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 3.3 and Chapter 4.

The Euler characteristic of one Alexander degree

noncomputable def TauCeti.OddComponentGridDiagram.alexanderGradedObject {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] (a : ℤ) : CategoryTheory.GradedObject ℤ (ModuleCat R)

The O-Maslov-graded object underlying the grid chain module in a fixed Alexander degree.

@[simp]

theorem TauCeti.OddComponentGridDiagram.alexanderGradedObject_apply {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] (a m : ℤ) : G.alexanderGradedObject R a m = ↧(G.BigradedChainPiece R (m, a))

The degree-m component of the Maslov-graded object in Alexander degree a.

theorem TauCeti.OddComponentGridDiagram.finrank_alexanderGradedObject {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (a m : ℤ) : Module.finrank R ↑(G.alexanderGradedObject R a m) = {x : GridState n | G.bidegree x = (m, a)}.card

The rank of the Maslov-graded object in degree m is the number of grid states of bidegree (m, a).

noncomputable def TauCeti.OddComponentGridDiagram.alexanderEulerChar {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] (a : ℤ) : ℤ

The Euler characteristic of the grid chain module in a fixed Alexander degree, taken with respect to the O-Maslov grading.

The complex shape is ComplexShape.down ℤ because the grid differential drops the Maslov grading by one.

@[simp]

theorem TauCeti.OddComponentGridDiagram.eulerChar_gradedFullyBlockedComplex {n : ℕ} (G : OddComponentGridDiagram n) (a : ℤ) : HomologicalComplex.eulerChar (G.gradedFullyBlockedComplex a) = G.alexanderEulerChar (ZMod 2) a

The Euler characteristic of gradedFullyBlockedComplex a equals alexanderEulerChar (ZMod 2) a. Its identification with the alternating state count is given by alexanderEulerChar_eq_sum_states.

theorem TauCeti.OddComponentGridDiagram.alexanderEulerChar_eq_sum_maslovSupport {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (a : ℤ) : G.alexanderEulerChar R a = ∑ m ∈ G.maslovSupport a, ↑m.negOnePow * ↑{x : GridState n | G.bidegree x = (m, a)}.card

The Euler characteristic of an Alexander degree, as a finite alternating sum of the ranks of its homogeneous pieces.

theorem TauCeti.OddComponentGridDiagram.alexanderEulerChar_eq_sum_states {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (a : ℤ) : G.alexanderEulerChar R a = ∑ x : GridState n with G.alexanderℤ x = a, ↑((↑G).maslovOℤ x).negOnePow

The Euler characteristic of an Alexander degree is the alternating count of the grid states of that degree, weighted by the parity of their O-Maslov grading.

@[simp]

theorem TauCeti.OddComponentGridDiagram.alexanderEulerChar_eq_zero_of_notMem {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] {a : ℤ} (ha : a ∉ G.alexanderSupport) : G.alexanderEulerChar R a = 0

In an unoccupied Alexander degree the Euler characteristic vanishes.

The graded Euler characteristic

noncomputable def TauCeti.OddComponentGridDiagram.bigradedPoincareSeries {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] : Bigraded.Series

The Poincaré series of the bigraded grid chain module in the standard (O-Maslov, Alexander) convention.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coeff_bigradedPoincareSeries {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] (g : ℤ × ℤ) : (G.bigradedPoincareSeries R).coeff g = Module.finrank R (G.BigradedChainPiece R g)

The coefficient of the grid-chain Poincaré series in a bidegree is the rank of that homogeneous piece.

@[simp]

theorem TauCeti.OddComponentGridDiagram.totalDim_bigradedPoincareSeries {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] : Bigraded.totalDim (G.bigradedPoincareSeries R) = n.factorial

The total dimension of the grid-chain Poincaré series is the number n! of grid states.

noncomputable def TauCeti.OddComponentGridDiagram.gradedEulerChar {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] : LaurentPolynomial ℤ

The graded Euler characteristic obtained by applying Bigraded.euler to the rank Poincaré series of the bigraded grid chain module and then doubling every Alexander exponent.

The grading variable T is a square root of the Alexander variable, as in Determinant.lean, so Alexander degree a contributes the monomial T^{2a}.

theorem TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_stateSum {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] : G.gradedEulerChar R = (↑G).stateSum

The graded Euler characteristic is the alternating Alexander state sum. Regrouping the states of the diagram by their bidegree turns the rank-weighted sum over occupied degrees into the sum over states.

theorem TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_smul_T_mul_det_weightMatrix {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] [StrongRankCondition R] : G.gradedEulerChar R = (Equiv.Perm.sign (↑G).O.toPerm * (↑n + 1).negOnePow) • (LaurentPolynomial.T (↑G).alexanderTwoShift * (↑G).weightMatrix.det)

The graded Euler characteristic is a normalized grid-determinant expression. Combining OddComponentGridDiagram.gradedEulerChar_eq_stateSum with the grid determinant formula, the graded Euler characteristic of the bigraded grid chain module is a sign times a monomial times the determinant of the weight matrix of the diagram.

theorem TauCeti.OddComponentGridDiagram.sum_alexanderEulerChar_eq_zero {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (hn : 2 ≤ n) : ∑ a ∈ G.alexanderSupport, G.alexanderEulerChar R a = 0

The ungraded Euler characteristic of the grid chain module vanishes on every grid of size at least two: the Euler characteristics of the Alexander degrees cancel.

This is the graded Euler characteristic evaluated at T = 1, where the weight matrix of the determinant formula acquires two equal rows.

Reading the Alexander degrees off the coefficients

theorem TauCeti.OddComponentGridDiagram.gradedEulerChar_eq_sum_alexanderSupport {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] : G.gradedEulerChar R = ∑ a ∈ G.alexanderSupport, G.alexanderEulerChar R a • LaurentPolynomial.T (2 * a)

The graded Euler characteristic is the generating function of the Euler characteristics in the occupied Alexander degrees, with doubled exponents for the square-root variable.

theorem TauCeti.OddComponentGridDiagram.coeff_gradedEulerChar {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (k : ℤ) : (G.gradedEulerChar R).coeff k = ∑ a ∈ G.alexanderSupport, if 2 * a = k then G.alexanderEulerChar R a else 0

The coefficients of the graded Euler characteristic, degree by degree.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coeff_gradedEulerChar_of_odd {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Semiring R] {k : ℤ} (hk : Odd k) : (G.gradedEulerChar R).coeff k = 0

Only even exponents occur in the graded Euler characteristic: the grading variable is a square root of the Alexander variable, and the Alexander gradings of an odd-component diagram are integers.

@[simp]

theorem TauCeti.OddComponentGridDiagram.coeff_gradedEulerChar_two_mul {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (a : ℤ) : (G.gradedEulerChar R).coeff (2 * a) = G.alexanderEulerChar R a

The graded Euler characteristic loses nothing: its coefficient in exponent 2a is the Euler characteristic of Alexander degree a.

theorem TauCeti.OddComponentGridDiagram.alexanderEulerChar_eq_coeff_smul_T_mul_det_weightMatrix {n : ℕ} (G : OddComponentGridDiagram n) (R : Type u_1) [Ring R] [StrongRankCondition R] (a : ℤ) : G.alexanderEulerChar R a = ((Equiv.Perm.sign (↑G).O.toPerm * (↑n + 1).negOnePow) • (LaurentPolynomial.T (↑G).alexanderTwoShift * (↑G).weightMatrix.det)).coeff (2 * a)

The Euler characteristics of the Alexander degrees are the coefficients of the normalized grid-determinant expression. The alternating count of grid states of Alexander degree a, weighted by the parity of their Maslov grading, is the coefficient of T^{2a} in the expression of GridDiagram.stateSum_eq_smul_T_mul_det_weightMatrix.