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 VX, WY map into an open US, then the open subscheme Q=p1(V)q1(W) represents V×UW, and also V×SW. Independently, for f:XS and an open US, the open subscheme f1(U) represents X×SU.

Facts & Assumptions

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

[F1]

Let f:XS and g:YS be morphisms of schemes. A fibre product is a scheme P, with projections p:PX and q:PY, such that fp=gq and, for every scheme T and morphisms a:TX, b:TY with fa=gb, there is exactly one h:TP 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:UX 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 XSY, there is a unique isomorphism u:PP with pu=p and qu=q. (Uniqueness of the fibre product)

Proof

1.1

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

givenF1F2
2.1

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

F3F4step 1.1
3.1

For the last assertion, a compatible pair a:TX,b:TU has a(T)f1(U). Its unique open factorization is a map to f1(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.

F2F3

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