Alphabeta Math
Session-authored (Fable 5 assisted)
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.

17 results · all verified · 11 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Field of Fractions and Localisation

1 · Prerequisites

2 · Summary

The prerequisites supply commutative rings, homomorphisms, units, integral domains, ideals, quotient rings, fields, and polynomial rings. Their definitions and universal properties provide the algebra needed to compare fractions, identify kernels, recognise maximal and prime ideals, and pass between a ring and its quotients.

Multiplicative subsets first give localisation by equivalence classes of fractions, followed by its arithmetic, kernel criterion, universal property, unit test, and iterated form. Localising a domain yields its field of fractions and rational function fields. The unit characterisations of local rings lead to localisation at a prime, residue fields, and trivial idempotents, while extension and contraction of ideals culminate in the ideal and prime correspondences and the compatibility of localisation with quotients.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-13Open item page →

Multiplicative subsets and the localisation S1R as equivalence classes of fractions

Definition

Let R be a commutative ring. A subset SR is multiplicative if 1S and s,tS implies stS.

On R×S, define (r,s)(r,s)u(rsrs)=0 for some uS. The localisation of R at S, denoted S1R, is the set of equivalence classes for this relation. The class of (r,s) is written r/s, and its arithmetic is rs+rs=rs+rsss,rsrs=rrss. The localisation map is the ring homomorphism λS:RS1R,rr/1. Every sS maps to a unit, with (s/1)1=1/s. The construction permits 0S; in that case the localisation is the zero ring.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

The localisation relation is an equivalence relation and fraction arithmetic is well defined

Statement

For every commutative ring R and multiplicative subset S, the relation in Multiplicative subsets and the localisation S1R as equivalence classes of fractions is an equivalence relation. The displayed addition and multiplication are independent of representatives and make S1R a commutative ring with zero 0/1 and identity 1/1. The map λS(r)=r/1 is a unital ring homomorphism, and every s/1 with sS is a unit with inverse 1/s.

Facts & Assumptions

Given: A commutative ring R and a multiplicative subset SR.

[F1]

A multiplicative subset contains 1, is closed under products, and localisation uses (r,s)(r,s) exactly when some uS satisfies u(rsrs)=0 (Multiplicative subsets and the localisation S1R as equivalence classes of fractions).

Proof

technique · direct construction
1.1

Reflexivity has witness 1, and symmetry uses the same witness with the negative equation. If u(rsrs)=0 and v(rsrs)=0, then uvsS and the identity s(rsrs)=s(rsrs)+s(rsrs) shows uvs(rsrs)=0; hence the relation is transitive.

F1algebra
2.1

Suppose (r,s)(ρ,σ) with witness u. For fixed (a,t), multiplying the relation by t2 shows (rt+as,st)(ρt+aσ,σt), and multiplying it by at shows (ra,st)(ρa,σt). Changing the second representative in the same way proves both operations are well defined.

F1step 1.1algebra
3.1

Associativity, commutativity, and distributivity follow by expanding the displayed fraction formulas over common denominators. The classes 0/1 and 1/1 satisfy the zero and identity laws, and additive inverses are (r)/s.

step 2.1algebra
4.1

The formulas give λS(r+r)=λS(r)+λS(r), λS(rr)=λS(r)λS(r), and λS(1)=1/1. Finally (s/1)(1/s)=s/s=1/1, since (s,s)(1,1) with witness 1.

F1step 2.1algebra
PropositionStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Equality, vanishing, and the kernel of the localisation map

Statement

Let R be a commutative ring and SR multiplicative. For r,rR and s,sS, rs=rsu(rsrs)=0 for some uS, and rs=0ur=0 for some uS. Consequently kerλS={rR:ur=0 for some uS}. The map λS is injective if and only if every uS has trivial annihilator. If R is nonzero, this is equivalent to 0S and no member of S being a zero divisor. Moreover, S1R is the zero ring if and only if 0S.

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(rsrs)=0 for some uS, 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 10 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(r10s)=ur=0 for some uS.

F1
2.1

If 0S, step 1.1 makes every fraction zero by using u=0. Conversely, if S1R is the zero ring, then 1/1=0, so step 1.1 gives uS with u1=0, whence u=0 and 0S.

step 1.1
2.2

Since λS(r)=r/1, step 1.1 gives the displayed kernel. Thus λS is injective exactly when ur=0 with uS 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 0S, because 01=0 and 10, and no uS is a zero divisor by [F2]. Conversely, if 0S and S contains no zero divisor, then uS is nonzero and ur=0 forces r=0 by [F2].

