CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

$R_{p} / p R_{p} ≅ Frac (R / p)$ is the residue field at $p$

Statement

For a prime ideal $p$ of a commutative ring $R$ , there is a canonical field isomorphism $R_{p} / p R_{p} ≅ Frac (R / p), r / s + p R_{p} ⟼ (r + p) / (s + p) .$ This quotient is the residue field of the local ring $R_{p}$ .

Facts & Assumptions

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

[F1]

Localisation commutes with quotients by the displayed fraction isomorphism (Localisation commutes with quotient rings: $S^{- 1} R / S^{- 1} I ≅ {\overset{ˉ}{S}}^{- 1} (R / I)$ ).

[F2]

The ring $R_{p}$ is local with maximal ideal $p R_{p}$ ( $R_{p}$ is local with unique maximal ideal $p R_{p}$ ).

[F3]

The quotient $R / p$ is an integral domain because $p$ is prime ( $R / P$ is an integral domain if and only if $P$ is a prime ideal).

[F4]

The localisation of a domain at all of its nonzero elements is its field of fractions and is a field ( $Frac (D)$ is a field and $d \mapsto d / 1$ embeds the integral domain $D$ ).

Proof

technique · direct

1.1F1

Apply [F1] with $S = R ∖ p$ and $I = p$ . The image of $S$ in $R / p$ is exactly $(R / p) ∖ {0}$ : a class $s + p$ is nonzero exactly when $s \notin p$ .

2.1F1F2F3F4step 1.1∎

By [F3] and [F4], localisation at that image is $Frac (R / p)$ and is a field. The formula is the formula from [F1], while [F2] identifies the source quotient as the residue field of $R_{p}$ .

Depends on

Dependency tree · 2 levels

Sources

The Stacks Project, Section 10.18: Local rings