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.

The graph is a pullback of the diagonal

Statement

For an $S$ -morphism $u : X \to Y$ , put $H = (u {pr}_{X}, {pr}_{Y}) : X \times_{S} Y \to Y \times_{S} Y$ . The square with top arrow $Γ_{u} : X \to X \times_{S} Y$ , bottom arrow $Δ_{Y / S} : Y \to Y \times_{S} Y$ , left arrow $u$ , and right arrow $H$ is Cartesian.

Facts & Assumptions

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

[F1]

For an $S$ -morphism $u : X \to Y$ (as in def-scheme-over-base), the graph morphism is $Γ_{u} = ({id}_{X}, u) : X \to X \times_{S} Y$ , supplied by thm-fibre-products-of-schemes-exist. Its first projection is the identity and its second projection is $u$ . The definition alone does not assert that its image is closed. (The graph morphism over a base)

[F2]

For $X \to S$ , the diagonal morphism is the unique $Δ_{X / S} : X \to X \times_{S} X$ satisfying ${pr}_{1} Δ_{X / S} = {id}_{X} = {pr}_{2} Δ_{X / S}$ . It exists by thm-fibre-products-of-schemes-exist. For any test scheme $T$ , it takes an $S$ -morphism $a : T \to X$ to the compatible pair $(a, a)$ . (The diagonal morphism)

[F3]

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)

Proof

1.1givenF1F2

By F1 and F2 both composites around the square are $(u, u)$ . A compatible test pair consists of $a : T \to X \times_{S} Y$ and $c : T \to Y$ satisfying $H a = Δ c$ . Write $a = (a_{X}, a_{Y})$ . Equality means exactly $u a_{X} = c$ and $a_{Y} = c$ .

2.1F1F3step 1.1∎

Thus $a_{X}$ is the unique map $T \to X$ whose graph composite is $a$ and whose $u$ -composite is $c$ . Conversely any map $d : T \to X$ supplies the pair $((d, u d), u d)$ . These operations are inverse, so the square has the pullback universal property, with its canonical uniqueness as in F3. The argument includes empty schemes and $u = id$ , and imposes no reducedness or separation hypothesis.

Depends on

Used by

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 proof 11.1.18, diagram (11.1.18.1), p.232 (standard reference, not scraped)