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

Increasing sequences of coherent subsheaves of a coherent module on a Noetherian scheme stabilize

Statement

Let $X$ be a Noetherian scheme and let $F$ be a coherent $O_{X}$ -module (Coherent module sheaves). If $F_{1} \subseteq F_{2} \subseteq F_{3} \subseteq \dots$ is an increasing sequence of coherent $O_{X}$ -submodules of $F$ , then the sequence stabilizes: there is an index $n_{0}$ with $F_{n} = F_{n_{0}}$ for every $n \geq n_{0}$ .

The proof inherits the Axiom of Choice through the affine quasi-coherent interface (Affine quasi-coherent sheaves are modules, The Axiom of Choice); apart from that interface it selects nothing and is otherwise choice-free.

Facts & Assumptions

[F1]

A scheme is Noetherian if and only if it has a finite affine open cover by spectra of Noetherian rings (Locally Noetherian and Noetherian schemes).

[F2]

On a locally Noetherian scheme a quasi-coherent module is coherent if and only if it is of finite type (Coherent sheaves on a locally Noetherian scheme); on an affine scheme $Spec A$ , finite type means that the module is isomorphic to $\tilde{M}$ for a finitely generated $A$ -module $M$ (Finite type and finitely presented module sheaves, Coherent module sheaves).

[F3]

For an affine scheme $U = Spec A$ , the functor $Γ (U, -)$ is an equivalence from quasi-coherent $O_{U}$ -modules to $A$ -modules with inverse $M \mapsto \tilde{M}$ (Affine quasi-coherent sheaves are modules, Quasi-coherent module on a scheme). An equivalence of abelian categories preserves and reflects monomorphisms, so a quasi-coherent subsheaf $G \subseteq H$ of a quasi-coherent sheaf on $U$ corresponds to the inclusion of $A$ -modules $Γ (U, G) \subseteq Γ (U, H)$ , and $G$ is recovered from its module of sections; thus two quasi-coherent subsheaves of $H$ with the same module of sections are equal.

[F4]

If $M$ is a finitely generated module over a Noetherian ring $A$ , then $M$ is a Noetherian module, so every ascending sequence of submodules of $M$ stabilizes (Finite modules over Noetherian rings are Noetherian, Finite generation, ACC, and maximal-condition characterizations of Noetherian modules, Noetherian modules: every submodule is finitely generated). This uses no choice principle.

Proof

Given: A Noetherian scheme $X$ , a coherent $O_{X}$ -module $F$ and an increasing sequence $F_{1} \subseteq F_{2} \subseteq \dots$ of coherent $O_{X}$ -submodules of $F$ .

1.1F1given

If $X = \emptyset$ there is nothing to prove, so assume $X \neq \emptyset$ . By [F1] fix a finite affine open cover $X = U_{1} \cup \dots \cup U_{r}$ with $U_{i} = Spec A_{i}$ and $A_{i}$ Noetherian; necessarily $r \geq 1$ . This is a single existential instantiation of the cover granted by the definition of a Noetherian scheme, not a choice from an infinite family.

2.1F2F3step 1.1

Fix $i$ . The restriction $F ∣_{U_{i}}$ is quasi-coherent, and it is of finite type because $F$ is coherent and the restriction of a coherent module to an open subscheme is coherent; by [F2] put $M_{i} : = Γ (U_{i}, F)$ , a finitely generated $A_{i}$ -module. Each $F_{n} ∣_{U_{i}}$ is likewise a coherent, hence finite type, quasi-coherent subsheaf of $F ∣_{U_{i}}$ , and $N_{i, n} : = Γ (U_{i}, F_{n})$ is a finitely generated $A_{i}$ -submodule of $M_{i}$ .

3.1F3step 2.1

For $m \leq n$ the inclusion $F_{m} \subseteq F_{n}$ induces, under the equivalence of [F3], an inclusion of $A_{i}$ -modules $N_{i, m} \subseteq N_{i, n}$ ; in particular $N_{i, 1} \subseteq N_{i, 2} \subseteq N_{i, 3} \subseteq \dots$ is an ascending sequence of submodules of $M_{i}$ .

4.1F4step 3.1

By [F4] the module $M_{i}$ is Noetherian, so the ascending sequence of step 3.1 stabilizes: there is an integer $s_{i}$ with $N_{i, n} = N_{i, s_{i}}$ for every $n \geq s_{i}$ . This holds for each fixed $i$ with no choice used.

5.1F3step 1.1step 4.1algebra∎

Set $s : = \max {s_{1}, \dots, s_{r}}$ , which exists because $r$ is finite. Let $n \geq s$ . For every $i$ we have $N_{i, n} = N_{i, s}$ , both being $N_{i, s_{i}}$ , so the quasi-coherent subsheaves $F_{n} ∣_{U_{i}}$ and $F_{s} ∣_{U_{i}}$ of $F ∣_{U_{i}}$ have the same module of sections and are therefore equal by [F3]. Equality of subsheaves of a quasi-coherent sheaf can be checked on the members of an open cover, and the $U_{i}$ cover $X$ ; hence $F_{n} = F_{s}$ for every $n \geq s$ , which is the asserted stabilization with $n_{0} = s$ .

Depends on

Used by

Regularization of a one-dimensional integral curve with finite normalization by point blowups Theorem

Dependency tree · two levels

46 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

The Stacks Project, tag 0BI4 (Lemma 54.15.1) (standard reference, not scraped)
The Stacks Project, tag 01Y8 (Lemma 30.10.1) (standard reference, not scraped)