Finite Laurent support and graded dimension

A family of vector spaces indexed by ℤ has a Laurent-polynomial-valued graded dimension only when every piece is finite-dimensional and only finitely many pieces are nonzero. This file packages those two conditions as TauCeti.HasFiniteLaurentSupport and defines TauCeti.gradedDimension without using a totalized infinite sum.

For a family V, gradedDimension k V h has coefficient dim_k(V j) in degree j. The companion targetShiftGradedDimension implements the convention used by the Grothendieck--Euler roadmap for target shifts:

qdim(V) = ∑ j, q⁻ʲ dim_k(V j).

Both definitions are built from the canonical finitely supported function of dimensions, so no chosen support appears in their public API. The finite-sum theorems allow calculations with any explicit bounding finset, while coefficient lemmas characterize the resulting Laurent polynomial.

Main definitions

• TauCeti.HasFiniteLaurentSupport: termwise finite-dimensionality and finite support.
• TauCeti.HasFiniteLaurentSupport.reindex_add: translation of the internal degree preserves finite Laurent support.
• TauCeti.gradedDimension: the Laurent polynomial with coefficient dim_k(V j) at j.
• TauCeti.targetShiftGradedDimension: the target-shift convention with exponent -j.
• TauCeti.targetShiftGradedDimension_reindex_add: translation of the family multiplies this polynomial by the corresponding Laurent monomial.
• TauCeti.laurentEval_one_gradedDimension and TauCeti.laurentEval_one_targetShiftGradedDimension: both conventions evaluate at q = 1 to the dimension of the direct sum of all the pieces.

The predicate is closed under degreewise exact sequences, and both dimension conventions are additive on degreewise short exact sequences.

References

• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for graded dimensions and the target-shift convention.
• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layer 6, "Finite Laurent support".

structure TauCeti.HasFiniteLaurentSupport (k : Type u) [DivisionRing k] (V : ℤ → Type v) [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] : Prop

A ℤ-graded family of vector spaces has finite Laurent support when every homogeneous piece is finite-dimensional and the set of degrees with nonzero dimension is finite.

The second field records the canonical support of the dimension function rather than a chosen bounding finset. For finite-dimensional vector spaces, zero dimension is equivalent to the piece being a subsingleton; see HasFiniteLaurentSupport.exists_finset for that formulation.

• finiteDimensional (j : ℤ) : FiniteDimensional k (V j)

  Every homogeneous piece is finite-dimensional.

• finite_finrankSupport : (Function.support fun (j : ℤ) => Module.finrank k (V j)).Finite

  Only finitely many homogeneous pieces have nonzero dimension.

