LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Affine pushforward algebra localizes

Statement

Let $f : X \to S$ be an affine morphism. For every affine open $U = Spec R \subseteq S$ , write $f^{- 1} (U) = Spec B$ and let $φ : R \to B$ be the ring map induced by $f$ on this chart. Then there is a canonical isomorphism of $O_{U}$ -algebras

(f_{*} O_{X}) ∣_{U} ≅ \tilde{B},

where $\tilde{B}$ is the sheaf associated to the $R$ -module $B$ on $Spec R$ . For every $r \in R$ its sections on the principal open $D (r)$ are canonically

Γ (D (r), (f_{*} O_{X}) ∣_{U}) ≅ B_{φ (r)},

and for $D (s) \subseteq D (r)$ the restriction map is the canonical localization $B_{φ (r)} \to B_{φ (s)}$ . Consequently $f_{*} O_{X}$ is affine-locally module-associated in the sense of Affine-local quasi-coherent algebras before general sheaf theory.

Facts & Assumptions

Given: A scheme morphism $f : X \to S$ that is affine, an affine open $U = Spec R \subseteq S$ , and an affine presentation $f^{- 1} (U) = Spec B$ .

[F1]

An affine morphism is one whose inverse image of every affine open of the target is affine; the empty scheme is affine (Affine morphisms).

[F2]

A scheme is a locally ringed space, so its structure sheaf is a sheaf (Schemes).

[F3]

Direct image is defined on an open $V$ by $(f_{*} F) (V) = F (f^{- 1} (V))$ , with restrictions induced by those of $F$ (Direct image of a sheaf along a continuous map).

[F4]

If $j : U ↪ S$ is open, then for an open $V \subseteq U$ the sections of a restricted sheaf satisfy $(F ∣_{U}) (V) = F (V)$ (Restriction of a sheaf to an open subspace).

[F5]

A morphism of ringed spaces includes the structure-sheaf map $f^{♯} : O_{S} \to f_{*} O_{X}$ (Morphisms of ringed spaces).

[F6]

On $Spec R$ , the sets $D (r)$ are a basis of open sets, and $D (r) \cap D (s) = D (r s)$ (The underlying space of an affine spectrum).

[F7]

Every morphism between affine schemes is induced by a unique ring map in the opposite direction (Affine schemes are contravariantly equivalent to commutative rings).

[F8]

For a ring map $φ : R \to B$ , the induced spectrum map sends $q$ to $φ^{- 1} (q)$ and its structure-sheaf map on $D (r)$ is $R_{r} \to B_{φ (r)}$ (The map of affine spectra induced by a ring homomorphism).

[F9]

The canonical map $Spec (B_{φ (r)}) \to D_{B} (φ (r))$ is an isomorphism of locally ringed spaces (A principal localization identifies its spectrum with a distinguished open).

[F10]

For an affine spectrum, sections on a principal open are the corresponding localization, and restriction between principal opens is the canonical localization map (Sections and restrictions on distinguished opens of an affine scheme).

[F11]

A sheaf has unique gluing for compatible sections on every open cover, including the empty cover (A sheaf on a topological space).

[F12]

For an $R$ -algebra $B$ with structure map $φ : R \to B$ , the standard associated module sheaf on $Spec R$ has sections $B [φ (r)^{- 1}]$ on $D (r)$ and the canonical localization restrictions; the affine-local module-associated condition uses these identifications (Affine-local quasi-coherent algebras before general sheaf theory).

Proof

technique · direct

1.1F1F7

Fix one affine open $U = Spec R \subseteq S$ . By [F1], its inverse image is affine; choose an affine presentation $f^{- 1} (U) = Spec B$ . The restricted morphism is therefore a morphism between affine schemes, so [F7] gives its unique ring map $φ : R \to B$ . This argument fixes one chart at a time and makes no simultaneous choice of presentations over a cover.

1.2F6F8F9

For $r \in R$ and $q \in Spec B$ , [F8] gives $q \in f^{- 1} (D_{R} (r)) ⟺ r \notin φ^{- 1} (q) ⟺ φ (r) \notin q .$ Thus $f^{- 1} (D_{R} (r)) = D_{B} (φ (r))$ . By [F9], this open is identified with $Spec (B_{φ (r)})$ .

2.1F3F4F5F8F10step 1.2

By [F3] and [F4], the direct-image sheaf restricted to $U$ has sections $Γ (D_{R} (r), (f_{*} O_{X}) ∣_{U}) = Γ (f^{- 1} (D_{R} (r)), O_{X}) .$ Using the affine presentation and step 1.2, [F10] identifies this ring with $B_{φ (r)}$ . The structure map from $O_{U}$ is, on these sections, the localization of $φ$ from $R_{r}$ to $B_{φ (r)}$ by [F5] and [F8]. Hence this isomorphism respects the $O_{U}$ -algebra structures.

2.2F3F6F8F10F12step 1.2

If $U = \emptyset$ , then $D_{R} (1) = \emptyset$ and [F10] gives $R = Γ (\emptyset, O_{U}) = 0$ . If $f^{- 1} (U) = \emptyset$ , then $D_{B} (1) = \emptyset$ and [F10] gives $B = Γ (\emptyset, O_{X}) = 0$ . For $r = 0$ , $D_{R} (r) = \emptyset$ , $φ (r) = 0$ , and step 1.2 identifies its inverse image with $D_{B} (0) = \emptyset$ ; [F10] and [F12] give the zero ring on both sides. For $r = 1$ , $D_{R} (r) = U$ , $φ (r) = 1$ , and both sides give $B$ by [F10] and [F12]. No injectivity, flatness, reducedness, or finite-type condition on $φ$ is used.

3.1F3F10F12step 1.2step 2.1

If $D_{R} (s) \subseteq D_{R} (r)$ , [F12] says that restriction on the associated module sheaf is $B_{φ (r)} \to B_{φ (s)}$ by localization. For the direct image, [F3] identifies the restriction with that of $O_{X}$ along $f^{- 1} (D_{R} (s)) \subseteq f^{- 1} (D_{R} (r))$ ; [F10] makes this the same localization map under the identifications in step 2.1. Therefore the principal-open identifications commute with every restriction.

4.1F2F3F6F11F12step 2.1step 3.1

Because $O_{X}$ is a sheaf by [F2], [F3] and [F11] show that $f_{*} O_{X}$ is a sheaf: an open cover pulls back to an open cover, and compatible sections glue uniquely on the inverse image. The standard associated module sheaf in [F12] is also a sheaf. The principal opens form a basis by [F6]. Therefore the compatible isomorphisms of steps 2.1 and 3.1 determine an isomorphism on every open subset of $U$ : restrict sections to all principal opens contained in that subset, identify the resulting compatible families, and glue uniquely in both sheaves by [F11]. Thus $(f_{*} O_{X}) ∣_{U} ≅ \tilde{B}$ as $O_{U}$ -algebras.

5.1F12step 4.1

Since $U$ was arbitrary, this chartwise description and its principal-open localization maps are exactly the condition in [F12]. Hence $f_{*} O_{X}$ is affine-locally module-associated.

6.1F1F11step 1.1step 4.1∎

The argument is choice-free: step 1.1 fixes one affine chart at a time, and the sheaf gluing in step 4.1 is unique.

Depends on

Used by

Affine morphisms are relative spectra Theorem

Dependency tree · two levels

32 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

Stacks Project, Morphisms of Schemes, §29.11 Lemma 29.11.3 (standard reference, not scraped)
Stacks Project, Schemes, §26.5 Definition 26.5.3 and Lemma 26.5.4 (standard reference, not scraped)