Documentation

TauCeti.Algebra.Bigraded.Basic

Bigraded Poincaré series #

This file defines the Poincaré series of a finite-dimensional bigraded vector space, together with its total dimension and Alexander-graded Euler characteristic.

Main definitions #

source
@[reducible, inline]
abbrev TauCeti.Bigraded.Series :
Type

The Poincaré series of a finite-dimensional bigraded vector space: the dimension of the summand in each bidegree (Maslov, Alexander), all but finitely many of them zero.

Over a field, a bigraded vector space with only finitely many nonzero finite-dimensional summands is determined up to bigraded isomorphism by this function, and the product is the Poincaré series of the tensor product.

Equations
Instances For
    source
    noncomputable def TauCeti.Bigraded.totalDim :
    Series →+* ℕ

    The total dimension of a finite-dimensional bigraded vector space, as a ring homomorphism: the tensor product multiplies total dimensions.

    Equations
    Instances For
      source
      theorem TauCeti.Bigraded.totalDim_apply (P : Series) :
      totalDim P = P.coeff.sum fun (x : ℤ × ℤ) (c : ℕ) => c

      The total dimension is the sum of the dimensions of all the bigraded summands.

      source
      @[simp]
      theorem TauCeti.Bigraded.totalDim_single (g : ℤ × ℤ) (r : ℕ) :
      totalDim (AddMonoidAlgebra.single g r) = r

      The total dimension of a series concentrated in one bidegree.

      source
      @[simp]
      theorem TauCeti.Bigraded.totalDim_eq_zero_iff (P : Series) :
      totalDim P = 0 ↔ P = 0

      Only the zero series has total dimension zero.

      source
      noncomputable def TauCeti.Bigraded.eulerMonoidHom :
      Multiplicative (ℤ × ℤ) →* LaurentPolynomial ℤ

      The Alexander-graded Euler characteristic of a bigraded vector space, as a monoid homomorphism on bidegrees: bidegree (m, a) contributes (-1)^m T^a.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def TauCeti.Bigraded.euler :
        Series →+* LaurentPolynomial ℤ

        The Alexander-graded Euler characteristic of a finite-dimensional bigraded vector space: the Laurent polynomial whose T^a coefficient is the alternating sum, over the Maslov grading, of the dimensions in Alexander grading a.

        This is a ring homomorphism, so it turns the tensor product into a product of Laurent polynomials.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.Bigraded.euler_single (m a : ℤ) (r : ℕ) :
          euler (AddMonoidAlgebra.single (m, a) r) = ↑r * AddMonoidAlgebra.single a ↑m.negOnePow

          The Euler characteristic of a series concentrated in one bidegree.