F2step 2.2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Universal property of localisation: maps that invert S factor uniquely through S1R

Statement

Let f:RA be a unital homomorphism of commutative rings such that f(s) is a unit for every sS. There is a unique unital ring homomorphism f~:S1RA satisfying f~λS=f, namely f~(r/s)=f(r)f(s)1.

Facts & Assumptions

Given: A multiplicative subset S of a commutative ring R and a unital ring homomorphism f:RA taking every element of S to a unit.

[F1]

Fraction equality means that u(rsrs)=0 for some uS (Equality, vanishing, and the kernel of the localisation map).

[F2]

Units form a group under multiplication, so products and inverses of units are units and inverses are unique (The units of a ring are the invertible elements of its multiplicative monoid, and R× is a group under multiplication; 0R× only in the zero ring).

[F3]

Localisation arithmetic is r/s+r/s=(rs+rs)/(ss) and (r/s)(r/s)=rr/(ss) (The localisation relation is an equivalence relation and fraction arithmetic is well defined).

Proof

technique · constructive
1.1

Define f~(r/s)=f(r)f(s)1. If r/s=r/s, [F1] gives u(rsrs)=0 for some uS. Applying f and cancelling the unit f(u) yields f(r)f(s)=f(r)f(s); multiplying by f(s)1f(s)1 proves the definition is independent of representatives.

F1F2construct
1.2

Using [F3] and the homomorphism laws for f, direct calculation shows that f~ preserves addition, multiplication, zero, and one. Also f~(r/1)=f(r)f(1)1=f(r), so f~λS=f.

F2F3algebra
2.1

If g:S1RA is another such homomorphism, then g(r/1)=f(r) and g(s/1)=f(s). Since (s/1)(1/s)=1, uniqueness of inverses gives g(1/s)=f(s)1; hence g(r/s)=g(r/1)g(1/s)=f~(r/s) for every fraction.

F2step 1.2
3.1

If 0S, the hypothesis says that f(0)=0 is a unit of A, so A is the zero ring. The construction and uniqueness above still apply, with the unique map between zero rings.

F2step 1.1step 1.2step 2.1discharge-construct
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

A localisation is unique up to a unique isomorphism compatible with the map from R

Statement

Let λ:RL and λ:RL be unital homomorphisms of commutative rings. Suppose each map sends every sS to a unit and has the localisation universal property: every homomorphism from R that inverts S factors uniquely through it. Then there is a unique ring isomorphism Φ:LL such that Φλ=λ.

Facts & Assumptions

Given: Two objects (L,λ) and (L,λ) satisfying the stated universal property for the same pair (R,S).

[F1]

A homomorphism from R that takes S to units factors uniquely through a localisation map (Universal property of localisation: maps that invert S factor uniquely through S1R).

Proof

technique · direct universal-property argument
1.1

Apply the universal property of L to λ and that of L to λ. This gives unique homomorphisms Φ:LL and Ψ:LL with Φλ=λ and Ψλ=λ.

F1
2.1

Both ΨΦ and idL compose with λ to give λ. Uniqueness for L gives ΨΦ=idL; similarly ΦΨ=idL. Thus Φ is an isomorphism.

F1step 1.1
3.1

Any isomorphism compatible with the maps from R is, in particular, a factorisation of λ through λ, so it equals Φ by uniqueness.

F1step 1.1
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

A fraction r/s is a unit in S1R exactly when arS for some aR

Statement

Let R be a commutative ring and SR multiplicative. A fraction r/sS1R is a unit if and only if arS for some aR.

Facts & Assumptions

Given: A fraction r/s in S1R.

[F1]

Fractions satisfy the usual multiplication law, and equality is detected by an annihilating element of S (The localisation relation is an equivalence relation and fraction arithmetic is well defined, Equality, vanishing, and the kernel of the localisation map).

Proof

technique · direct
1.1

If arS, then as/(ar) is a valid fraction and (r/s)(as/(ar))=ars/(sar)=1 by [F1]. Hence r/s is a unit.

F1
2.1

Conversely, suppose (r/s)(b/t)=1. Then rb/(st)=1, so [F1] supplies uS with u(rbst)=0. Therefore (ub)r=ustS, because u,s,tS. Taking a=ub proves the criterion.

