CorollaryStatement: 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.

Good reduction supplies a Neron model

Statement

Assume AC and DC. Let $S$ be a Dedekind scheme with function field $K$ and let $A_{K}$ be an abelian variety over $K$ with good reduction over $S$ (Good reduction of an abelian variety over a Dedekind scheme). Then $A_{K}$ admits a Neron model over $S$ , namely any abelian scheme model $A \to S$ of $A_{K}$ , and this model is unique up to a unique $S$ -isomorphism inducing the specified identity on $A_{K}$ . In particular, for a discrete valuation ring $R$ with fraction field $K$ , every abelian variety over $K$ with good reduction has a Neron model over $R$ , and that Neron model is proper and smooth over $R$ .

Facts & Assumptions

Given: AC and DC, a Dedekind scheme $S$ with function field $K$ , an abelian variety $A_{K} / K$ with good reduction, and an abelian scheme model $A \to S$ of $A_{K}$ .

[F1]

By definition of good reduction there is an abelian scheme $A \to S$ with $A \times_{S} Spec K ≅ A_{K}$ (Good reduction of an abelian variety over a Dedekind scheme).

[F2]

An abelian scheme over a Dedekind scheme is a Neron model of its generic fibre, and Neron models are unique up to a unique isomorphism over the generic fibre (An abelian scheme is the Neron model of its generic fibre, Neron models, the Neron mapping property and weak Neron models).

Proof

technique · direct

1.1F1F2givenalgebra

Let $A \to S$ be an abelian scheme model of $A_{K}$ , supplied by [F1]. By [F2] $A$ satisfies the Neron mapping property; since $A \to S$ is smooth, separated and of finite type, it is a Neron model of $A_{K}$ .

2.1F2step 1.1algebra∎

Any two Neron models of $A_{K}$ are related by a unique $S$ -isomorphism inducing the specified identity on $A_{K}$ , by the uniqueness clause of [F2], so the model is unique up to unique isomorphism over the specified generic fibre; it is proper and smooth because it is an abelian scheme. In the DVR case the same statement applies to $S = Spec R$ .

Depends on

Used by

Dependency tree · two levels

21 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 and 1.3/1 (good reduction and Neron models) (standard reference, not scraped)