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
- Affine schemes and affine morphisms are separated Corollary
- Euler characteristic in a proper flat family is locally constant Corollary
- General hypersurfaces give smooth complete intersections Corollary
- Upper semicontinuity of fibre cohomology dimensions Corollary
- Affine morphisms are separated Lemma
- Base change and composition of affine morphisms Lemma
- Base change of immersions Lemma
- Dense relative-dimension strata in flat finitely presented fibres Lemma
- Every scheme diagonal is an immersion Lemma
- Finite decomposition around isolated fibre points after an elementary étale change Lemma
- Finite is affine and local on its target Lemma
- Finite morphisms survive base change and composition Lemma
- Finite neighbourhood of an isolated fibre point after elementary etale change Lemma
- Finite projective complex for proper flat coherent cohomology Lemma
- Flat field extension commutes with coherent cohomology Lemma
- Fpqc descent of properness components Lemma
- Glue relative spectra of affine-local algebras Lemma
- Gluing fibre products along open covers Lemma
- Points and topology of a fibre Lemma
- Quasi-separatedness and the diagonal Lemma
- Scheme Zariski Main factorization for separated quasi-finite morphisms Lemma
- Universal finite projective cohomology complex over any base Lemma
- Affine-overlap criterion for separatedness Theorem
- Bertini smoothness away from the base locus Theorem
- Classical products and scheme products Theorem
- Cohomology and base change for proper flat coherent families Theorem
- Generic smoothness over a dense target open Theorem
- High powers of an ample line bundle embed a proper scheme Theorem
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)