CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Dimensions of finitely generated FI-modules are eventually polynomial

Statement

Let $k$ be a field of characteristic $0$ and let $V$ be a finitely generated FI-module over $k$ with finite-dimensional values, weight $d = weight (V)$ and stability degree $s = stab-deg (V)$ , with character polynomial $P_{V}$ as in Finitely generated FI-modules have eventual character polynomials (Weight of an FI-module over a field of characteristic zero, Injectivity, surjectivity and stability degree). Then

$\dim_{k} V_{n} = P_{V} (n, 0, 0, \dots)$

for every $n \geq s + d$ , the rational value on the right being read in $k$ through the prime field $Q \subseteq k$ ; in particular $\dim_{k} V_{n}$ is given by a polynomial in $n$ of degree at most $d$ for all sufficiently large $n$ (Character polynomials in the cycle counts $X_{i}$ ). No choice principle is used.

Facts & Assumptions

Given: A characteristic-zero field $k$ and a finitely generated FI-module $V$ over $k$ with finite-dimensional values, weight $d < \infty$ , stability degree $s < \infty$ and character polynomial $P_{V} \in Q [X_{1}, X_{2}, \dots]$ of weighted degree $\leq d$ satisfying $χ_{V_{n}} (σ) = P_{V} (X_{1} (σ), X_{2} (σ), \dots)$ for all $n \geq s + d$ and all $σ \in S_{n}$ (Finitely generated FI-modules have eventual character polynomials).

[F1]

For a finite-dimensional $k S_{n}$ -module the character value at the identity is the dimension: $χ_{V_{n}} ({i d}_{n}) = tr ({i d}_{n}; V_{n}) = \dim_{k} V_{n}$ (The trace $tr (A)$ as the sum of the diagonal entries).

[F2]

The identity permutation of $S_{n}$ has $X_{1} ({i d}_{n}) = n$ fixed points and $X_{i} ({i d}_{n}) = 0$ for every $i \geq 2$ (Character polynomials in the cycle counts $X_{i}$ , Support, fixed points, disjoint cycles, cycle length, disjoint-cycle decompositions, and cycle type).

[F3]

Evaluating a character polynomial $P \in Q [X_{1}, X_{2}, \dots]$ of weighted degree $\leq d$ at $(n, 0, 0, \dots)$ gives a polynomial in $n$ over $Q$ of degree at most $d$ : substitution is a ring homomorphism, and the surviving monomials are $X_{1}^{a_{1}}$ with $a_{1} \leq d$ (Character polynomials in the cycle counts $X_{i}$ ).

Proof

technique · direct

1.1F1F2given

Fix $n \geq s + d$ . By the character identity of Finitely generated FI-modules have eventual character polynomials applied to $σ = {i d}_{n}$ , and by [F1] and [F2], $\dim_{k} V_{n} = χ_{V_{n}} ({i d}_{n}) = P_{V} (X_{1} ({i d}_{n}), X_{2} ({i d}_{n}), \dots) = P_{V} (n, 0, 0, \dots)$ .

2.1F3step 1.1∎

By [F3] the function $n \mapsto P_{V} (n, 0, 0, \dots)$ is a polynomial over $Q$ of degree at most $d$ ; hence step 1.1 exhibits a polynomial of degree at most $d$ agreeing with $\dim_{k} V_{n}$ for every $n \geq s + d$ . This proves the claim.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Thomas Church, Jordan S. Ellenberg and Benson Farb, “FI-modules and stability for representations of symmetric groups”, arXiv:1204.4533v4 (2014); published in Duke Math. J. 164 (2015) 1833–1910 (standard reference, not scraped)
Thomas Church, Jordan S. Ellenberg, Benson Farb and Rohit Nagpal, “FI-modules over Noetherian rings”, Geom. Topol. 18 (2014) 2951–2984; author-hosted full text (standard reference, not scraped)