Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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:r∈p, s∉p}, and its units are exactly the fractions r/s with r∉p.

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=(R∖p)−1R).

[F2]

A fraction r/s is a unit exactly when ar belongs to the denominator set for some a∈R (A fraction r/s is a unit in S−1R exactly when ar∈S for some a∈R).

[F3]

Fractions satisfy r/s=r′/s′ exactly when some denominator u annihilates rs′−r′s; 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 u∉p with u=0, impossible because 0∈p.

F1F3
1.2

By [F2], if r∉p, then r/s is a unit by taking a=1. If r∈p 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 r∈p, then [F3] gives u∉p with u(rs′−r′s)=0. Hence ur′s=urs′∈p; primality and u,s∉p force r′∈p.

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 1∉p, 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 · 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