Poincaré series of modular invariant rings

DefinitionLinear substitution by a matrix#✓fully proved

For natural numbers \(p\) and \(n\) and an \(n \times n\) matrix \(g\) over \(\mathbb{Z}/p\mathbb{Z}\), the linear substitution by \(g\) is the \(\mathbb{Z}/p\mathbb{Z}\)-algebra endomorphism of the polynomial ring \((\mathbb{Z}/p\mathbb{Z})[x_0, \dots, x_{n-1}]\) that sends each variable \(x_i\) to \(\sum_j g_{ij} x_j\). Viewing polynomials as functions on \(V = (\mathbb{Z}/p\mathbb{Z})^n\), it sends \(f\) to the function \(x \mapsto f(gx)\).

noncomputable def linSubst {p n : ℕ} (g : Matrix (Fin n) (Fin n) (ZMod p)) :
    MvPolynomial (Fin n) (ZMod p) →ₐ[ZMod p] MvPolynomial (Fin n) (ZMod p) :=
  aeval fun i => ∑ j, C (g i j) * X j

Used by 1

Used byHomogeneous component of the invariant ring

DefinitionHomogeneous component of the invariant ring#✓fully proved

For natural numbers \(p\) and \(n\), a subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{Z}/p\mathbb{Z})\) and \(m \in \mathbb{N}\), the degree-\(m\) component \(T_m\) of the invariant ring \(T\) of \(G\) is the \(\mathbb{Z}/p\mathbb{Z}\)-submodule of the polynomial ring \((\mathbb{Z}/p\mathbb{Z})[x_0, \dots, x_{n-1}]\) consisting of the homogeneous polynomials \(f\) of degree \(m\) that are fixed by the linear substitution \(x_i \mapsto \sum_j g_{ij} x_j\) of every \(g \in G\), that is, with \(f(gx) = f(x)\) as polynomials for all \(g \in G\), where \(x = (x_0, \dots, x_{n-1})\) is the column vector of variables.

noncomputable def invariantComponent {p n : ℕ} (G : Subgroup (GL (Fin n) (ZMod p))) (m : ℕ) :
    Submodule (ZMod p) (MvPolynomial (Fin n) (ZMod p)) :=
  homogeneousSubmodule (Fin n) (ZMod p) m ⊓
    ⨅ g ∈ G, LinearMap.ker
      ((linSubst (g : Matrix (Fin n) (Fin n) (ZMod p))).toLinearMap - LinearMap.id)

Uses 1 · Used by 1

Statement usesLinear substitution by a matrix

Used byPoincaré series of the invariant ring

DefinitionPoincaré series of the invariant ring#✓fully proved

For natural numbers \(p\) and \(n\) and a subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{Z}/p\mathbb{Z})\), the Poincaré series of the invariant ring \(T\) of \(G\) is the formal power series \(P(t) = \sum_{m \ge 0} b_m t^m\) over \(\mathbb{Q}\), where \(b_m\) is the rank over \(\mathbb{Z}/p\mathbb{Z}\) (the dimension, when \(p\) is prime) of the degree-\(m\) homogeneous component \(T_m\) of \(T\).

noncomputable def poincareSeries {p n : ℕ} (G : Subgroup (GL (Fin n) (ZMod p))) :
    PowerSeries ℚ :=
  PowerSeries.mk fun m => (Module.finrank (ZMod p) (invariantComponent G m) : ℚ)

Uses 1 · Used by 1

Statement usesHomogeneous component of the invariant ring

Used byCarlisle–Kropholler conjecture on the second Laurent coefficient (Kourovka 12.36)

DefinitionPointwise stabilizer#✓fully proved

For natural numbers \(p\) and \(n\), a subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{Z}/p\mathbb{Z})\) and a submodule \(W\) of \(V = (\mathbb{Z}/p\mathbb{Z})^n\), the pointwise stabilizer \(G_W\) of \(W\) in \(G\) is the set of all \(g \in G\) with \(g w = w\) for every \(w \in W\), where \(g\) acts on column vectors by matrix multiplication.

def pointwiseStabilizer {p n : ℕ} (G : Subgroup (GL (Fin n) (ZMod p)))
    (W : Submodule (ZMod p) (Fin n → ZMod p)) : Set (GL (Fin n) (ZMod p)) :=
  {g | g ∈ G ∧ ∀ w ∈ W, (g : Matrix (Fin n) (Fin n) (ZMod p)).mulVec w = w}

Used by 1

Used byHyperplane term

DefinitionHyperplane term#✓fully proved

For natural numbers \(p\) and \(n\), a subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{Z}/p\mathbb{Z})\) and a submodule \(W\) of \(V = (\mathbb{Z}/p\mathbb{Z})^n\), let \(N\) be the number of elements of the pointwise stabilizer \(G_W\) of \(W\) in \(G\) (taken to be \(0\) if \(G_W\) is infinite), let \(\alpha_W\) be the exponent of \(p\) in the prime factorization of \(N\) (which is \(0\) unless \(p\) is prime and \(N \ne 0\)), and let \(s_W = N / p^{\alpha_W}\), so that \(N = p^{\alpha_W} s_W\) and \(p \nmid s_W\) when \(p\) is prime and \(N \ne 0\). The hyperplane term of \(W\) is the rational number \((p - 1) \alpha_W + s_W - 1\).

noncomputable def hyperplaneTerm {p n : ℕ} (G : Subgroup (GL (Fin n) (ZMod p)))
    (W : Submodule (ZMod p) (Fin n → ZMod p)) : ℚ :=
  let N := Nat.card (pointwiseStabilizer G W)
  (((p - 1) * N.factorization p : ℕ) : ℚ) + ((N / p ^ N.factorization p : ℕ) : ℚ) - 1

