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

Products and initial and terminal S-schemes

Statement

For every scheme $S$ , the category of $S$ -schemes has binary products $X \times_{S} Y$ , terminal object $S \overset{i d}{\to} S$ , and initial object $\emptyset \to S$ . A product with the empty scheme is empty. Disjoint unions, including the empty disjoint union, are coproducts of $S$ -schemes.

Facts & Assumptions

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

[F1]

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}) .$ (Existence of all scheme fibre products)

[F2]

An $S$ -scheme is a scheme $X$ equipped with a morphism $X \to S$ . An $S$ -morphism $X \to Y$ is a scheme morphism commuting with the maps to $S$ . For $n \geq 0$ , choose an affine open cover $S = ⋃_{i} Spec A_{i}$ . Over each chart take $Spec A_{i} [t_{1}, \dots, t_{n}]$ . On overlaps, localization in the coefficients gives canonical isomorphisms that fix the variables; these satisfy the cocycle condition and glue by thm-gluing-affine-schemes. The result, independent of the cover up to the unique $S$ -isomorphism respecting the coefficient maps and the ordered coordinate functions $t_{1}, \dots, t_{n}$ , is the relative affine space $A_{S}^{n}$ . Its structure morphism is affine, although its total scheme need not be affine when $S$ is not. For $n = 0$ it is $S$ ; for $S = \emptyset$ the construction gives the empty scheme. The uniqueness assertion concerns these coordinate-compatible identifications, not arbitrary $S$ -isomorphisms. (Schemes and morphisms over a base)

Proof

1.1

By F2, a map over $S$ is exactly a map commuting with structure maps. Therefore the fibre product supplied by F1 is a categorical product of $S$ -schemes. A map from $X$ to the terminal candidate $S$ over $S$ is forced to equal its structure morphism.

givenF1F2

2.1

The empty scheme has exactly one morphism to every scheme, since both its underlying map and all its sheaf data are unique. Conversely a map into the empty scheme exists only for an empty source. Thus the empty scheme satisfies the initial property, and compatible pairs into $X$ and $\emptyset$ are represented by $\emptyset$ . This includes $S = \emptyset$ .

step 1.1given

3.1

The topological disjoint union of schemes, with the structure sheaf specified separately on each component, is a scheme because every component is open and has its original affine charts. Maps out of it are exactly independent component maps, including their sheaf maps, so it is the coproduct over $S$ . For zero components it is empty and for one component it is that component.

F2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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 10.1.1 and 10.1.A (empty gluing specialization) (standard reference, not scraped)