F1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Principal localisation Rf={1,f,f2,}1R

Definition

For a commutative ring R and fR, the powers Sf={1,f,f2,}={fn:nN} form a multiplicative subset. The principal localisation of R at f is Rf=Sf1R. Its elements may be written r/fn. In particular, R1 is canonically isomorphic to R, while R0 is the zero ring.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Localising twice is localising once at the multiplicative set generated by both denominator sets

Statement

Let S,TR be multiplicative, let T be the image of T in S1R, and let UR be the multiplicative subset generated by ST. Then there is a unique R-algebra isomorphism T1(S1R)U1R. In particular, (Rf)gRfg for f,gR, where g on the left denotes its image in Rf.

Facts & Assumptions

Given: Multiplicative subsets S,TR, their generated multiplicative set U, and the image TS1R.

[F1]

A homomorphism out of a localisation is uniquely determined by a map from the original ring that sends the denominator set to units (Universal property of localisation: maps that invert S factor uniquely through S1R).

[F2]

Two objects with the same localisation universal property are uniquely isomorphic over the original ring (A localisation is unique up to a unique isomorphism compatible with the map from R).

[F3]

The principal localisation Rf inverts the powers of f (Principal localisation Rf={1,f,f2,}1R).

Proof

technique · direct universal-property argument
1.1

A map h:RA extends to T1(S1R) exactly when it sends S to units and, after the first extension, sends every t/1 with tT to a unit.

F1
2.1

The image of t/1 is h(t), so the condition in step 1.1 is exactly that h send every member of ST to a unit, equivalently every element of the generated set U to a unit.

step 1.1algebra
3.1

Hence T1(S1R) and U1R have the same universal property over R, so [F2] gives the unique displayed R-algebra isomorphism.

F1F2step 2.1
4.1

For S={fn:nN} and T={gn:nN}, the set U is generated by f and g. A map inverts both precisely when it inverts fg: if fg is a unit, then f(g(fg)1)=1 and g(f(fg)1)=1. Thus [F1] identifies this localisation with Rfg, including f=0 or g=0.

F1F3algebra
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

The field of fractions Frac(D)=(D{0})1D of an integral domain

Definition

If D is an integral domain, then D{0} is multiplicative. Its localisation Frac(D)=(D{0})1D is the field of fractions of D. Thus its elements are fractions a/b with a,bD and b0, modulo the localisation equivalence relation.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Frac(D) is a field and dd/1 embeds the integral domain D

Statement

For every integral domain D, the localisation Frac(D) is a field. Its canonical map DFrac(D),dd/1, is an injective unital ring homomorphism.

Facts & Assumptions

Given: An integral domain D.

[F1]

The field of fractions is the localisation at D{0} (The field of fractions Frac(D)=(D{0})1D of an integral domain).

[F2]

A localisation map is injective exactly when every denominator has trivial annihilator (Equality, vanishing, and the kernel of the localisation map).

[F3]

Localisation is a commutative ring with the stated fraction arithmetic (The localisation relation is an equivalence relation and fraction arithmetic is well defined).

[F4]

A field is a nonzero commutative ring in which every nonzero element is a unit (Field).

Proof

technique · direct
1.1

Every nonzero element of the domain D has trivial annihilator. Hence [F2], applied to S=D{0}, makes the canonical homomorphism injective. In particular 1/10/1, so the localisation is nonzero.

F1F2
1.2

Let a/b be nonzero. By the vanishing criterion in [F2], a0, because otherwise a/b=0. Thus aD{0}, and [F3] gives (a/b)(b/a)=1.

F1F2F3
2.1

Every nonzero element is therefore a unit, and [F3] supplies the commutative-ring structure. By [F4], Frac(D) is a field.

F3F4step 1.1step 1.2
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Every injective ring map from a domain into a field factors uniquely through its field of fractions

Statement

Let D be an integral domain, K a field, and f:DK an injective unital ring homomorphism. There is a unique unital ring homomorphism f~:Frac(D)K such that f~(d/1)=f(d) for all dD. It is injective and satisfies f~(a/b)=f(a)f(b)1.

Facts & Assumptions

Given: An injective unital ring homomorphism f:DK from an integral domain to a field.

[F1]

Every nonzero element of a field is a unit (Field).

[F2]

A map that sends every localisation denominator to a unit factors uniquely through the localisation, by the displayed fraction formula (Universal property of localisation: maps that invert S factor uniquely through S1R).

