TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Existence of all scheme fibre products

Statement

Every diagram $X \to S \leftarrow Y$ of schemes has a fibre product. Given an affine cover $S = ⋃_{i} Spec A_{i}$ and affine covers $f^{- 1} (Spec A_{i}) = ⋃_{j} Spec B_{i j}$ and $g^{- 1} (Spec A_{i}) = ⋃_{k} Spec C_{i k}$ , the product has open affine cover $Spec (B_{i j} \otimes_{A_{i}} C_{i k}) .$

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

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)

[F2]

Let $X \to S \leftarrow Y$ be given. If $Y = ⋃_{i} Y_{i}$ is an open cover and every $P_{i} = X \times_{S} Y_{i}$ exists, these products glue along their inverse images over $Y_{i} \cap Y_{j}$ to a fibre product $X \times_{S} Y$ . There is also a base-cover version: if $S = ⋃_{i} S_{i}$ and $f^{- 1} (S_{i}) \times_{S_{i}} g^{- 1} (S_{i})$ exists for every $i$ , these products glue to $X \times_{S} Y$ . No overlap is required to be affine. (Gluing fibre products along open covers)

Proof

1.1givenF1F2

When $X, S$ are affine, cover $Y$ by affines. Each local product exists by F1, so F2 glues them to the desired product, with the displayed affine charts.

2.1F2step 1.1

When only $S$ is affine, cover $X$ by affine opens. The preceding construction gives each product of one of these opens with $Y$ . Interchanging the roles of the two projections in F2 glues them. This interchange is justified directly by the symmetric compatible-pair condition, without needing a later associativity result.

3.1F1F2step 2.1∎

For arbitrary $S$ , apply the preceding result over each affine $Spec A_{i}$ , and then use the base-cover clause of F2. Its overlap construction makes the stated tensor spectra an open cover. Empty schemes and zero tensor rings give empty charts, and the empty-base case forces both factors to be empty.

Depends on

Used by

Products and initial and terminal S-schemes Corollary
Base change of objects, morphisms and properties Definition
Geometric fibre functor and étale fundamental group Definition
Group schemes of finite type over a field Definition
Group schemes over a base scheme Definition
Relative projective space from standard charts Definition
The diagonal morphism Definition
The graph morphism over a base Definition
A split affine extension of an abelian variety Example
The diagonal of the affine line Example
A tangent direction is realized by a local smooth curve Lemma
A transverse hyperplane slice is smooth at the chosen point Lemma
Affine charts after extension of the ground field Lemma
Affine-local graded algebras glue their Proj charts Lemma
Closed graphs over separated targets Lemma
Closed subgroup schemes are detected on all algebra-valued points Lemma
Every representable functor is an algebraic space Lemma
Finite morphisms survive base change and composition Lemma
Fpqc descent of properness components Lemma
Local finiteness conditions under base change Lemma
Monomorphisms and diagonals Lemma
Points of a fibre product via residue-field tensors Lemma
Products preserve smoothness Lemma
Properness survives composition Lemma
Pushouts of closed immersions exist Lemma
Quasi-compactness is local on the target and survives base change Lemma
Separated morphisms compose Lemma
Structure sheaf of a quasi-compact quasi-separated morphism is affine-local Lemma
Symmetry, associativity and units Lemma
Tangent spaces of products over a field Lemma
The invariant differentials of a group scheme Lemma
The submersion criterion between smooth varieties Lemma
The tangent space at the identity is a vector space, and Lie is a functor Lemma
The universal member away from the base locus Lemma
Classical products and scheme products Theorem
Equalizers into separated schemes are closed Theorem
Generic smoothness over a dense target open Theorem
Projective n-space has quasi-coherent cohomological dimension at most n Theorem
Submersion criterion for locally standard smooth morphisms Theorem

Dependency tree · two levels

9 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

Vakil Theorem 10.1.1, complete proof; Stacks 26.17.4 (standard reference, not scraped)