theorem TauCeti.HasFiniteLaurentSupport.of_finset {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (hfinite : ∀ (j : ℤ), FiniteDimensional k (V j)) (s : Finset ℤ) (hzero : ∀ j ∉ s, Subsingleton (V j)) : HasFiniteLaurentSupport k V

A finite set outside which every piece is zero proves finite Laurent support.

theorem TauCeti.HasFiniteLaurentSupport.exists_finset {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : ∃ (s : Finset ℤ), ∀ j ∉ s, Subsingleton (V j)

Finite Laurent support can be exhibited by a finite set outside which every piece is zero.

theorem TauCeti.HasFiniteLaurentSupport.of_equiv {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (h : HasFiniteLaurentSupport k V) (e : (j : ℤ) → V j ≃ₗ[k] W j) : HasFiniteLaurentSupport k W

A pointwise linear equivalence preserves finite Laurent support.

theorem TauCeti.HasFiniteLaurentSupport.prod {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (hW : HasFiniteLaurentSupport k W) : HasFiniteLaurentSupport k fun (j : ℤ) => V j × W j

The degreewise product of two finitely Laurent-supported families is finitely supported.

theorem TauCeti.HasFiniteLaurentSupport.of_exact {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {U : ℤ → Type v'} [(j : ℤ) → AddCommGroup (U j)] [(j : ℤ) → Module k (U j)] {W : ℤ → Type u_1} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hU : HasFiniteLaurentSupport k U) (hW : HasFiniteLaurentSupport k W) (f : (j : ℤ) → U j →ₗ[k] V j) (g : (j : ℤ) → V j →ₗ[k] W j) (hfg : ∀ (j : ℤ), Function.Exact ⇑(f j) ⇑(g j)) : HasFiniteLaurentSupport k V

In a degreewise exact sequence, finite Laurent support of the outer families implies finite Laurent support of the middle family.

theorem TauCeti.HasFiniteLaurentSupport.reindex_add {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (r : ℤ) : HasFiniteLaurentSupport k fun (j : ℤ) => V (j + r)

A finite Laurent support is preserved by translating the degree index.

noncomputable def TauCeti.gradedDimension (k : Type u) [DivisionRing k] (V : ℤ → Type v) [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : LaurentPolynomial ℤ

The graded dimension of a finitely Laurent-supported family of vector spaces. Its coefficient in degree j is dim_k(V j).

Equations

• TauCeti.gradedDimension k V h = AddMonoidAlgebra.ofCoeff (Finsupp.ofSupportFinite (fun (j : ℤ) => ↑(Module.finrank k (V j))) ⋯)

@[simp]

theorem TauCeti.coeff_gradedDimension {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (j : ℤ) : (gradedDimension k V h).coeff j = ↑(Module.finrank k (V j))

The coefficient of the graded dimension is the dimension of the corresponding piece.

theorem TauCeti.gradedDimension_reindex_add {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (r : ℤ) : gradedDimension k (fun (j : ℤ) => V (j + r)) ⋯ = LaurentPolynomial.T (-r) * gradedDimension k V h

The graded dimension of a translated family is multiplied by the Laurent monomial T (-r).

theorem TauCeti.support_gradedDimension {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : (gradedDimension k V h).coeff.support = ⋯.toFinset

The support of the graded dimension is exactly the set of degrees with nonzero dimension.

theorem TauCeti.gradedDimension_eq_sum {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (s : Finset ℤ) (hs : ∀ j ∉ s, Subsingleton (V j)) : gradedDimension k V h = ∑ j ∈ s, LaurentPolynomial.C ↑(Module.finrank k (V j)) * LaurentPolynomial.T j

Any finite set outside which the pieces vanish computes the graded dimension as a finite sum. Thus calculations do not depend on the particular support bound supplied by a caller.

theorem TauCeti.gradedDimension_congr {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (hW : HasFiniteLaurentSupport k W) (hdim : ∀ (j : ℤ), Module.finrank k (V j) = Module.finrank k (W j)) : gradedDimension k V hV = gradedDimension k W hW

Pointwise equality of dimensions determines the graded dimension.

theorem TauCeti.gradedDimension_equiv {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (e : (j : ℤ) → V j ≃ₗ[k] W j) : gradedDimension k V hV = gradedDimension k W ⋯

Pointwise linear equivalences preserve graded dimension.

@[simp]

theorem TauCeti.gradedDimension_eq_zero_iff {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : gradedDimension k V h = 0 ↔ ∀ (j : ℤ), Subsingleton (V j)

The graded dimension vanishes exactly when every homogeneous piece is zero.

theorem TauCeti.gradedDimension_prod {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (hW : HasFiniteLaurentSupport k W) : gradedDimension k (fun (j : ℤ) => V j × W j) ⋯ = gradedDimension k V hV + gradedDimension k W hW

Graded dimension is additive on degreewise direct sums.

theorem TauCeti.gradedDimension_shortExact {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {U : ℤ → Type v'} [(j : ℤ) → AddCommGroup (U j)] [(j : ℤ) → Module k (U j)] {W : ℤ → Type u_1} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hU : HasFiniteLaurentSupport k U) (hW : HasFiniteLaurentSupport k W) (f : (j : ℤ) → U j →ₗ[k] V j) (g : (j : ℤ) → V j →ₗ[k] W j) (hinj : ∀ (j : ℤ), Function.Injective ⇑(f j)) (hfg : ∀ (j : ℤ), Function.Exact ⇑(f j) ⇑(g j)) (hsurj : ∀ (j : ℤ), Function.Surjective ⇑(g j)) : gradedDimension k V ⋯ = gradedDimension k U hU + gradedDimension k W hW

Graded dimension is additive on a degreewise short exact sequence.

noncomputable def TauCeti.targetShiftGradedDimension (k : Type u) [DivisionRing k] (V : ℤ → Type v) [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : LaurentPolynomial ℤ

The graded dimension in the target-shift convention: the piece indexed by j contributes dim_k(V j) q⁻ʲ. This is gradedDimension with the standard Laurent involution applied.

Equations

• TauCeti.targetShiftGradedDimension k V h = LaurentPolynomial.invert (TauCeti.gradedDimension k V h)

@[simp]

theorem TauCeti.coeff_targetShiftGradedDimension {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (j : ℤ) : (targetShiftGradedDimension k V h).coeff j = ↑(Module.finrank k (V (-j)))

The coefficient at exponent j in the target-shift graded dimension is the dimension of the piece indexed by -j.

theorem TauCeti.targetShiftGradedDimension_reindex_add {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (r : ℤ) : targetShiftGradedDimension k (fun (j : ℤ) => V (j + r)) ⋯ = LaurentPolynomial.T r * targetShiftGradedDimension k V h

The target-shift dimension of a translated family is multiplied by the Laurent monomial T r.

theorem TauCeti.support_targetShiftGradedDimension {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : (targetShiftGradedDimension k V h).coeff.support = Finset.image (fun (j : ℤ) => -j) ⋯.toFinset

The support of the target-shift graded dimension is the negation of the set of degrees with nonzero dimension.

theorem TauCeti.targetShiftGradedDimension_congr {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (hW : HasFiniteLaurentSupport k W) (hdim : ∀ (j : ℤ), Module.finrank k (V j) = Module.finrank k (W j)) : targetShiftGradedDimension k V hV = targetShiftGradedDimension k W hW

Pointwise equality of dimensions determines the target-shift graded dimension.

theorem TauCeti.targetShiftGradedDimension_equiv {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (e : (j : ℤ) → V j ≃ₗ[k] W j) : targetShiftGradedDimension k V hV = targetShiftGradedDimension k W ⋯

Pointwise linear equivalences preserve target-shift graded dimension.

@[simp]

theorem TauCeti.targetShiftGradedDimension_eq_zero_iff {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : targetShiftGradedDimension k V h = 0 ↔ ∀ (j : ℤ), Subsingleton (V j)

The target-shift graded dimension vanishes exactly when every homogeneous piece is zero.

theorem TauCeti.targetShiftGradedDimension_eq_sum {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) (s : Finset ℤ) (hs : ∀ j ∉ s, Subsingleton (V j)) : targetShiftGradedDimension k V h = ∑ j ∈ s, LaurentPolynomial.C ↑(Module.finrank k (V j)) * LaurentPolynomial.T (-j)

An explicit support bound computes the target-shift graded dimension as ∑ j, dim_k(V j) q⁻ʲ.

theorem TauCeti.targetShiftGradedDimension_prod {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {W : ℤ → Type v'} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hV : HasFiniteLaurentSupport k V) (hW : HasFiniteLaurentSupport k W) : targetShiftGradedDimension k (fun (j : ℤ) => V j × W j) ⋯ = targetShiftGradedDimension k V hV + targetShiftGradedDimension k W hW

Target-shift graded dimension is additive on degreewise direct sums.

theorem TauCeti.targetShiftGradedDimension_shortExact {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] {U : ℤ → Type v'} [(j : ℤ) → AddCommGroup (U j)] [(j : ℤ) → Module k (U j)] {W : ℤ → Type u_1} [(j : ℤ) → AddCommGroup (W j)] [(j : ℤ) → Module k (W j)] (hU : HasFiniteLaurentSupport k U) (hW : HasFiniteLaurentSupport k W) (f : (j : ℤ) → U j →ₗ[k] V j) (g : (j : ℤ) → V j →ₗ[k] W j) (hinj : ∀ (j : ℤ), Function.Injective ⇑(f j)) (hfg : ∀ (j : ℤ), Function.Exact ⇑(f j) ⇑(g j)) (hsurj : ∀ (j : ℤ), Function.Surjective ⇑(g j)) : targetShiftGradedDimension k V ⋯ = targetShiftGradedDimension k U hU + targetShiftGradedDimension k W hW

Target-shift graded dimension is additive on a degreewise short exact sequence.

The total dimension

theorem TauCeti.HasFiniteLaurentSupport.finiteDimensional_directSum {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : FiniteDimensional k (DirectSum ℤ fun (j : ℤ) => V j)

A family with finite Laurent support has a finite-dimensional direct sum.

@[simp]

theorem TauCeti.laurentEval_one_gradedDimension {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : (laurentEval 1) (gradedDimension k V h) = ↑(Module.finrank k (DirectSum ℤ fun (j : ℤ) => V j))

The graded dimension at q = 1 is the total dimension. Its coefficients are the dimensions of the homogeneous pieces, so setting q = 1 adds them up.

@[simp]

theorem TauCeti.laurentEval_one_targetShiftGradedDimension {k : Type u} [DivisionRing k] {V : ℤ → Type v} [(j : ℤ) → AddCommGroup (V j)] [(j : ℤ) → Module k (V j)] (h : HasFiniteLaurentSupport k V) : (laurentEval 1) (targetShiftGradedDimension k V h) = ↑(Module.finrank k (DirectSum ℤ fun (j : ℤ) => V j))

The target-shift graded dimension at q = 1 is the total dimension. The two conventions differ by q ↦ q⁻¹, which the specialization at q = 1 does not see.