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 exists, with projections . If opens , map into an open , then the open subscheme represents , and also . Independently, for and an open , the open subscheme represents .
Facts & Assumptions
Given: The objects, hypotheses and conventions in the statement above.
Let and be morphisms of schemes. A fibre product is a scheme , with projections and , such that and, for every scheme and morphisms , with , there is exactly one satisfying and . Thus, naturally in every test scheme , Write . The commutative square with edges 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)
A morphism is an open immersion if it identifies isomorphically with an open subscheme of . (Open immersions of schemes)
An open immersion is a monomorphism of schemes, and a composite of open immersions is an open immersion. (Open immersions are monomorphisms)
If and are fibre products of the same pair , there is a unique isomorphism with and . (Uniqueness of the fibre product)
Proof
Given compatible maps over , their composites to agree. F1 gives a unique . Its image lies in , so the morphism factors uniquely through that open subscheme by restriction of its sheaf map.
Conversely a map gives maps to agreeing in ; they agree in because is a monomorphism. The two constructions are inverse, including empty opens and the full opens. F4 supplies the canonical identification with any other product.
For the last assertion, a compatible pair has . Its unique open factorization is a map to ; its composite to is 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
- Stacks 26.17.3; Vakil proof 10.1.1 Step 1 (standard reference, not scraped)