ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

$Z_{(p)}$ consists of rationals with denominator not divisible by $p$ , has maximal ideal $p Z_{(p)}$ , and residue field $F_{p}$

Example

For a positive prime integer $p$ , $Z_{(p)} = {\frac{a}{b} \in Q : a, b \in Z, p ∤ b} .$ It is local with maximal ideal $p Z_{(p)}$ , and its residue field is canonically $F_{p} = Z / p Z$ .

Facts & Assumptions

Given: A positive prime integer $p$ .

[F1]

The quotient $Z / p Z$ is a field for prime $p$ ; every field is a domain; and $R / P$ is a domain exactly when $P$ is prime (For every prime $p$ , the two operations on $Z / p$ make it a field, Every field is a commutative ring with $1 \neq 0$ ; it is an integral domain, and it is a commutative division ring, $R / P$ is an integral domain if and only if $P$ is a prime ideal, For every $n \in N$ , the congruence-class ring $Z / n$ is the quotient ring $Z / n Z$ ).

[F2]

Localising at a prime gives a local ring with maximal ideal the extended prime ( $R_{p}$ is local with unique maximal ideal $p R_{p}$ ).

[F3]

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

[F4]

The field of fractions of $Z$ is $Q$ ( $Frac (Z)$ is canonically isomorphic to $Q$ ).

[F5]

A homomorphism that sends all denominators to units factors uniquely through the localisation (Universal property of localisation: maps that invert $S$ factor uniquely through $S^{- 1} R$ ).

[F6]

A localisation fraction $a / b$ is zero exactly when some denominator annihilates $a$ (Equality, vanishing, and the kernel of the localisation map).

[F7]

Localisation at a prime ideal $P$ uses the multiplicative set $R ∖ P$ (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ ).

Verification

technique · direct

1.1

Fact [F1] makes $(p)$ a prime ideal, and [F7] says that the denominators in $Z_{(p)}$ are exactly the integers outside $(p)$ , namely those not divisible by $p$ . Such integers are nonzero and hence units in $Q$ , so [F5] gives a map $Z_{(p)} \to Q$ sending $a / b$ to the same fraction. If its image is zero, multiplication by the nonzero $b$ in $Q$ gives $a = 0$ , and [F6] makes $a / b = 0$ in the localisation; thus the map is injective. Its image is exactly the displayed set.

F1F4F5F6F7algebra

2.1

By [F2], the ring is local with maximal ideal $(p) Z_{(p)} = p Z_{(p)}$ . By [F3], its residue field is $Frac (Z / p Z)$ . Since the latter base ring is already a field by [F1], every fraction satisfies $a / b = (a b^{- 1}) / 1$ , so its fraction field is canonically itself.

F1F2F3algebra∎

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: 108 results over 17 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)

Z(p)Z(p)​ consists of rationals with denominator not divisible by pp, has maximal ideal pZ(p)pZ(p)​, and residue field FpFp​