TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

An abelian scheme is the Neron model of its generic fibre

Statement

Assume AC and DC. Let $S$ be a Dedekind scheme with function field $K$ , and let $A \to S$ be an abelian scheme (Abelian schemes over a base). Then $A$ is a Neron model (Neron models, the Neron mapping property and weak Neron models) of its generic fibre $A_{K}$ : for every smooth $S$ -scheme $Y$ and every $K$ -morphism $u_{K} : Y_{K} \to A_{K}$ there is a unique $S$ -morphism $Y \to A$ extending $u_{K}$ .

Facts & Assumptions

Given: AC and DC, a Dedekind scheme $S$ with function field $K$ , an abelian scheme $A \to S$ , a smooth $S$ -scheme $Y$ , and a $K$ -morphism $u_{K} : Y_{K} \to A_{K}$ .

[F1]

For a smooth finite-type $S$ -scheme $Z$ , every $K$ -morphism $Z_{K} \to A_{K}$ extends uniquely to $Z \to A$ (K-morphisms from smooth models into abelian schemes extend uniquely).

[F2]

A smooth morphism is locally of finite presentation; over the locally Noetherian scheme $S$ , every point of a smooth $S$ -scheme has an open neighbourhood of finite type over $S$ (Smooth morphism of schemes, Locally Noetherian and Noetherian schemes).

[F3]

Two $S$ -morphisms from a flat $S$ -scheme to a separated $S$ -scheme agreeing on the generic fibre are equal. Indeed their equalizer is closed; on a chart over an affine integral open $Spec B \subseteq S$ , its ideal vanishes after tensoring with $K$ . Flatness makes the chart ring $B$ -torsion-free, so that ideal is zero. This argument uses the closed diagonal (Separated morphism of schemes) and generic localization (Scheme-theoretic fibre); it does not require the generic fibre to be open.

Proof

technique · apply the extension result for finite-type smooth tests, then cover an arbitrary smooth test by finite-type opens and glue using separatedness

1.1F1givenconstruct

First suppose $Y$ is of finite type over $S$ . Then [F1] gives the unique extension $u : Y \to A$ of $u_{K}$ . This proves the mapping property for finite-type smooth test schemes.

2.1F1F2F3step 1.1construct∎

For an arbitrary smooth $S$ -scheme $Y$ , use [F2] to cover it by open subschemes $Y_{i}$ of finite type over $S$ . Apply step 1.1 to each restriction $u_{K} ∣_{(Y_{i})_{K}}$ , obtaining $u_{i} : Y_{i} \to A$ . On an overlap $Y_{i} \cap Y_{j}$ , the maps agree on the schematically dense generic fibre, so they agree everywhere by [F3]. The $u_{i}$ glue to an $S$ -morphism $u : Y \to A$ extending $u_{K}$ . The same density and separatedness give uniqueness. Thus $A$ satisfies the full Neron mapping property; the weak property is a consequence, and no group law on a general model is constructed.

Depends on

Used by

Dependency tree · two levels

48 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

S. Bosch, W. Lutkebohmert, M. Raynaud, Neron Models (1990), 1.2/8 (an abelian scheme is a Neron model of its generic fibre) (standard reference, not scraped)