[F3]

The canonical map embeds D in Frac(D) (Frac(D) is a field and dd/1 embeds the integral domain D).

Proof

technique · direct
1.1

If b0 in D, injectivity gives f(b)0, so [F1] makes f(b) a unit. Since the denominators defining Frac(D) are exactly the nonzero elements, [F2] gives the unique extension and its formula.

F1F2
2.1

If f~(a/b)=0, multiply f(a)f(b)1=0 by the unit f(b) to obtain f(a)=0. Injectivity of f gives a=0, hence a/b=0. Thus f~ is injective.

step 1.1F3algebra
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Fields of fractions are uniquely isomorphic over their embedded domain

Statement

Let D be an integral domain. Suppose K and L are fields containing embedded copies of D, and every element of either field is a quotient of two elements from that copy with nonzero denominator. Then there is a unique field isomorphism KL fixing D pointwise.

Facts & Assumptions

Given: Fields K,L with the stated embeddings and quotient-generation property.

[F1]

An injective map from a domain into a field extends uniquely to an injective homomorphism from its field of fractions, with a/b sent to the corresponding quotient (Every injective ring map from a domain into a field factors uniquely through its field of fractions).

Proof

technique · direct
1.1

By [F1], the embeddings of D produce injective homomorphisms ϕ:Frac(D)K and ψ:Frac(D)L. Their images contain every quotient of embedded elements of D, so the quotient-generation hypothesis makes both maps surjective.

F1
2.1

The composite ψϕ1:KL is therefore a field isomorphism fixing D. If θ:KL also fixes D, then for every a/bK one has θ(a/b)=a/b, so θ=ψϕ1.

step 1.1algebra
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

For a field F, F(t)=Frac(F[t]) is its rational function field; in particular R(t)=Frac(R[t])

Statement

For every field F, the polynomial ring F[t] is an integral domain, and F(t):=Frac(F[t])={f(t)g(t):f,gF[t], g0} is a field containing an embedded copy of F[t]. It is called the rational function field over F. In particular, R(t)=Frac(R[t]).

Facts & Assumptions

Given: A field F.

[F2]

If R is an integral domain, then R[t] is an integral domain (A polynomial ring over an integral domain is an integral domain).

[F3]

The field of fractions of a domain consists of fractions with nonzero denominator and is a field containing the domain injectively (The field of fractions Frac(D)=(D{0})1D of an integral domain, Frac(D) is a field and dd/1 embeds the integral domain D).

Proof

technique · direct
1.1

By [F1] and [F2], F[t] is an integral domain. Applying [F3] gives the displayed set of fractions, its field structure, and the embedding of F[t].

F1F2F3
2.1

Taking F=R gives the final assertion.

step 1.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

A local ring is a nonzero commutative ring with a unique maximal ideal

Definition

A local ring is a nonzero commutative ring R with exactly one maximal ideal. That ideal is usually denoted mR or simply m. The quotient R/m, which is a field, is the residue field of the local ring.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of x and 1x is a unit for every x

Statement

Assume the Axiom of Choice. For a nonzero commutative ring R, the following are equivalent:

  1. R is local;
  2. the set of nonunits of R is an ideal;
  3. for every xR, at least one of x and 1x is a unit.

When these conditions hold, the ideal of nonunits is the unique maximal ideal.

Facts & Assumptions

Given: A nonzero commutative ring R and the Axiom of Choice.

[F1]

A local ring is a nonzero commutative ring with one maximal ideal (A local ring is a nonzero commutative ring with a unique maximal ideal).

[F2]

Assuming Choice, every proper ideal in a nonzero commutative ring lies in a maximal ideal (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal).

[F4]

An ideal contains 0, is closed under addition and additive inverses, and absorbs multiplication by ring elements (Left, right and two-sided ideals).

Proof

technique · direct cycle of implications
1.1

Assume R is local with maximal ideal m. No element of m is a unit. Conversely, if x is a nonunit, then (x) is proper and [F2] places it in a maximal ideal, necessarily m. Thus the nonunits are exactly m, proving condition 2.

F1F2F3
1.2

Assume the nonunits form an ideal N. If both x and 1x were nonunits, then [F4] would give 1=x+(1x)N, contrary to [F3]. Hence condition 3 holds.

F3F4
1.3

Assume condition 3 and let N be the nonunits. By [F3], 0N. If xN and rR, then rx cannot be a unit, since an inverse for rx would make x a unit; also x cannot be a unit.

