Bigraded vector spaces up to ⊗ W-stabilization

Grid homology comes in a family of flavors whose blocked versions depend on the size of the grid rather than on the link alone: the fully blocked homology of an n × n grid diagram presenting an ℓ-component link L is the simply blocked grid homology of L tensored with W^{⊗(n-ℓ)}, where W is the two-dimensional bigraded vector space with one generator in bidegree (0, 0) and one in bidegree (-1, -1). The link invariant is therefore not the bigraded vector space itself but its class modulo tensoring with copies of W. This file builds that quotient, together with the canonical representatives that make it usable.

A finite-dimensional bigraded vector space over a field is determined up to bigraded isomorphism by its dimension function, so the whole discussion takes place at the level of Poincaré series: TauCeti.Bigraded.Series is ℕ[ℤ × ℤ], a finitely supported function assigning a dimension to each bidegree (Maslov, Alexander), with convolution as its product. Tensoring with W is multiplication by TauCeti.Bigraded.W, and unwinding the convolution gives the expected (P * W)(m, a) = P(m, a) + P(m + 1, a + 1).

The quotient is not vacuous, and that is the substance here. Multiplication by W is injective (TauCeti.Bigraded.mul_W_left_injective), so no information beyond the number of stabilizations is lost; note this genuinely uses finite support, since on unbounded bigraded vector spaces tensoring with W is not injective. Consequently each stable class contains exactly one W-indivisible series (TauCeti.Bigraded.exists_isReduced, TauCeti.Bigraded.IsReduced.eq_of_mul_W_pow_eq), the reduced representative, and two series are stably equivalent exactly when their reduced representatives agree (TauCeti.Bigraded.isStablyEquiv_iff_reducedRep_eq). Reduction is therefore a complete invariant of a stable class.

Finally, the Alexander-graded Euler characteristic TauCeti.Bigraded.euler records how much the stabilization actually costs: it is a ring homomorphism to the Laurent polynomials sending W to 1 - T⁻¹, so stabilizing k times multiplies the Euler characteristic by (1 - T⁻¹)^k. That is exactly the factor by which the grid state sum of an n × n diagram differs from the Alexander polynomial of the link it presents, so the Euler characteristic is an invariant of a stable class only after that factor is divided out.

Main definitions

• TauCeti.Bigraded.Series: the Poincaré series of a finite-dimensional bigraded vector space.
• TauCeti.Bigraded.W: the Poincaré series of the stabilization factor W.
• TauCeti.Bigraded.totalDim: the total dimension, as a ring homomorphism.
• TauCeti.Bigraded.IsStablyEquiv, TauCeti.Bigraded.StableSeries: the stabilization equivalence and the quotient it defines.
• TauCeti.Bigraded.IsReduced, TauCeti.Bigraded.reducedRep: W-indivisibility and the canonical representative of a stable class.
• TauCeti.Bigraded.euler: the Alexander-graded Euler characteristic.

Main results

• TauCeti.Bigraded.coeff_mul_W and TauCeti.Bigraded.coeff_mul_W_pow: tensoring with W adds the diagonal shift by (1, 1), and iterating it adds binomial multiples of the shifts.
• TauCeti.Bigraded.mul_W_left_injective: tensoring with W is injective.
• TauCeti.Bigraded.exists_isReduced and TauCeti.Bigraded.IsReduced.eq_of_mul_W_pow_eq: every series is a stabilization of a unique reduced one.
• TauCeti.Bigraded.isStablyEquiv_iff_reducedRep_eq: the reduced representative is a complete invariant of a stable class.
• TauCeti.Bigraded.reduce_injective and TauCeti.Bigraded.stableEquivReduced: the reduced representative identifies the quotient with the W-indivisible series.
• TauCeti.Bigraded.euler_mul_W_pow: stabilizing multiplies the Euler characteristic by 1 - T⁻¹.

References

