Alphabeta Math
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.

Restricting fibre products to open subschemes

Statement

Suppose P=X×SY exists, with projections p,q. If opens V⊆X, W⊆Y map into an open U⊆S, then the open subscheme Q=p−1(V)∩q−1(W) represents V×UW, and also V×SW. Independently, for f:X→S and an open U⊆S, the open subscheme f−1(U) represents X×SU.

Facts & Assumptions

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

[F1]

Let f:X→S and g:Y→S be morphisms of schemes. A fibre product is a scheme P, with projections p:P→X and q:P→Y, such that fp=gq and, for every scheme T and morphisms a:T→X, b:T→Y with fa=gb, there is exactly one h:T→P satisfying ph=a and qh=b. Thus, naturally in every test scheme T, Hom⁡(T,P)≅Hom⁡(T,X)×Hom⁡(T,S)Hom⁡(T,Y). Write P=X×SY. 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)

[F2]

A morphism j:U→X is an open immersion if it identifies U isomorphically with an open subscheme of X. (Open immersions of schemes)

[F3]

An open immersion is a monomorphism of schemes, and a composite of open immersions is an open immersion. (Open immersions are monomorphisms)

[F4]

If (P,p,q) and (P′,p′,q′) are fibre products of the same pair X→S←Y, there is a unique isomorphism u:P→P′ with p′u=p and q′u=q. (Uniqueness of the fibre product)

Proof

1.1givenF1F2

Given compatible maps T→V,T→W over U, their composites to S agree. F1 gives a unique T→P. Its image lies in Q, so the morphism factors uniquely through that open subscheme by restriction of its sheaf map.

2.1F3F4step 1.1

Conversely a map T→Q gives maps to V,W agreeing in S; they agree in U because U→S is a monomorphism. The two constructions are inverse, including empty opens and the full opens. F4 supplies the canonical identification with any other product.

3.1F2F3∎

For the last assertion, a compatible pair a:T→X,b:T→U has a(T)⊆f−1(U). Its unique open factorization is a map to f−1(U); its composite to U is b by the monomorphism property. Conversely such a factorization gives the pair. This argument does not assume any general existence theorem.

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