CorollaryStatement: 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.

Assuming the Axiom of Choice, a local ring $R$ is canonically isomorphic to $R_{m}$ at its maximal ideal

Statement

Assume the Axiom of Choice. If $(R, m)$ is a local ring, its localisation map $λ : R ⟶ R_{m}$ is a ring isomorphism. Its inverse sends $r / s$ to $r s^{- 1}$ .

Facts & Assumptions

Given: A local ring $(R, m)$ .

[F1]

In a local ring, the unique maximal ideal is exactly the set of nonunits (Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of $x$ and $1 - x$ is a unit for every $x$ ).

[F2]

The denominators in $R_{m}$ are the elements of $R ∖ m$ (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ ).

[F3]

Any map that inverts all denominators extends uniquely through the localisation (Universal property of localisation: maps that invert $S$ factor uniquely through $S^{- 1} R$ ).

Proof

technique · direct universal-property argument

1.1

By [F1] and [F2], every denominator is already a unit in $R$ . Applying [F3] to ${id}_{R}$ gives $g : R_{m} \to R$ with $g (r / s) = r s^{- 1}$ and $g λ = {id}_{R}$ .

F1F2F3

2.1

Both $λ g$ and ${id}_{R_{m}}$ compose with $λ$ to give $λ$ . The uniqueness clause of [F3] gives $λ g = {id}_{R_{m}}$ , so $λ$ is an isomorphism with inverse $g$ .

F3step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 30 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

The Stacks Project, Section 10.18: Local rings (standard reference, not scraped)

Assuming the Axiom of Choice, a local ring RR is canonically isomorphic to RmRm​ at its maximal ideal