This supplies the stabilization convention of TauCetiRoadmap/CombinatorialHeegaardFloer/README.md, Lane ALG, which asks for the "graded vector space up to ⊗W-stabilization" quotient "as API, not ad hoc", and which Lane G.5 needs to state which of the blocked grid homologies is a link invariant. The bigraded conventions follow Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapters 4 and 5, where W is the bigraded vector space with generators in bidegrees (0, 0) and (-1, -1).

noncomputable def TauCeti.Bigraded.W : Series

The Poincaré series of the stabilization factor W: one generator in bidegree (0, 0) and one in bidegree (-1, -1).

Equations

• TauCeti.Bigraded.W = 1 + AddMonoidAlgebra.single (-1, -1) 1

@[simp]

theorem TauCeti.Bigraded.coeff_W_zero : W.coeff 0 = 1

The coefficient of W in bidegree (0, 0).

theorem TauCeti.Bigraded.W_ne_zero : W ≠ 0

W is not the zero series: it has a generator in bidegree (0, 0).

theorem TauCeti.Bigraded.coeff_mul_W (P : Series) (g : ℤ × ℤ) : (P * W).coeff g = P.coeff g + P.coeff (g + (1, 1))

Tensoring with W is a shifted sum: the bidegree (m, a) part of P ⊗ W is the bidegree (m, a) part of P plus its bidegree (m + 1, a + 1) part.

theorem TauCeti.Bigraded.mul_W_left_injective : Function.Injective fun (P : Series) => P * W

Tensoring with W is injective. This is where finite support is essential: on bigraded vector spaces with unbounded support the same operation is not injective, since for instance a one-dimensional summand in every bidegree (m, m) and a two-dimensional summand in every second such bidegree have the same stabilization.

theorem TauCeti.Bigraded.mul_W_pow_left_injective (k : ℕ) : Function.Injective fun (P : Series) => P * W ^ k

Tensoring with W repeatedly is injective.

theorem TauCeti.Bigraded.coeff_mul_W_pow (P : Series) (k : ℕ) (g : ℤ × ℤ) : (P * W ^ k).coeff g = ∑ i ∈ Finset.range (k + 1), k.choose i * P.coeff (g + (↑i, ↑i))

The bigraded dimensions of a k-fold stabilization. The summand of P ⊗ W^{⊗k} in bidegree (m, a) collects the summands of P in the bidegrees (m + i, a + i) on the diagonal above it, each with the binomial multiplicity k.choose i.

@[simp]

theorem TauCeti.Bigraded.totalDim_W : totalDim W = 2

The stabilization factor W is two-dimensional.

theorem TauCeti.Bigraded.totalDim_mul_W_pow (P : Series) (k : ℕ) : totalDim (P * W ^ k) = 2 ^ k * totalDim P

Stabilizing k times multiplies the total dimension by 2 ^ k: this is the grid-size dependence of the blocked grid homologies, and it is why the unstabilized theories are not link invariants.

def TauCeti.Bigraded.IsStablyEquiv (P Q : Series) : Prop

Two bigraded vector spaces are stably equivalent when they become isomorphic after tensoring each with some number of copies of W.

Equations

• TauCeti.Bigraded.IsStablyEquiv P Q = ∃ (i : ℕ) (j : ℕ), P * TauCeti.Bigraded.W ^ i = Q * TauCeti.Bigraded.W ^ j

theorem TauCeti.Bigraded.isStablyEquiv_refl (P : Series) : IsStablyEquiv P P

Stable equivalence is reflexive.

theorem TauCeti.Bigraded.IsStablyEquiv.symm {P Q : Series} (h : IsStablyEquiv P Q) : IsStablyEquiv Q P

Stable equivalence is symmetric.