F3algebra
2.1

If x,yN and u=x+y were a unit, then xu1 and yu1=1xu1 would both be nonunits, because a unit among either would make x or y a unit. This contradicts condition 3. Thus x+yN, and [F4] with step 1.3 shows that N is an ideal.

F3F4step 1.3
3.1

The ideal N is proper because 1N. Every proper ideal consists entirely of nonunits, so it is contained in N. Hence N is maximal and is the only maximal ideal; by [F1], R is local.

F1F3F4step 2.1
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Localisation at a prime ideal: Rp=(Rp)1R

Definition

Let R be a commutative ring and let pR be a prime ideal. Since 1p and the product of two elements outside p remains outside p, the complement Rp is multiplicative. The localisation of R at p is Rp=(Rp)1R. Its elements are fractions r/s with sp.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

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:rp, sp}, and its units are exactly the fractions r/s with rp.

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=(Rp)1R).

[F2]

A fraction r/s is a unit exactly when ar belongs to the denominator set for some aR (A fraction r/s is a unit in S1R exactly when arS for some aR).

[F3]

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

F1F3
1.2

By [F2], if rp, then r/s is a unit by taking a=1. If rp 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 rp, then [F3] gives up with u(rsrs)=0. Hence urs=ursp; primality and u,sp force rp.

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 1p, 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
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Assuming the Axiom of Choice, a local ring R is canonically isomorphic to Rm at its maximal ideal

Statement

Assume the Axiom of Choice. If (R,m) is a local ring, its localisation map λ:RRm is a ring isomorphism. Its inverse sends r/s to rs1.

Facts & Assumptions

Given: A local ring (R,m).

[F2]

The denominators in Rm are the elements of Rm (Localisation at a prime ideal: Rp=(Rp)1R).

[F3]

Any map that inverts all denominators extends uniquely through the localisation (Universal property of localisation: maps that invert S factor uniquely through S1R).

Proof

technique · direct universal-property argument
1.1

By [F1] and [F2], every denominator is already a unit in R. Applying [F3] to idR gives g:RmR with g(r/s)=rs1 and gλ=idR.

F1F2F3
2.1

Both λg and idRm compose with λ to give λ. The uniqueness clause of [F3] gives λg=idRm, so λ is an isomorphism with inverse g.

F3step 1.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Assuming the Axiom of Choice, a local ring has no idempotents other than 0 and 1

Statement

Assume the Axiom of Choice. If R is a local ring and eR satisfies e2=e, then e=0 or e=1.

Facts & Assumptions

Given: A local ring R and an idempotent eR.

Proof

technique · cases
1.1

By [F1], either e is a unit or 1e is a unit. If e is a unit, multiplying e2=e by e1 gives e=1.

F1algebraassume-case eunit
2.1

If 1e is a unit, then (1e)e=ee2=0; multiplying by (1e)1 gives e=0. The two cases prove the claim, including the endpoint idempotents themselves.

F1algebraassume-case complementcases-exhaustive
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Ideals of S1R correspond to S-saturated ideals of R, and prime ideals correspond to primes disjoint from S

Statement

Let R be a commutative ring and SR multiplicative. For an ideal IR, write S1I={r/s:rI, sS},Isat={rR:srI for some sS}. An ideal is S-saturated when I=Isat. Extension IS1I and contraction JλS1(J) give inverse inclusion-preserving bijections between S-saturated ideals of R and ideals of S1R. Moreover, they restrict to inverse bijections {pSpecR:pS=}Spec(S1R),pS1p.

Facts & Assumptions

Given: A commutative ring R, a multiplicative subset S, and the localisation map λS.

[F1]

Localisation has the usual fraction arithmetic, equality is detected by a witness in S, and every s/1 is a unit (The localisation relation is an equivalence relation and fraction arithmetic is well defined, Equality, vanishing, and the kernel of the localisation map).

[F2]

Ideals are additive subgroups absorbing multiplication; a prime ideal is proper and contains one factor whenever it contains a product (Left, right and two-sided ideals, Prime ideals and maximal ideals in a commutative ring).

[L1]

Each ideal of S1R is S1I for its inverse-image ideal I in R (The Stacks Project, Lemma 10.9.16).

[L2]

The map RS1R induces a bijection from the prime ideals of S1R to the prime ideals of R disjoint from S, with inverse pS1p (The Stacks Project, Lemma 10.17.5).

