LemmaStatement: 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.

Generation in bounded degree presents an FI-module as a quotient of free FI-modules

Statement

Let $V$ be an FI-module over $k$ (The category FI and FI-modules over a commutative ring), with free FI-modules $M (m)$ as in The free FI-module $M (W)$ generated by an $S_{m}$ -module and span as in Span, finite generation and generation degree of an FI-module.

(a) For $v \in V_{m}$ the map of FI-modules $M (m) \to V$ sending the canonical generator ${i d}_{m} \in M (m)_{m}$ to $v$ has image ${span}_{V} (v)$ ; more generally, for any set $Σ$ of elements, each lying in some $V_{S}$ , the canonical map $⨁_{s \in Σ} M (S_{s}) \to V$ sending ${i d}_{S_{s}}$ to $s$ has image ${span}_{V} (Σ)$ . Here $S_{s}$ is the specified supporting set of $s$ , and $M (S)_{T}$ is the free $k$ -module on injections $S \to T$ , with postcomposition as transition maps. Each $M (S)$ is isomorphic to $M (∣ S ∣)$ after choosing a single bijection $[∣ S ∣] \to S$ .

(b) $V$ is finitely generated if and only if there is a finite family $m_{1}, \dots, m_{r} \geq 0$ with a surjection

$M (m_{1}) \oplus \dots \oplus M (m_{r}) ↠ V;$

$V$ is generated in degree $\leq d$ if and only if there is a surjection $⨁_{i \in I} M (m_{i}) ↠ V$ with $m_{i} \leq d$ for all $i$ . In particular, if $V$ is generated in degree $\leq d$ , then the evaluation map $⨁_{m \leq d} M (V_{m}) \to V$ , whose value on a summand $V_{T}$ supported on an $m$ -element subset $T \subseteq S$ is the transition map $V_{T} \to V_{S}$ , is surjective.

(c) If $V$ is finitely generated, then $V_{S}$ is a finitely generated $k$ -module for every finite set $S$ (Generated submodule, cyclic and finitely generated modules, module basis and free module).

No choice principle is used: all maps come from a finite or explicitly indexed set of generators, and the image computations are linear algebra on the values at a fixed finite set.

Facts & Assumptions

Given: An FI-module $V$ over $k$ , a set $Σ$ of elements with each element lying in some $V_{S}$ , and for each $m$ the free FI-module $M (m)$ with its canonical generator ${i d}_{m}$ .

[F1]

$M (m)_{S}$ has as $k$ -basis the injections $[m] ↪ S$ ; for a map of FI-modules $F ⁣ : M (m) \to V$ and the element $v = F ({i d}_{m}) \in V_{m}$ , naturality forces $F (f) = f_{*} (v)$ for an injection $f ⁣ : [m] ↪ S$ ; the module $M (m)$ represents the functor $V \mapsto V_{m}$ (The free FI-module $M (W)$ generated by an $S_{m}$ -module).

[F2]

${span}_{V} (Σ)$ is the smallest sub-FI-module of $V$ containing $Σ$ , and ${span}_{V} (Σ)_{T}$ is the $k$ -span of the elements $f_{*} (s)$ with $(S, s) \in Σ$ and $f ⁣ : S \to T$ a morphism of $F I$ ; $V$ is finitely generated when ${span}_{V} (Σ) = V$ for a finite $Σ$ , and generated in degree $\leq d$ when ${span}_{V} (V_{\leq d}) = V$ (Span, finite generation and generation degree of an FI-module).

[F3]

A direct summand inclusion and the coordinate maps of a direct sum are $k$ -linear, and the image of a direct sum of maps is the sum of the images (The direct sum of an indexed family of modules, Module homomorphism and isomorphism, kernel, image and cokernel).

[F4]

A quotient of a finitely generated $k$ -module is finitely generated, and a finitely generated free $k$ -module on a finite set is finitely generated (Generated submodule, cyclic and finitely generated modules, module basis and free module).

Proof

technique · direct

1.1F1F2given

For $v \in V_{m}$ let $F ⁣ : M (m) \to V$ correspond to $v$ under the representing property, so $F ({i d}_{m}) = v$ and $F (f) = f_{*} (v)$ for every injection $f ⁣ : [m] ↪ S$ [F1]. Then $im (F)_{S}$ is the $k$ -span of the elements $f_{*} (v)$ , which is exactly ${span}_{V} (v)_{S}$ by [F2]; hence $im (F) = {span}_{V} (v)$ .

2.1F2F3step 1.1

More generally, the map $⨁_{s \in Σ} M (S_{s}) \to V$ has image the sum of the images of its summands, and the summand indexed by $s \in V_{S}$ sends a basis injection $f : S \to T$ to $f_{*} (s)$ , so has image ${span}_{V} (s)$ by the same computation as step 1.1; hence the image is ${span}_{V} (Σ)$ by [F2, F3].

2.2F1F2step 1.1

The same argument with an arbitrary index set $I$ shows that $V$ is generated in degree $\leq d$ if and only if there is a surjection $⨁_{i \in I} M (m_{i}) \to V$ with all $m_{i} \leq d$ : the generators $v_{i}$ of the image lie in degrees $m_{i} \leq d$ , and conversely the skeletal generating set $V_{\leq d}$ produces a surjection from the sum of the $M (m)$ indexed by $(m, v)$ with $m \leq d$ and $v \in V_{m}$ . Separately, the adjunction defining $M$ gives the evaluation map $⨁_{m \leq d} M (V_{m}) \to V$ from the FB-module which agrees with $V$ on sets of cardinality $m$ and is zero elsewhere: its $V_{T}$ summand maps by the inclusion $T ↪ S$ . Its image consists of the transition images from degrees $\leq d$ and is therefore $V$ .

3.1F1F2step 2.1

If $V = {span}_{V} (Σ)$ for a finite $Σ$ , then the map of step 2.1 is surjective onto $V$ and the finitely many supporting sets can be transported to $[m_{i}]$ by finitely many bijections, giving generators $s_{1}, \dots, s_{r}$ with $s_{i} \in V_{m_{i}}$ , so $M (m_{1}) \oplus \dots \oplus M (m_{r}) ↠ V$ . Conversely, if $⨁_{i = 1}^{r} M (m_{i}) ↠ V$ is a surjection, let $v_{i}$ be the image of the canonical generator of the $i$ -th summand; step 2.1 identifies the image with ${span}_{V} (v_{1}, \dots, v_{r})$ , so this span is $V$ and $V$ is finitely generated.

4.1F1F4step 3.1

If $V$ is finitely generated, fix a surjection $M (m_{1}) \oplus \dots \oplus M (m_{r}) ↠ V$ from step 3.1. Evaluating at a finite set $S$ gives a surjection of $k$ -modules $M (m_{1})_{S} \oplus \dots \oplus M (m_{r})_{S} ↠ V_{S}$ , and each $M (m_{i})_{S}$ is free with the finite basis $Inj ([m_{i}], S)$ [F1]; a finite direct sum of finitely generated free modules is finitely generated, and its quotient $V_{S}$ is finitely generated by [F4]. This proves (c).

5.1step 1.1step 2.1step 3.1step 2.2step 4.1∎

Steps 1.1 and 2.1 prove (a); steps 3.1 and 2.2 prove (b), including the evaluation map; step 4.1 proves (c).

Depends on

Used by

Dependency tree · two levels

25 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)