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.

Uniqueness of the fibre product

Statement

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$ .

Facts & Assumptions

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

[F1]

Let $f : X \to S$ and $g : Y \to S$ be morphisms of schemes. A fibre product is a scheme $P$ , with projections $p : P \to X$ and $q : P \to Y$ , such that $f p = g q$ and, for every scheme $T$ and morphisms $a : T \to X$ , $b : T \to Y$ with $f a = g b$ , there is exactly one $h : T \to P$ satisfying $p h = a$ and $q h = b$ . Thus, naturally in every test scheme $T$ , $Hom (T, P) ≅ Hom (T, X) \times_{Hom (T, S)} Hom (T, Y) .$ Write $P = X \times_{S} Y$ . The commutative square with edges $p, q, f, g$ is Cartesian when it has this universal property. Morphisms here are morphisms of locally ringed spaces, as in def-morphism-of-schemes. No existence assertion is part of the definition. (Fibre product of schemes)

Proof

1.1

Apply the universal property of $P^{'}$ to the compatible maps $p, q$ . It supplies a unique map $u : P \to P^{'}$ with the required projections. This works also for $P = \emptyset$ .

givenF1

2.1

Apply the universal property of $P$ to $p^{'}, q^{'}$ to obtain $v : P^{'} \to P$ . Both $v u$ and ${id}_{P}$ have projections $p, q$ , so uniqueness gives $v u = {id}_{P}$ ; likewise $u v = {id}_{P^{'}}$ .

F1step 1.1

3.1

Thus $u$ is an isomorphism, and any projection-compatible isomorphism must equal the map already uniquely obtained. No condition on the number of points or on local nilpotents was used.

step 1.1step 2.1∎

Depends on

Fibre product of schemes

Used by

Dependency tree · two levels

2 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.3 and 10.1.5 (standard reference, not scraped)