Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13
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.

Rp is local with unique maximal ideal pRp

Statement

Let p be a prime ideal of a commutative ring R. Then Rp is a nonzero local ring. Its unique maximal ideal is pRp={r/s:rp, sp}, and its units are exactly the fractions r/s with rp.

Facts & Assumptions

Given: A commutative ring R and a prime ideal p.

[F1]

The denominators of Rp are the elements outside p (Localisation at a prime ideal: Rp=(Rp)1R).

[F2]

A fraction r/s is a unit exactly when ar belongs to the denominator set for some aR (A fraction r/s is a unit in S1R exactly when arS for some aR).

[F3]

Fractions satisfy r/s=r/s exactly when some denominator u annihilates rsrs; in particular, a fraction vanishes exactly when some denominator annihilates its numerator (Equality, vanishing, and the kernel of the localisation map).

[F4]

A local ring is a nonzero commutative ring with a unique maximal ideal (A local ring is a nonzero commutative ring with a unique maximal ideal).

Proof

technique · direct
1.1

The ring is nonzero: if 1/1=0, [F3] gives up with u=0, impossible because 0p.

F1F3
1.2

By [F2], if rp, then r/s is a unit by taking a=1. If rp and ar lay outside p, the ideal property would be contradicted; hence r/s is not a unit. Thus the displayed set is exactly the set of nonunits.

F1F2
1.3

Membership in the displayed set is independent of the chosen fraction: if r/s=r/s with rp, then [F3] gives up with u(rsrs)=0. Hence urs=ursp; primality and u,sp force rp.

F1F3algebra
2.1

The displayed set is an ideal: common-denominator addition and multiplication by arbitrary fractions preserve numerator membership in p. It is proper because 1p, so 1/1 is not in it. Every proper ideal contains only nonunits, so step 1.2 makes every proper ideal lie inside it. It is therefore the unique maximal ideal, and [F4] makes Rp local.

F4step 1.2step 1.3algebra

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 26 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources