Alphabeta Math
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.

9 results · all verified · 4 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Dedekind Domains and Ideal Classes Examples

1 · Prerequisites

2 · Summary

These examples work through the standard concrete consequences of the Dedekind package: PIDs and semilocal Dedekind domains, explicit fractional-ideal arithmetic in Z, localizations at a prime, the two-generator construction, and the divisor/class translation. The final example also records a singular one-dimensional domain where local principality fails, so invertibility fails with it.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Every nonfield PID is a Dedekind domain with trivial class group

Example

Assume the Axiom of Choice. Every principal ideal domain that is not a field is a Dedekind domain, and its ideal class group is trivial.

Facts & Assumptions

Given: A principal ideal domain R that is not a field.

[F1]

In a principal ideal domain every ideal is principal (Principal ideal domain).

[L1]

Every principal ideal domain is Noetherian (Every principal ideal domain is Noetherian).

[L2]

A nonfield Noetherian domain is Dedekind exactly when every nonzero proper ideal is locally principal (Equivalent local characterizations of Dedekind domains).

[L3]

A Dedekind domain is a PID exactly when its class group is trivial (A Dedekind domain is a PID exactly when its class group is trivial).

Verification

technique · direct
1.1

By [F1], every nonzero proper ideal of R is principal, hence remains principal after localising at any maximal ideal. The ring is Noetherian by [L1], so [L2] makes R a Dedekind domain.

F1L1L2
2.1

Now [L3] applies to the Dedekind domain R and gives that its class group is trivial.

L3step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-31Open item page →

A semilocal Dedekind domain is a PID

Example

Assume the Axiom of Choice.

Let R be a Dedekind domain with only finitely many maximal ideals. Then R is a principal ideal domain.

Facts & Assumptions

Given: The Axiom of Choice and a Dedekind domain R whose distinct maximal ideals are m1,,mr.

[L1]

Every nonzero ideal of R has a unique prime-power factorization (Unique factorization of nonzero fractional ideals into prime powers).

[L2]

The Chinese remainder theorem solves simultaneous congruences modulo the pairwise comaximal powers mini+1 (Chinese remainder theorem for pairwise comaximal ideals).

[L3]

A Dedekind domain is a PID exactly when its class group is trivial (A Dedekind domain is a PID exactly when its class group is trivial).

Verification

technique · direct
1.1

Let I=i=1rmini be a nonzero ideal by [L1]. For each i, choose ximinimini+1. By [L2], there exists xR with xxi(modmini+1) for each i. Then x has valuation exactly ni at mi for every i, and there are no other primes to consider. Hence (x)=I by uniqueness in [L1].

L1L2givenchoose
2.1

Every nonzero ideal of R is therefore principal, so [L3] identifies R as a PID.

L3step 1.1
ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passaudited 2026-08-31Open item page →

A fractional ideal of the integers with positive and negative prime exponents

Example

In Z, the fractional ideal

I:=1235Z

has factorization

I=(2)2(3)(5)1(7)1.

Facts & Assumptions

Given: The domain Z and the fractional ideal I=(12/35)Z.

[F1]

A fractional ideal is a bounded nonzero submodule of the fraction field (Fractional ideals).

[L1]

Nonzero fractional ideals of a Dedekind domain factor uniquely into prime powers (Unique factorization of nonzero fractional ideals into prime powers).

Verification

technique · direct
1.1

The ideal I is fractional because 35I=12ZZ, so [F1] applies.

F1given
2.1

In the PID Z, the principal ideal generated by 12/35 records the usual prime factorization of the numerator and denominator. Hence the exponents are 2 at (2), 1 at (3), 1 at (5), and 1 at (7), with all others zero. By [L1] this is exactly the prime-ideal factorization of I.

L1step 1.1algebra
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-31Open item page →

Computing an inverse fractional ideal explicitly

Example

In R=Z, let I=(2/3)Z. Then

(R:I)=(3/2)Z,

and therefore I(R:I)=R.

Facts & Assumptions

Given: The fractional ideal I=(2/3)Z of R=Z.

[F1]

The inverse candidate is defined by (R:I)={xQ:xIR} (Products, colons, and inverse candidates for fractional ideals).

[L1]

Fractional ideals factor uniquely into prime powers (Unique factorization of nonzero fractional ideals into prime powers).

Verification

technique · direct
1.1

An element xQ lies in (R:I) exactly when x(2/3)Z, equivalently when x(3/2)Z. Thus (R:I)=(3/2)Z.

F1givenalgebra
2.1

Multiplying the displayed generators gives (2/3)(3/2)=1, so I(R:I)=Z. This agrees with the valuation description from [L1].

L1step 1.1algebra
ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passaudited 2026-08-31Open item page →

A rank-two module and its ideal-class label

Example

Assume the Axiom of Choice. Let R be a Dedekind domain and let I be an invertible fractional ideal. Then the module

M:=RI

is a finite torsion-free module of rank 2, and under the class-group identification its second summand contributes the class [I]Cl(R).

Facts & Assumptions

Given: A Dedekind domain R and an invertible fractional ideal I.

[L1]

