Alphabeta MathHow 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.
Every abelian variety over a field is projective
Statement
Assume the Axiom of Choice. Every abelian variety over every field is projective over that field. Neither perfectness of the field nor a polarization is an assumption.
Facts & Assumptions
An abelian variety is a proper smooth geometrically integral group variety. (Abelian varieties over a field)
Every smooth geometrically integral separated finite-type group scheme over a field has an ample invertible sheaf, under AC. (A smooth geometrically integral algebraic group has an ample line bundle)
On a proper finite-type scheme over a Noetherian base with an ample line bundle, sufficiently high powers define a closed immersion into projective space over that base, under AC. (High powers of an ample line bundle embed a proper scheme)
Proof
Given: AC, a field , and an abelian variety .
By [F1], satisfies every hypothesis of [F2], so there is an ample invertible sheaf on . Its construction in [F2] uses the divisor and étale parameter-family proof of Stacks 0BF7; it does not use Barsotti–Chevalley or Milne's unproved projectivity statement.
Apply [F3] with base , which is Noetherian and has ample structure sheaf. Properness and finite type come from [F1]. A sufficiently high tensor power therefore gives a closed immersion . This is projectivity over . AC is inherited from [F2] and [F3], and the construction worked over itself even when the field was imperfect.
Depends on
Used by
- The theorem of the cube for an abelian variety Lemma
- Barsotti-Chevalley existence over an arbitrary field, allowing nonsmooth affine kernel Theorem
- Barsotti-Chevalley over a perfect field: unique smooth affine normal subgroup Theorem
- Nonzero multiplication on an abelian variety is finite and faithfully flat Theorem
Dependency tree · two levels
59 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 Project, Lemma 39.9.2, with 39.8.7 and 37.50.1 (standard reference, not scraped)
- Stacks Project, Lemma 37.50.1 (standard reference, not scraped)