LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Flat base change for quasi-coherent surface cohomology by Čech

Statement

Assume AC and DC. For a quasi-compact separated scheme $X$ over a ring $A$ , a quasi-coherent sheaf $F$ and a flat $A$ -algebra $C$ , the canonical maps $H^{q} (X, F) \otimes_{A} C \to H^{q} (X_{C}, F_{C})$ are isomorphisms for every $q$ . No flatness of $F$ over $A$ is required.

Facts & Assumptions

Given: A quasi-compact separated scheme $X$ over a ring $A$ , a quasi-coherent sheaf $F$ on $X$ , and a flat $A$ -algebra $C$ .

[F1]

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $F$ all of whose members are nonempty, there exists a function $g$ with domain $F$ satisfying $g (S) \in S$ for all $S \in F$ . (The Axiom of Choice)

[F2]

def-dependent-choice. Let $X$ be a set and let $R \subseteq X \times X$ be a binary relation on $X$ . Call $R$ entire on $X$ when $for every x \in X there is y \in X with x R y .$ The Axiom of Dependent Choice, written $D C$ , is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F3]

thm-affine-fibre-product-tensor-ring. Let $A \to B$ and $A \to C$ be maps of commutative unital rings, allowing the zero ring. In the category of all schemes, $Spec B \times_{Spec A} Spec C ≅ Spec (B \otimes_{A} C) .$ The projections correspond to $b \mapsto b \otimes 1$ and $c \mapsto 1 \otimes c$ . (Affine fibre products are spectra of tensor products)

[F4]

thm-affine-quasi-coherent-equivalence. Assume the Axiom of Choice (The Axiom of Choice). Let $A$ be a commutative ring with $1$ and put $X = Spec A$ . Let ${Mod}_{A}$ be the category of $A$ -modules and $QCoh (X)$ the full subcategory of $O_{X}$ -modules consisting of the quasi-coherent ones (def-quasi-coherent-module-scheme). (Affine quasi-coherent sheaves are modules)

[F5]

thm-cech-computes-qc-cohomology-separated-scheme-affine-cover. Assume the Axiom of Choice, inherited from sheaf cohomology. Let $X$ be a quasi-compact separated scheme (def-separated-morphism-schemes), let $U_{0}, \dots, U_{r}$ be a finite affine open cover of $X$ and let $F$ be a quasi-coherent $O_{X}$ -module (def-quasi-coherent-module-scheme). (Cech cohomology computes quasi-coherent cohomology on a separated scheme)

Proof

1.1F5given

Choose a finite affine open cover $U_{1}, \dots, U_{n}$ of $X$ , which exists because $X$ is quasi-compact; since $X$ is separated, every finite intersection $U_{i_{0} \dots i_{q}}$ is affine.

2.1F5step 1.1

By the comparison theorem for the derived functor cohomology of a quasi-coherent sheaf on a separated scheme, the Cech complex $C^{∙} ({U_{i}}, F)$ built from the affine intersections computes $H^{q} (X, F)$ for every $q$ .

3.1F3F4step 1.1step 2.1

For the base change $X_{C} = X \times_{Spec A} Spec C$ the preimages $V_{i} = U_{i} \times_{Spec A} Spec C$ form an affine cover with the same index set, each intersection $V_{i_{0} \dots i_{q}}$ is affine with coordinate ring $B_{i_{0} \dots i_{q}} \otimes_{A} C$ , and the sections of $F_{C}$ there are $Γ (U_{i_{0} \dots i_{q}}, F) \otimes_{A} C$ by the affine tensor formula and the affine quasi-coherent equivalence.

4.1F4step 3.1

Consequently the Cech complex of the base change is the tensor product of complexes $C^{∙} ({V_{i}}, F_{C}) ≅ C^{∙} ({U_{i}}, F) \otimes_{A} C$ , degreewise, with the boundary maps obtained by tensoring the original ones with the identity of $C$ .

5.1F4step 2.1step 4.1

Tensoring with the flat $A$ -algebra $C$ preserves kernels, images and their quotients, so taking cohomology commutes with the base change: $H^{q} (C^{∙} ({V_{i}}, F_{C})) ≅ H^{q} (C^{∙} ({U_{i}}, F)) \otimes_{A} C$ ; combined with the comparison isomorphisms of step 2.1 this gives $H^{q} (X_{C}, F_{C}) ≅ H^{q} (X, F) \otimes_{A} C$ canonically.

6.1F1F2step 5.1∎

All identifications used are restrictions along the cover and tensor maps, so they are natural in $F$ and compatible with the boundary maps; in particular, for a prime $p \subset A$ , flat localization gives $H^{q} (X, F)_{p} ≅ H^{q} (X \times_{A} Spec A_{p}, F_{A_{p}})$ . The cohomology on the right is that of the base-changed scheme, rather than that of $Spec A_{p}$ . The Axiom of Choice and the Axiom of Dependent Choice are inherited from the cohomology suppliers.

Remarks

No flatness of $F$ over $A$ is needed: only the flatness of $C$ over $A$ enters, in step 5.1.
The Cech route avoids any derived-category machinery; separatedness makes all finite intersections affine, which is what makes the complex available.

Depends on

Used by

Dependency tree · two levels

36 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, Resolution of Surfaces, Sections 54.8–54.9: complete source arguments with local prerequisite replacements (standard reference, not scraped)