Every finite torsion-free Dedekind module splits as a finite direct sum of invertible fractional ideals (Finite torsion-free Dedekind modules split into invertible ideal summands).

[L2]

The ideal class group agrees with the Picard group of rank-one projectives (The ideal class group is the Picard group of rank-one projectives).

Verification

technique · direct
1.1

The module M=RI is already displayed as a direct sum of two invertible ideal summands, so it is finite torsion-free and fits the decomposition pattern of [L1].

L1given
2.1

Under the identification of [L2], the free summand R contributes the neutral Picard class and the other summand contributes exactly the class of I. Thus the rank-two module M is labelled by the same ideal class [I].

L2step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Localizing a Dedekind domain at a nonzero prime

Example

Let R be a Dedekind domain, let p be a nonzero prime ideal, and let n0 be an integer. Then Rp is a DVR, and

(pn)p=pnRp.

Hence vp(pn)=n.

Facts & Assumptions

Given: A Dedekind domain R, a nonzero prime ideal p, and an integer n0.

[L1]

The localisation Rp is a discrete valuation ring (Localizing a Dedekind domain at a nonzero prime gives a DVR).

[F1]

The valuation vp(I) is defined by the equality Ip=pvp(I)Rp (Prime-ideal valuations on fractional ideals).

Verification

technique · direct
1.1

By [L1], the localisation Rp is a DVR. Localising the ideal pn gives exactly pnRp by the definition of localisation of ideals.

L1given
2.1

Comparing step 1.1 with [F1] shows that the corresponding valuation is vp(pn)=n.

F1step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

Constructing two generators for a Dedekind ideal

Example

Let I be a nonzero ideal in a Dedekind domain R, and choose 0aI. Then the proof of the two-generator theorem constructs an element bI such that I=(a,b) by correcting only the finitely many prime valuations at which (a) is too large.

Facts & Assumptions

Given: A Dedekind domain R, a nonzero ideal I, and a chosen nonzero element aI.

[L1]

Every nonzero ideal of a Dedekind domain is generated by the chosen element a together with one further element bI (Every nonzero ideal in a Dedekind domain is generated by two elements).

Verification

technique · direct
1.1

The theorem [L1] identifies a finite set of bad primes, namely those for which vp(a)>vp(I), chooses local correction terms at those primes, and combines them by the Chinese remainder step in its proof.

L1given
2.1

The resulting element bI has exactly the missing prime valuations, so (a,b)=I. This is the concrete content of the two-generator construction.

L1step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31Open item page →

The divisor and class of a fractional ideal

Example

Assume the Axiom of Choice.

In R=Z, the fractional ideal

I:=409Z=(2)3(5)(3)2

has divisor

div(40/9)=3[(2)]+[(5)]2[(3)],

and its ideal class is trivial.

Facts & Assumptions

Given: The Axiom of Choice, the Dedekind domain R=Z, and the fractional ideal I=(40/9)Z.

[L1]

For xQ×, the principal-divisor sequence sends x to the valuation vector of (x) and then sends that divisor to the trivial class of (x) (The principal-divisor exact sequence for a Dedekind domain).

Verification

technique · direct
1.1

The generator 40/9 contributes prime exponents 3 at (2), 1 at (5), and 2 at (3), so div(40/9) is the displayed valuation vector.

L1givenalgebra
2.1

Because I is principal, its class is zero in the class group by [L1].

L1step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-31Open item page →

A noninvertible ideal in a singular one-dimensional domain

Example

Assume the Axiom of Choice. Let k be a field, let R:=k[t2,t3]k(t), and let m=(t2,t3). Then R is a one-dimensional domain that is not Dedekind, and m is not an invertible ideal.

Facts & Assumptions

Given: A field k, the cusp ring R=k[t2,t3] inside k(t), and its maximal ideal m=(t2,t3).

[L1]

A nonzero finitely generated fractional ideal is invertible exactly when all maximal localisations are principal (Equivalent characterizations of invertible fractional ideals).

[L2]

Assuming Choice, injective integral extensions preserve Krull dimension (Injective integral extensions preserve Krull dimension).

Verification

technique · direct
1.1

The inclusion Rk[t] is integral because t satisfies the monic equation X2t2=0 with coefficient t2R. The ring k[t] is a one-variable polynomial ring over a field, hence a nonfield principal ideal domain and therefore one-dimensional. Thus [L2] gives dimR=1. The same monic equation shows that t is integral over R, but tR, so R is not integrally closed and therefore is not Dedekind.

L2givenalgebra
2.1

In the local ring Rm one has mm2=(t4,t5,t6)Rm. If t2 lay in mm2, we could write t2=(at4+bt5+ct6)/s with a,b,cR and sm, so s=t2(a+bt+ct2)m, contradiction. Hence t2mmmm2. If mm were principal, say mm=aRm, then t2=au for some uRm. Because t2mm2=amm, the element u is a unit, so mm=t2Rm. But then t3mm implies t=t3/t2Rm, impossible: if t=r/s with rR and sm, then r=ts would have a linear t-term while elements of R=k[t2,t3] have no such term. Therefore mm is not principal.

step 1.1givenalgebra
3.1

Since mm is not principal, [L1] shows that m is not invertible.

L1step 2.1

Sources