CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31

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.

The integral closure of a Dedekind domain in a finite separable extension is Dedekind

Statement

Assume the Axiom of Choice. Let $R$ be a Dedekind domain with fraction field $F$ , let $L / F$ be a finite separable field extension, and let $A$ be the integral closure of $R$ in $L$ . Then $A$ is a Dedekind domain.

Facts & Assumptions

Given: A Dedekind domain $R$ with fraction field $F$ , a finite separable extension $L / F$ , and the integral closure $A$ of $R$ in $L$ .

[F1]

A Dedekind domain is a Noetherian integrally closed domain of dimension $1$ (Dedekind domains).

[L1]

The integral closure $A$ is a finite $R$ -module (Finite separable integral closures over normal Noetherian domains are module-finite).

[L2]

Assuming Choice, an injective integral extension of nonzero commutative rings preserves Krull dimension (Injective integral extensions preserve Krull dimension).

Proof

technique · direct

1.1

By [L1], the ring $A$ is a finite $R$ -module, hence integral over $R$ . Since $R$ is Noetherian by [F1], every ideal of $A$ is an $R$ -submodule of the finite $R$ -module $A$ , so $A$ is Noetherian. If $x \in Frac (A) \subseteq L$ is integral over $A$ , then transitivity of integrality makes $x$ integral over $R$ , so the defining property of $A$ forces $x \in A$ . Thus $A$ is integrally closed.

F1L1givenalgebra

1.2

The inclusion $R \subseteq A$ is an injective integral extension of nonzero domains. Since [F1] gives $\dim R = 1$ , [L2] gives $\dim A = 1$ .

F1L1L2given

2.1

Steps 1.1 and 1.2 show that $A$ is a Noetherian integrally closed domain of dimension $1$ . Hence [F1] makes $A$ a Dedekind domain.

F1step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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, A Primer of Commutative Algebra, §20 (standard reference, not scraped)
Mircea Mustata, Introduction to Commutative Algebra, §8.5 (standard reference, not scraped)