PropositionStatement: AI-adaptedProof: 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.

Equality, vanishing, and the kernel of the localisation map

Statement

Let $R$ be a commutative ring and $S \subseteq R$ multiplicative. For $r, r^{'} \in R$ and $s, s^{'} \in S$ , $\frac{r}{s} = \frac{r^{'}}{s^{'}} ⟺ u (r s^{'} - r^{'} s) = 0 for some u \in S,$ and $\frac{r}{s} = 0 ⟺ u r = 0 for some u \in S .$ Consequently $\ker λ_{S} = {r \in R : u r = 0 for some u \in S} .$ The map $λ_{S}$ is injective if and only if every $u \in S$ has trivial annihilator. If $R$ is nonzero, this is equivalent to $0 \notin S$ and no member of $S$ being a zero divisor. Moreover, $S^{- 1} R$ is the zero ring if and only if $0 \in S$ .

Facts & Assumptions

Given: A commutative ring $R$ , a multiplicative subset $S$ , and its localisation map $λ_{S}$ .

[F1]

Fractions are precisely equivalence classes for the relation $u (r s^{'} - r^{'} s) = 0$ for some $u \in S$ , and $0 = 0 / 1$ (The localisation relation is an equivalence relation and fraction arithmetic is well defined).

[F2]

In a nonzero commutative ring, a zero divisor is a nonzero element annihilating some nonzero element; by convention, $0$ itself is not called a zero divisor (Zero divisor, and integral domain: a commutative ring with $1 \neq 0$ and no zero divisors).

Proof

technique · direct

1.1

The equality criterion is the definition of equality of equivalence classes. Taking $(r^{'}, s^{'}) = (0, 1)$ gives $r / s = 0 / 1$ exactly when $u (r \cdot 1 - 0 \cdot s) = u r = 0$ for some $u \in S$ .

2.1

If $0 \in S$ , step 1.1 makes every fraction zero by using $u = 0$ . Conversely, if $S^{- 1} R$ is the zero ring, then $1 / 1 = 0$ , so step 1.1 gives $u \in S$ with $u \cdot 1 = 0$ , whence $u = 0$ and $0 \in S$ .

step 1.1

2.2

Since $λ_{S} (r) = r / 1$ , step 1.1 gives the displayed kernel. Thus $λ_{S}$ is injective exactly when $u r = 0$ with $u \in S$ always forces $r = 0$ , which says precisely that every member of $S$ has trivial annihilator.

step 1.1

3.1

Assume $R$ is nonzero. If every member of $S$ has trivial annihilator, then $0 \notin S$ , because $0 \cdot 1 = 0$ and $1 \neq 0$ , and no $u \in S$ is a zero divisor by [F2]. Conversely, if $0 \notin S$ and $S$ contains no zero divisor, then $u \in S$ is nonzero and $u r = 0$ forces $r = 0$ by [F2].

F2step 2.2∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 13 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.9: Localization (standard reference, not scraped)