Uses 1 · Used by 1

Statement usesPointwise stabilizer

Used byHyperplane sum

DefinitionHyperplane sum#✓fully proved

For natural numbers \(p\) and \(n\) and a subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{Z}/p\mathbb{Z})\), the hyperplane sum of \(G\) is the rational number \(r = \sum_W ((p - 1) \alpha_W + s_W - 1)\), where \(W\) runs over the maximal proper submodules of \(V = (\mathbb{Z}/p\mathbb{Z})^n\) (the hyperplanes of \(V\) when \(p\) is prime) and \((p - 1) \alpha_W + s_W - 1\) is the hyperplane term of \(W\): here \(N_W\) is the number of elements of the pointwise stabilizer \(G_W\) of \(W\) in \(G\) (taken to be \(0\) if \(G_W\) is infinite), \(\alpha_W\) is the exponent of \(p\) in the prime factorization of \(N_W\) (which is \(0\) unless \(p\) is prime and \(N_W \ne 0\)), and \(s_W = N_W / p^{\alpha_W}\), so that \(N_W = p^{\alpha_W} s_W\). The sum is defined to be \(0\) if infinitely many of its terms are nonzero, which can happen only for \(p = 0\).

noncomputable def hyperplaneSum {p n : ℕ} (G : Subgroup (GL (Fin n) (ZMod p))) : ℚ :=
  ∑ᶠ (W : Submodule (ZMod p) (Fin n → ZMod p)) (_ : IsCoatom W), hyperplaneTerm G W

Uses 1 · Used by 1

Statement usesHyperplane term

Used byCarlisle–Kropholler conjecture on the second Laurent coefficient (Kourovka 12.36)

DefinitionCarlisle–Kropholler conjecture on the second Laurent coefficient (Kourovka 12.36)#✓fully proved

The statement that for every prime \(p\), every \(n \in \mathbb{N}\) and every subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{F}_p)\), with \(P(t)\) the Poincaré series of the invariant ring of \(G\) and \(r\) the hyperplane sum of \(G\), there are polynomials \(A, B \in \mathbb{Q}[t]\) with \(B(1) \ne 0\) and \(B(t) (1 - t)^n P(t) = A(t)\) in \(\mathbb{Q}[[t]]\) such that

\[\frac{A(1) B'(1) - A'(1) B(1)}{B(1)^2} = \frac{r}{2 |G|}.\]

Here \((1 - t)^n P(t) = A(t) / B(t) = a_{-n} + a_{-n+1} (1 - t) + \cdots\), where \(P(t) = \sum_{i \ge -n} a_i (1 - t)^i\) is the Laurent expansion of \(P\) at \(t = 1\), so the left side is \(a_{-n+1} = -(A / B)'(1)\), and the conjecture says \(a_{-n+1} = r / (2 |G|)\).

def poincareSeriesSecondCoefficient : Prop :=
  ∀ p : ℕ, p.Prime → ∀ (n : ℕ) (G : Subgroup (GL (Fin n) (ZMod p))),
    ∃ A B : Polynomial ℚ, B.eval 1 ≠ 0 ∧
      ((B * (1 - Polynomial.X) ^ n : Polynomial ℚ) : PowerSeries ℚ) * poincareSeries G =
        (A : PowerSeries ℚ) ∧
      (A.eval 1 * (Polynomial.derivative B).eval 1 - (Polynomial.derivative A).eval 1 * B.eval 1) /
          B.eval 1 ^ 2 = hyperplaneSum G / (2 * Nat.card G)

Uses 2 · Used by 1

Statement usesHyperplane sum · Poincaré series of the invariant ring

Used byBenson–Crawley-Boevey hyperplane formula (Kourovka 12.36)

TheoremBenson–Crawley-Boevey hyperplane formula (Kourovka 12.36)#●ready to prove

For every prime \(p\), every \(n \in \mathbb{N}\) and every subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{F}_p)\), with \(P(t)\) the Poincaré series of the invariant ring of \(G\) and \(r\) the hyperplane sum of \(G\), there are polynomials \(A, B \in \mathbb{Q}[t]\) with \(B(1) \ne 0\) and \(B(t) (1 - t)^n P(t) = A(t)\) in \(\mathbb{Q}[[t]]\) such that

\[\frac{A(1) B'(1) - A'(1) B(1)}{B(1)^2} = \frac{r}{2 |G|}.\]

That is, the Carlisle–Kropholler conjecture on the second Laurent coefficient holds: the coefficient \(a_{-n+1}\) in the expansion \(P(t) = \sum_{i \ge -n} a_i (1 - t)^i\) equals \(r / (2 |G|)\).

Resolved true: the Kourovka Archive records the conjecture as proved by Benson and Crawley-Boevey (Bull. London Math. Soc. 27 (1995)), with a second proof by Neeman (Comment. Math. Helv. 70 (1995)) based on the Grothendieck-Riemann-Roch theorem. Source: E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 12.36 (D. Carlisle, P. H. Kropholler); resolution: D. J. Benson and W. W. Crawley-Boevey, Bull. London Math. Soc. 27 (1995), no. 5, 435-440; A. Neeman, Comment. Math. Helv. 70 (1995), no. 3, 339-349, Kourovka Archive, Problem 12.36: the conjecture is proved.

public theorem_wanted poincareSeriesSecondCoefficient_holds : poincareSeriesSecondCoefficient

Uses 1

Statement usesCarlisle–Kropholler conjecture on the second Laurent coefficient (Kourovka 12.36)

7 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.