Proof

technique · direct extension and contraction
1.1

The displayed S1I is an ideal: common-denominator addition preserves numerator membership in I, and multiplication by an arbitrary fraction does likewise. It is also the ideal generated by the elements i/1 with iI, since i/s=(i/1)(1/s).

F1F2
1.2

For completeness, let p be prime and disjoint from S. It is saturated, since srp with sp forces rp. Its extension is proper: 1=i/s with ip would give u(si)=0, hence us=uip, contradicting u,sS.

F1F2
2.1

An element r lies in the contraction of S1I exactly when r/1=i/s for some iI. Equality gives u(rsi)=0, hence (us)r=uiI, so rIsat. Conversely, if trI for tS, then r/1=tr/tS1I. Thus the contraction is exactly Isat.

F1step 1.1
3.1

If JS1R is an ideal and I=λS1(J), then r/sJ implies r/1=(s/1)(r/s)J, while r/1J implies r/s=(1/s)(r/1)J. Hence J=S1I, as in [L1]. Step 2.1 also makes I saturated.

F1F2L1
3.2

If (a/s)(b/t)S1p, contraction and saturation give uabp for some uS. Since up, primality gives ap or bp, so one factor lies in S1p. Thus the extension is prime.

F1F2step 2.1step 1.2
4.1

Steps 2.1 and 3.1 prove that extension and contraction are inverse on the stated ideals. Both operations visibly preserve inclusion.

step 2.1step 3.1
5.1

Conversely, the contraction qc of a prime qS1R is proper because 1/1q. If abqc, then (a/1)(b/1)q, so primality gives aqc or bqc. It also misses S, because each s/1 is a unit and no proper ideal contains a unit. Together with steps 3.2 and 4.1, this proves the prime bijection stated in [L2].

F1F2L2step 3.2step 4.1
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Localisation commutes with quotient rings: S1R/S1ISˉ1(R/I)

Statement

Let I be an ideal of a commutative ring R, let SR be multiplicative, and let Sˉ be the image of S in R/I. There is a canonical isomorphism (S1R)/(S1I)Sˉ1(R/I),r/s+S1I(r+I)/(s+I). This includes the case SI, when both sides are the zero ring.

Facts & Assumptions

Given: A commutative ring R, an ideal I, and a multiplicative subset S with image Sˉ in R/I.

[F1]

A map that sends a multiplicative subset to units factors uniquely through the corresponding localisation (Universal property of localisation: maps that invert S factor uniquely through S1R).

[F2]

A homomorphism killing an ideal factors uniquely through the quotient by that ideal (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[F3]

The extended ideal S1I consists of the fractions with a numerator in I (Ideals of S1R correspond to S-saturated ideals of R, and prime ideals correspond to primes disjoint from S).

Proof

technique · construction of inverse maps
1.1

The map RSˉ1(R/I) given by r(r+I)/1 sends S to units, so [F1] gives Φ:S1RSˉ1(R/I) with Φ(r/s)=(r+I)/(s+I). It kills S1I by [F3], so [F2] gives a homomorphism Φ:(S1R)/(S1I)Sˉ1(R/I).

F1F2F3construct
1.2

The map R(S1R)/(S1I) given by rr/1+S1I kills I, so [F2] induces R/I(S1R)/(S1I). Every s+ISˉ maps to the unit s/1+S1I, so [F1] extends this to Ψ:Sˉ1(R/I)(S1R)/(S1I).

F1F2F3
2.1

The composites ΨΦ and ΦΨ fix, respectively, every class r/s+S1I and every fraction (r+I)/(s+I) by the formulas in steps 1.1 and 1.2. Hence the maps are inverse isomorphisms. If sSI, then 1=s/sS1I, so the left side is zero; also s+I=0 lies in Sˉ, so the right localisation is zero.

step 1.1step 1.2F3algebradischarge-construct
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13Open item page →

Rp/pRpFrac(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 Rp/pRpFrac(R/p),r/s+pRp(r+p)/(s+p). This quotient is the residue field of the local ring Rp.

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: S1R/S1ISˉ1(R/I)).

[F2]

The ring Rp is local with maximal ideal pRp (Rp is local with unique maximal ideal pRp).

[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 dd/1 embeds the integral domain D).

Proof

technique · direct
1.1

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

F1
2.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 Rp.

F1F2F3F4step 1.1

5 · Examples, counterexamples and false statements

None yet.

Sources