ExampleConstruction: Literature-sourcedVerification: 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.

The permutation FI-module has character polynomial $X_{1}$

Example

For every finite set $S$ let $V_{S}$ be the free $k$ -module on $S$ , and for an injection $f ⁣ : S \to S^{'}$ let $V (f)$ be the linear extension of $f$ . Then $V$ is an FI-module (The category FI and FI-modules over a commutative ring), isomorphic to $M (1)$ in the notation of The free FI-module $M (W)$ generated by an $S_{m}$ -module; it satisfies $V_{n} ≅ k^{n}$ with the permutation action of $S_{n}$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation) and is generated by $V_{{0}}$ in degree $\leq 1$ (Span, finite generation and generation degree of an FI-module). Its character is the character polynomial $X_{1}$ of weighted degree $1$ (Character polynomials in the cycle counts $X_{i}$ ): for every $n \geq 0$ and every $σ \in S_{n}$ the trace $tr (σ; V_{n})$ (The trace $tr (A)$ as the sum of the diagonal entries) equals $X_{1} (σ)$ , the number of fixed points of $σ$ . No choice principle is used.

The displayed integer-valued expression is first evaluated on the integer cycle counts and then mapped to $k$ by $Z \to k$ . This convention also covers positive characteristic; rational polynomial coefficients are not reduced individually when their denominators vanish in $k$ .

Facts & Assumptions

Given: A field $k$ and, for every finite set $S$ , the free $k$ -module $V_{S}$ on $S$ with its basis ${e_{s} : s \in S}$ , and for an injection $f ⁣ : S \to S^{'}$ the $k$ -linear extension $V (f) (e_{s}) : = e_{f (s)}$ .

[F1]

An FI-module over $k$ is a covariant functor from finite sets and injections to $k$ -modules; functoriality means $V ({i d}_{S}) = {i d}_{V_{S}}$ and $V (g \circ f) = V (g) \circ V (f)$ (The category FI and FI-modules over a commutative ring).

[F2]

For $m \geq 0$ , $M (m)_{S}$ has as $k$ -basis the injections $[m] ↪ S$ , the transition map along $g ⁣ : S \to S^{'}$ sends the basis injection $u$ to $g \circ u$ , and $M (1)$ represents the functor $V \mapsto V_{[1]}$ (The free FI-module $M (W)$ generated by an $S_{m}$ -module).

[F3]

For a set $Σ$ of supported elements $(S, s)$ with $s \in V_{S}$ , ${span}_{V} (Σ)_{T}$ is the $k$ -span of the elements $f_{*} (s)$ with $(S, s) \in Σ$ and $f ⁣ : S \to T$ an injection; $V$ is generated in degree $\leq d$ when ${span}_{V} (V_{\leq d}) = V$ (Span, finite generation and generation degree of an FI-module).

[F4]

$X_{1}$ is the class function with $X_{1} (σ) = c_{1} (σ)$ , the number of fixed points of $σ$ ; it has weighted degree $1$ (Character polynomials in the cycle counts $X_{i}$ ).

[F5]

The trace of a square matrix is the sum of its diagonal entries; for $n = 0$ the empty matrix has trace $0$ (The trace $tr (A)$ as the sum of the diagonal entries).

Verification

technique · direct

1.1F1givenalgebra

$V$ is a functor: $V ({i d}_{S})$ sends each basis element $e_{s}$ to $e_{s}$ , hence is the identity, and for composable injections $f ⁣ : S \to T$ , $g ⁣ : T \to U$ one has $V (g \circ f) (e_{s}) = e_{g (f (s))} = V (g) (e_{f (s)}) = V (g) V (f) (e_{s})$ on every basis element, so $V (g \circ f) = V (g) V (f)$ ; hence $V$ is an FI-module with basis $S$ of $V_{S}$ .

2.1F2step 1.1

Identify $V_{S}$ with $M (1)_{S}$ by sending the basis element $e_{s}$ to the injection $u_{s} ⁣ : [1] \to S$ with $u_{s} (0) = s$ ; this is a $k$ -linear isomorphism because the $u_{s}$ are exactly the basis injections of $M (1)_{S}$ [F2]. It is compatible with transition maps: for $f ⁣ : S \to S^{'}$ , $M (1) (f) (u_{s}) = f \circ u_{s} = u_{f (s)}$ corresponds to $e_{f (s)} = V (f) (e_{s})$ . Hence $V ≅ M (1)$ ; in particular $V_{n} ≅ k^{n}$ with basis $[n]$ , and $σ \in S_{n}$ acts by $σ \cdot e_{s} = e_{σ (s)}$ , the permutation representation.

2.2F3step 1.1

The element $e_{0} \in V_{[1]}$ generates: for any finite set $S$ and $s \in S$ , the injection $u_{s} ⁣ : [1] \to S$ satisfies $(u_{s})_{*} (e_{0}) = e_{u_{s} (0)} = e_{s}$ , so ${span}_{V} ({([1], e_{0})})$ contains every basis element and equals $V$ ; thus $V$ is generated in degree $\leq 1$ by $V_{{0}}$ .

3.1F4F5step 2.1

For $σ \in S_{n}$ and basis elements $s, t \in [n]$ , the coefficient of $e_{t}$ in $σ \cdot e_{s} = e_{σ (s)}$ is $δ_{t, σ (s)}$ ; the diagonal entry at $s$ is therefore $δ_{s, σ (s)}$ , equal to $1$ if $σ$ fixes $s$ and to $0$ otherwise. By [F5], $tr (σ; V_{n}) = \sum_{s \in [n]} δ_{s, σ (s)}$ , the number of fixed points of $σ$ , which is $X_{1} (σ)$ ; for $n = 0$ both sides are $0$ . This holds for every $n$ , so the trace function of $V_{n}$ is the character polynomial $X_{1}$ on the whole range.

4.1step 1.1step 2.1step 2.2step 3.1∎

Steps 1.1, 2.1 and 2.2 exhibit $V ≅ M (1)$ as the permutation FI-module generated in degree $\leq 1$ , and step 3.1 identifies its character with $X_{1}$ , a character polynomial of weighted degree $1$ .

Depends on

Used by

The exterior square of the permutation FI-module has character polynomial C(X₁, 2)-X₂ Example

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)
I. G. Macdonald, Symmetric Functions and Hall Polynomials, 2nd ed., Oxford Mathematical Monographs, 1995 (author-hosted full text) (standard reference, not scraped)

The permutation FI-module has character polynomial X1X1​