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

Tensor products of finitely generated FI-modules are finitely generated

Statement

Let $V$ and $W$ be FI-modules over a commutative ring $k$ , with pointwise tensor product $(V \otimes W)_{S} : = V_{S} \otimes_{k} W_{S}$ and transition maps $f_{*} \otimes f_{*}$ . If $V$ and $W$ are finitely generated, then $V \otimes W$ is finitely generated; more precisely, if $V$ is generated in degree $\leq m_{1}$ and $W$ in degree $\leq m_{2}$ (Span, finite generation and generation degree of an FI-module), then $V \otimes W$ is generated in degree $\leq m_{1} + m_{2}$ . No choice principle is used.

Facts & Assumptions

Given: FI-modules $V, W$ over $k$ and the pointwise tensor product $V \otimes W$ .

[F1]

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

[F2]

$M (m)_{S}$ has as $k$ -basis the injections $[m] ↪ S$ (The free FI-module $M (W)$ generated by an $S_{m}$ -module); if $M$ has basis $(x_{i})$ and $N$ has basis $(y_{j})$ then $M \otimes_{k} N$ has basis $(x_{i} \otimes y_{j})$ (The elementary tensors of two bases form the product basis of the tensor product).

[F3]

$V$ is generated in degree $\leq d$ if and only if there is a surjection $⨁_{i \in I} M (m_{i}) ↠ V$ with all $m_{i} \leq d$ ; in particular finitely generated modules admit finite surjections $⨁_{i = 1}^{r} M (m_{i}) ↠ V$ (Generation in bounded degree presents an FI-module as a quotient of free FI-modules).

[F4]

Tensoring a surjection with the identity of a module yields a surjection, and tensor products distribute over direct sums: $(⨁_{i} A_{i}) \otimes_{k} (⨁_{j} B_{j}) ≅ ⨁_{i, j} (A_{i} \otimes_{k} B_{j})$ naturally, so a tensor product of sums of surjections is a surjection from the sum of the pairwise tensor products (Tensoring is right exact, Tensor products commute with arbitrary direct sums, The tensor product $M \otimes_{R} N$ from the additive group underlying the free $Z$ -module on $M \times N$ , elementary tensors, and finite tensor sums).

Proof

technique · direct

1.1givenalgebra

$V \otimes W$ is an FI-module: $(V \otimes W) ({i d}_{S}) = {i d}_{V_{S}} \otimes {i d}_{W_{S}} = {i d}_{V_{S} \otimes W_{S}}$ , and $(g \circ f)_{*} \otimes (g \circ f)_{*} = (g_{*} \otimes g_{*}) (f_{*} \otimes f_{*})$ for composable injections; the pointwise tensor product of $k$ -linear maps and the functor axioms in each variable give the claim.

2.1F1F2step 1.1

Let $U : = M (m_{1}) \otimes M (m_{2})$ , with $(U)_{S}$ having $k$ -basis the pairs $(f_{1}, f_{2})$ of injections $f_{1} ⁣ : [m_{1}] ↪ S$ , $f_{2} ⁣ : [m_{2}] ↪ S$ [F2]. For a basis element $(f_{1}, f_{2})$ , put $T : = im (f_{1}) \cup im (f_{2}) \subseteq S$ , so $∣ T ∣ \leq m_{1} + m_{2}$ ; the maps $f_{i}$ factor as $f_{i} = ι \circ g_{i}$ with $g_{i} ⁣ : [m_{i}] ↪ T$ injective and $ι ⁣ : T ↪ S$ the inclusion, and functoriality gives $(f_{1}, f_{2}) = (ι_{*} \otimes ι_{*}) (g_{1}, g_{2})$ with $(g_{1}, g_{2}) \in U_{T}$ . Hence every basis element of $U_{S}$ lies in the span of the images of the $U_{T}$ with $∣ T ∣ \leq m_{1} + m_{2}$ , so ${span}_{U} (U_{\leq m_{1} + m_{2}}) = U$ by [F1]: $U$ is generated in degree $\leq m_{1} + m_{2}$ .

2.2F3F4step 1.1

Now let $V$ be generated in degree $\leq m_{1}$ and $W$ in degree $\leq m_{2}$ , so that by [F3] there are surjections $⨁_{i \in I} M (m_{i}) ↠ V$ and $⨁_{j \in J} M (n_{j}) ↠ W$ with $m_{i} \leq m_{1}$ , $n_{j} \leq m_{2}$ . Tensoring them pointwise and distributing the direct sums [F4] gives a surjection $⨁_{i, j} (M (m_{i}) \otimes M (n_{j})) ↠ V \otimes W$ .

3.1F1step 2.1step 2.2

Each summand $U_{i j} : = M (m_{i}) \otimes M (n_{j})$ is generated in degree $\leq m_{i} + n_{j} \leq m_{1} + m_{2}$ by step 2.1, hence so is their direct sum; and a quotient of a module generated in degree $\leq d$ is generated in degree $\leq d$ , because the image of $span (U_{\leq d}) = U$ under a surjective map of FI-modules is $span$ of the images of $U_{\leq d}$ , which is the whole quotient. Therefore $V \otimes W$ , being a quotient of the sum of the $U_{i j}$ , is generated in degree $\leq m_{1} + m_{2}$ .

4.1F1F3step 3.1∎

If $V$ and $W$ are finitely generated, they are generated in degrees $\leq m_{1}$ and $\leq m_{2}$ for suitable finite $m_{1}, m_{2}$ , and [F3] allows finite index sets $I, J$ in step 2.2. For each pair $(i, j)$ , the finitely many basis pairs of injections into the finitely many sets $[t]$ with $t \leq m_{i} + n_{j}$ generate $M (m_{i}) \otimes M (n_{j})$ by step 2.1 and transport by a bijection $[∣ T ∣] \to T$ . Their union over the finite $I \times J$ is finite and its image generates $V \otimes W$ ; hence $V \otimes W$ is finitely generated, with the stated degree bound.

Depends on

Used by

Murnaghan stability for Kronecker coefficients Theorem

Dependency tree · two levels

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