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

Gluing fibre products along open covers

Statement

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.

Facts & Assumptions

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

[F1]

Suppose $P = X \times_{S} Y$ exists, with projections $p, q$ . If opens $V \subseteq X$ , $W \subseteq Y$ map into an open $U \subseteq S$ , then the open subscheme $Q = p^{- 1} (V) \cap q^{- 1} (W)$ represents $V \times_{U} W$ , and also $V \times_{S} W$ . Independently, for $f : X \to S$ and an open $U \subseteq S$ , the open subscheme $f^{- 1} (U)$ represents $X \times_{S} U$ . (Restricting fibre products to open subschemes)

[F2]

If $(P, p, q)$ and $(P^{'}, p^{'}, q^{'})$ are fibre products of the same pair $X \to S \leftarrow Y$ , there is a unique isomorphism $u : P \to P^{'}$ with $p^{'} u = p$ and $q^{'} u = q$ . (Uniqueness of the fibre product)

[F3]

Affine schemes equipped with open subschemes and isomorphisms on overlaps satisfying the identity and cocycle conditions glue to a scheme, uniquely up to unique isomorphism; the given affine schemes become an open affine cover. (Gluing affine schemes along compatible open isomorphisms)

[F4]

Compatible morphisms of schemes on an open cover of a scheme $X$ glue uniquely to a morphism from $X$ ; two morphisms out of $X$ are equal if their restrictions to an open cover are equal. Both assertions may be checked after affine-open refinement of source and target. (Morphisms of schemes are local on compatible open covers)

Proof

1.1

Let $P_{i j} \subseteq P_{i}$ be the inverse image of $Y_{i} \cap Y_{j}$ . By F1 it represents $X \times_{S} (Y_{i} \cap Y_{j})$ . F2 identifies it with the corresponding open in $P_{j}$ . The transition maps satisfy identity, inverse and cocycle identities: on each triple overlap both candidate maps have identical projections and are equal by uniqueness.

givenF1F2

2.1

To use F3 with exactly its affine hypothesis, cover each $P_{i}$ by affine opens. For two such charts use the open subset on which the preceding transition lands in the second chart; their isomorphisms are restrictions of those transitions. These are open subschemes, even when nonaffine, and their cocycles are already verified. F3 glues the affine charts to a scheme $P$ ; the charts belonging to $P_{i}$ glue back to $P_{i}$ . F4 glues the projection maps to $X, Y$ .

F3F4step 1.1

3.1

For a compatible pair $a : T \to X, b : T \to Y$ , cover $T$ by $T_{i} = b^{- 1} (Y_{i})$ . Each pair restricted to $T_{i}$ gives a unique map to $P_{i}$ . On $T_{i} \cap T_{j}$ both factor through $P_{i j}$ and agree by its universal property. F4 glues them to one map $T \to P$ . Any other such map has the same restrictions, proving uniqueness for arbitrary, possibly empty, $T$ . The empty cover of empty $Y$ gives $P = \emptyset$ .

F1F4step 1.1step 2.1

4.1

For a base cover, replace the local factors by $X_{i} = f^{- 1} (S_{i})$ and $Y_{i} = g^{- 1} (S_{i})$ . F1 describes the overlap over $S_{i} \cap S_{j}$ as the open inverse image in either local product. The same cocycle and affine refinement construction applies. A compatible pair from $T$ is glued on the inverse images of $S_{i}$ under its common composite to $S$ . A singleton cover changes nothing.

F1F2F3F4step 3.1∎

Depends on

Used by

Existence of all scheme fibre products Theorem

Dependency tree · two levels

12 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 proof 10.1.1 Steps 2–5 (standard reference, not scraped)