ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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 exterior square of the permutation FI-module has character polynomial $(\binom{X_{1}}{2}) - X_{2}$

Example

Let $V = M (1)$ be the permutation FI-module of The permutation FI-module has character polynomial $X_{1}$ , so $V_{S}$ is the free $k$ -module on $S$ and $V (f)$ is the linear extension of $f$ , and define $W_{S} : = Λ^{2} V_{S}$ with $W (f) : = Λ^{2} V (f)$ (The $k$ th exterior power as the tensor-power quotient by repeated-vector relations, The induced map $Λ^{k} T$ on exterior powers). Then $W$ is an FI-module (The category FI and FI-modules over a commutative ring) with $W_{n} ≅ Λ^{2} (k^{n})$ as an $S_{n}$ -module, and its character is the character polynomial

$(\binom{X_{1}}{2}) - X_{2}$

of weighted degree $2$ (Character polynomials in the cycle counts $X_{i}$ ): for every $n \geq 0$ and every $σ \in S_{n}$ the trace of $σ$ on $W_{n}$ equals $(\binom{X_{1} (σ)}{2}) - X_{2} (σ)$ , where $X_{1} (σ)$ is the number of fixed points and $X_{2} (σ)$ the number of $2$ -cycles (Support, fixed points, disjoint cycles, cycle length, disjoint-cycle decompositions, and cycle type). 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$ ; the permutation FI-module $V$ with $V_{S} = k^{(S)}$ and basis ${e_{s} : s \in S}$ ; and $W_{S} = Λ^{2} V_{S}$ with $W (f) = Λ^{2} V (f)$ .

[F1]

$V$ is an FI-module: $V ({i d}_{S}) = i d$ and $V (g \circ f) = V (g) V (f)$ ; $V ≅ M (1)$ and $V_{n} ≅ k^{n}$ is the permutation representation of $S_{n}$ (The category FI and FI-modules over a commutative ring, The permutation FI-module has character polynomial $X_{1}$ ).

[F2]

For a linear map $T ⁣ : V \to W$ , the exterior square $Λ^{2} T$ is induced by $T \otimes T$ on $V \otimes V$ and satisfies $Λ^{2} (g \circ f) = Λ^{2} (g) \circ Λ^{2} (f)$ and $Λ^{2} (i d) = i d$ ; $Λ^{2}$ is the quotient of $V^{\otimes 2}$ by the span of the tensors $v \otimes v$ (The induced map $Λ^{k} T$ on exterior powers, The $k$ th exterior power as the tensor-power quotient by repeated-vector relations).

[F3]

If $F$ is a finite free $R$ -module with ordered basis $e_{1}, \dots, e_{r}$ , the wedges $e_{i} \land e_{j}$ with $i < j$ form an $R$ -basis of the degree-two part $⋀^{2} F$ of the exterior algebra, which is the same quotient as $Λ^{2} F$ (Exterior Algebra Of A Finite Free Module, Exterior Algebra Basis Monomials, The $k$ th exterior power as the tensor-power quotient by repeated-vector relations).

[F4]

$X_{1} (σ)$ is the number $c_{1} (σ)$ of fixed points of $σ$ and, more generally, $X_{r} (σ) = c_{r} (σ)$ is the number of $r$ -element orbits; a partition of ${i, j}$ into orbits of $σ$ is either two $1$ -cycles or one $2$ -cycle (Character polynomials in the cycle counts $X_{i}$ , Support, fixed points, disjoint cycles, cycle length, disjoint-cycle decompositions, and cycle type).

[F5]

For a square matrix, the trace is the sum of the diagonal entries (The trace $tr (A)$ as the sum of the diagonal entries); the polynomial $(\binom{X_{1}}{2}) - X_{2} \in Q [X_{1}, X_{2}]$ has weighted degree $2$ .

Verification

technique · direct

1.1F1F2

$W$ is a functor: $W ({i d}_{S}) = Λ^{2} ({i d}_{V_{S}}) = {i d}_{W_{S}}$ and $W (g \circ f) = Λ^{2} (V (g) V (f)) = Λ^{2} V (g) \circ Λ^{2} V (f) = W (g) W (f)$ , using that $V$ satisfies the functor axioms [F1] and that $Λ^{2}$ preserves identities and composites [F2]; hence $W$ is an FI-module with values $W_{S} = Λ^{2} V_{S}$ , and for $S = [n]$ this is $W_{n} = Λ^{2} (k^{n})$ with the action induced by the permutation action of $S_{n}$ on $k^{n}$ .

1.2F3F4givenalgebra

Fix $n$ and $σ \in S_{n}$ . By [F3], applied to the free module $V_{n}$ with basis $e_{0}, \dots, e_{n - 1}$ , the elements $e_{i} \land e_{j}$ with $i < j$ form a $k$ -basis of $W_{n}$ ; and $σ \cdot (e_{i} \land e_{j}) = e_{σ (i)} \land e_{σ (j)}$ . Hence the diagonal entry of the matrix of $σ$ at the basis element $e_{i} \land e_{j}$ is the coefficient of $e_{i} \land e_{j}$ in $e_{σ (i)} \land e_{σ (j)}$ , which can be nonzero only when ${σ (i), σ (j)} = {i, j}$ . In that case $σ$ restricts to a bijection of the two-element set ${i, j}$ : it is either the identity, giving coefficient $+ 1$ , or the transposition $(i j)$ , giving $e_{j} \land e_{i} = - e_{i} \land e_{j}$ and coefficient $- 1$ . There is no other possibility, so the diagonal entry is $+ 1$ exactly for the unordered pairs of distinct fixed points of $σ$ , is $- 1$ exactly for the $2$ -cycles of $σ$ , and is $0$ otherwise.

2.1F4F5step 1.2

By [F5] the trace of $σ$ on $W_{n}$ is the sum of the diagonal entries computed in step 1.2, namely the number $(\binom{X_{1} (σ)}{2})$ of unordered pairs of distinct fixed points minus the number $X_{2} (σ)$ of $2$ -cycles: $tr (σ; W_{n}) = (\binom{X_{1} (σ)}{2}) - X_{2} (σ)$ . For $n = 0$ and $n = 1$ the module $W_{n}$ is $0$ and both sides are $0$ , since then $X_{1} (σ) \leq 1$ . This holds for every $n$ , and $(\binom{X_{1}}{2}) - X_{2}$ is a character polynomial of weighted degree $2$ , so the trace function of $W$ is given by that character polynomial.

3.1step 1.1step 1.2step 2.1∎

Steps 1.1, 1.2 and 2.1 show that $W = Λ^{2} V$ is an FI-module with $W_{n} ≅ Λ^{2} (k^{n})$ whose character is the weighted-degree-two character polynomial $(\binom{X_{1}}{2}) - X_{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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 exterior square of the permutation FI-module has character polynomial (X12)−X2(2X1​​)−X2​