theorem TauCeti.Bigraded.IsStablyEquiv.trans {P Q R : Series} (h : IsStablyEquiv P Q) (h' : IsStablyEquiv Q R) : IsStablyEquiv P R

Stable equivalence is transitive: tensor the two witnesses together.

theorem TauCeti.Bigraded.isStablyEquiv_mul_W_pow (P : Series) (k : ℕ) : IsStablyEquiv (P * W ^ k) P

Tensoring with W does not change the stable class.

def TauCeti.Bigraded.stableSetoid : Setoid Series

Stable equivalence as a setoid, so that the stable classes form a quotient type.

Equations

• TauCeti.Bigraded.stableSetoid = { r := TauCeti.Bigraded.IsStablyEquiv, iseqv := TauCeti.Bigraded.stableSetoid._proof_1✝ }

def TauCeti.Bigraded.StableSeries : Type

A bigraded vector space up to ⊗ W-stabilization. This is the shape of the invariant attached to a link by a blocked grid homology: the grid size is visible in a representative but not in the class.

Equations

• TauCeti.Bigraded.StableSeries = Quotient TauCeti.Bigraded.stableSetoid

def TauCeti.Bigraded.stableMk (P : Series) : StableSeries

The stable class of a bigraded vector space.

Equations

• TauCeti.Bigraded.stableMk P = ⟦P⟧

theorem TauCeti.Bigraded.StableSeries.induction_on {motive : StableSeries → Prop} (S : StableSeries) (mk : ∀ (P : Series), motive (stableMk P)) : motive S

Prove a property of a stable series by proving it on every representative.

def TauCeti.Bigraded.StableSeries.lift {X : Sort u_1} (f : Series → X) (h : ∀ {P Q : Series}, IsStablyEquiv P Q → f P = f Q) : StableSeries → X

Define a function on stable series from a function on representatives that respects stable equivalence.

Equations

• TauCeti.Bigraded.StableSeries.lift f h = Quotient.lift f ⋯

@[simp]

theorem TauCeti.Bigraded.StableSeries.lift_stableMk {X : Sort u_1} (f : Series → X) (h : ∀ {P Q : Series}, IsStablyEquiv P Q → f P = f Q) (P : Series) : StableSeries.lift f ⋯ (stableMk P) = f P

Lifting a function to the stable class of a representative returns its value there.

theorem TauCeti.Bigraded.stableMk_eq_stableMk_iff {P Q : Series} : stableMk P = stableMk Q ↔ IsStablyEquiv P Q

Two series have the same stable class exactly when they are stably equivalent.

@[simp]

theorem TauCeti.Bigraded.stableMk_mul_W_pow (P : Series) (k : ℕ) : stableMk (P * W ^ k) = stableMk P

Tensoring with copies of W does not change the stable class.

def TauCeti.Bigraded.IsReduced (P : Series) : Prop

A bigraded vector space is reduced when it is not a nontrivial stabilization: the only way to write it as Q ⊗ W is with Q = 0. The zero series is reduced.

Equations

• TauCeti.Bigraded.IsReduced P = ∀ (Q : TauCeti.Bigraded.Series), P = Q * TauCeti.Bigraded.W → Q = 0

theorem TauCeti.Bigraded.isReduced_zero : IsReduced 0

The zero series is reduced.

theorem TauCeti.Bigraded.isReduced_of_odd_totalDim {P : Series} (h : Odd (totalDim P)) : IsReduced P

A series of odd total dimension is reduced, since a stabilization has even total dimension. In particular the one-dimensional series in a single bidegree, the Poincaré series of the simply blocked grid homology of the unknot, is reduced.

theorem TauCeti.Bigraded.exists_isReduced (P : Series) : ∃ (Q : Series), IsReduced Q ∧ ∃ (k : ℕ), P = Q * W ^ k

Every bigraded vector space is a stabilization of a reduced one.

theorem TauCeti.Bigraded.IsReduced.eq_of_mul_W_pow_eq {P Q : Series} (hP : IsReduced P) (hQ : IsReduced Q) {i j : ℕ} (h : P * W ^ i = Q * W ^ j) : P = Q

Reduced representatives are unique: two reduced series with a common stabilization are equal.

noncomputable def TauCeti.Bigraded.reducedRep (P : Series) : Series

The reduced representative of a bigraded vector space: the unique reduced series of which it is a stabilization.

Equations

• TauCeti.Bigraded.reducedRep P = ⋯.choose

@[simp]

theorem TauCeti.Bigraded.isReduced_reducedRep (P : Series) : IsReduced (reducedRep P)

The reduced representative is reduced.

theorem TauCeti.Bigraded.exists_mul_W_pow_reducedRep (P : Series) : ∃ (k : ℕ), P = reducedRep P * W ^ k

A series is a stabilization of its reduced representative.

theorem TauCeti.Bigraded.isStablyEquiv_reducedRep (P : Series) : IsStablyEquiv P (reducedRep P)

A series is stably equivalent to its reduced representative.

@[simp]

theorem TauCeti.Bigraded.reducedRep_eq_self {P : Series} (hP : IsReduced P) : reducedRep P = P

A reduced series is its own reduced representative.

theorem TauCeti.Bigraded.isStablyEquiv_iff_reducedRep_eq {P Q : Series} : IsStablyEquiv P Q ↔ reducedRep P = reducedRep Q

Stably equivalent series have the same reduced representative, and conversely: reduction is a complete invariant of a stable class.

noncomputable def TauCeti.Bigraded.reduce : StableSeries → Series

Reduction descends to the quotient: the canonical representative of a stable class.

Equations

• TauCeti.Bigraded.reduce = TauCeti.Bigraded.StableSeries.lift TauCeti.Bigraded.reducedRep @TauCeti.Bigraded.reduce._proof_1✝

@[simp]

theorem TauCeti.Bigraded.reduce_stableMk (P : Series) : reduce (stableMk P) = reducedRep P

The canonical representative of the class of P is the reduced representative of P.

@[simp]

theorem TauCeti.Bigraded.isReduced_reduce (S : StableSeries) : IsReduced (reduce S)

The canonical representative of a stable class is reduced.

@[simp]

theorem TauCeti.Bigraded.stableMk_reduce (S : StableSeries) : stableMk (reduce S) = S

The canonical representative of a stable class lies in that class.

theorem TauCeti.Bigraded.reduce_injective : Function.Injective reduce

A stable class is determined by its canonical representative.

theorem TauCeti.Bigraded.isReduced_one : IsReduced 1

The unit series, the Poincaré series of a one-dimensional bigraded vector space in bidegree (0, 0), is reduced.

@[simp]

theorem TauCeti.Bigraded.totalDim_W_pow (k : ℕ) : totalDim (W ^ k) = 2 ^ k

Stabilizing the trivial one-dimensional bigraded vector space k times doubles its dimension each time. This is the grid-size dependence of the fully blocked grid homology of an n × n unknot grid, whose Poincaré series is W ^ (n - 1).

@[simp]

theorem TauCeti.Bigraded.reducedRep_W_pow (k : ℕ) : reducedRep (W ^ k) = 1

All the stabilizations of the trivial bigraded vector space have the same reduced representative, although their dimensions 2 ^ k are all different.

noncomputable def TauCeti.Bigraded.stableEquivReduced : StableSeries ≃ { P : Series // IsReduced P }

The stable classes of finite-dimensional bigraded vector spaces are exactly the W-indivisible ones: reduction and inclusion are mutually inverse.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.Bigraded.euler_W : euler W = 1 - LaurentPolynomial.T (-1)

The Euler characteristic of the stabilization factor is 1 - T⁻¹.

theorem TauCeti.Bigraded.euler_mul_W_pow (P : Series) (k : ℕ) : euler (P * W ^ k) = euler P * (1 - LaurentPolynomial.T (-1)) ^ k

Stabilizing multiplies the Alexander-graded Euler characteristic by 1 - T⁻¹. The blocked grid homology of an n × n grid presenting an ℓ-component link therefore has Euler characteristic (1 - T⁻¹)^(n-ℓ) times that of the link invariant it stabilizes, which is the discrepancy between the grid state sum and the Alexander polynomial.