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.
Fibrewise constant morphisms from an abelian scheme factor through the base
Statement
Assume AC and DC. Let be an abelian scheme (Abelian schemes over a base), let be any morphism, write with structure morphism and unit section , and let be any scheme. If a morphism sends each geometric fibre of to a single point, then as morphisms .
Facts & Assumptions
Given: AC and DC, an abelian scheme , a morphism , a scheme and a morphism which is constant on geometric fibres over .
is an isomorphism for every base change, with inverse evaluation along the identity section (Universal structure-sheaf sections of an abelian scheme, assuming AC and DC).
A proper morphism has closed image, and properness is stable under base change; the base change is proper (Proper morphisms are closed, Properness survives arbitrary base change, Abelian schemes over a base).
Morphisms into an affine scheme correspond to ring maps on global sections (Morphisms to an affine scheme and global sections).
Proof
Fix and choose an affine open containing the image point of the fibre ; this is possible because the fibre image is a single point. The complement is closed, and since is proper by [F2] the set has closed image in ; by construction that image misses . Choose an affine neighbourhood of disjoint from the image; then for is closed in and disjoint from , so lands in . Thus over an affine neighbourhood of every point the map factors through an affine target.
On the structure morphism is proper and the restriction corresponds by [F3] to a ring map . The universal-sections lemma [F1] identifies , so this ring map factors through and defines a morphism with . Evaluating along the unit section gives , so .
The local factorizations of step 2.1 agree on overlaps: on both and equal evaluated there, because restricted to the unit section is an isomorphism onto the base; hence they glue to a morphism with , and by the same evaluation. Therefore . This controls nilpotents: the factorization is an identity of morphisms, not merely of geometric points.
Depends on
- The Axiom of Choice
- The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain
- Abelian schemes over a base
- Universal structure-sheaf sections of an abelian scheme
- Proper morphisms are closed
- Properness survives arbitrary base change
- Morphisms to an affine scheme and global sections
Used by
Dependency tree · two levels
36 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
- J. S. Milne, Abelian Varieties, v2.00 (2008), Chapter I sections 3, 5, 8 (rigidity) (standard reference, not scraped)