Rings, ideals and fields

Lens

MotivationH

When factorisation stops being unique

Every whole number greater than $1$ factors into primes in essentially one way. Polynomials over a field behave the same way: $x^4 - 1 = (x - 1)(x + 1)(x^2 + 1)$ over $\Q$ , and there is no other factorisation into irreducibles. The reason is the same in both cases: division with remainder, which gives Euclid's algorithm, then Bézout's identity, then Euclid's lemma ( $p \mid ab \Rightarrow p \mid a$ or $p \mid b$ ), and finally uniqueness.

Mathematicians soon found they wanted to factor other kinds of numbers. In his Algebra (1770), Leonhard Euler solved $y^3 = x^2 + 2$ in integers by factoring $x^2 + 2 = (x + \sqrt{-2})(x - \sqrt{-2})$ and arguing as if unique factorisation held for numbers $a + b\sqrt{-2}$ . (It does, but Euler did not prove it.) In 1847 Gabriel Lamé announced a proof of Fermat's Last Theorem that factored $x^p + y^p$ over the complex $p$ -th roots of unity, and it rested on the same unproved assumption. Joseph Liouville pointed out the gap at once. Ernst Kummer had already discovered that unique factorisation fails for some of these number systems. The simplest failure is in the numbers $a + b\sqrt{-5}$ , $a, b \in \Z$ :

6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5}),

where none of the four factors can be broken down further, and $2$ is not a unit multiple of either $1 \pm \sqrt{-5}$ .

Kummer's response was to invent "ideal numbers" that restore uniqueness, and Richard Dedekind turned them into the ideals of this lesson. We define rings and their ideals, find their units and zero divisors, and prove the chain

\text{Euclidean domain} \;\Longrightarrow\; \text{principal ideal domain} \;\Longrightarrow\; \text{unique factorisation domain},

with examples showing that neither arrow reverses and that $\Z[\sqrt{-5}]$ is not even a UFD.

IntuitionH

Two operations, and the multiples of a number

A group has one operation (see groups). Numbers, polynomials, matrices and functions have two, addition and multiplication, linked by the distributive law. A ring is the structure they share.

The ring axioms say nothing about division, and the interesting questions are about it. Which elements can be inverted? Can a product of non-zero elements be zero? Is there a division algorithm? Does factorisation into "atoms" exist, and is it unique?

The key new notion is the set of all multiples of an element. In $\Z$ the multiples of $6$ form $6\Z$ . This set is closed under addition, and it absorbs multiplication: any integer times a multiple of $6$ is again a multiple of $6$ . Divisibility is containment: $2 \mid 6$ exactly when $6\Z \subseteq 2\Z$ . A gcd is a generator of a sum: $4\Z + 6\Z = 2\Z$ . Sets of this kind are called ideals. In $\Z[\sqrt{-5}]$ the set $(2, 1 + \sqrt{-5})$ of all combinations $2\alpha + (1 + \sqrt{-5})\beta$ is an ideal, but it consists of the multiples of no single element: it behaves like a "gcd of $2$ and $1 + \sqrt{-5}$ " that does not exist as a number. Kummer's ideal numbers were exactly such missing gcds.

DefinitionsH

Rings, ideals and the factorisation hierarchy

Convention. In this lesson (and the following ones) a ring has a multiplicative identity $1$ , and ring homomorphisms preserve it. Some books (for example in analysis) allow rings without $1$ ; then $2\Z$ is a ring. Commutativity is not assumed unless stated. Integral domains and fields are commutative and have $0 \ne 1$ .

Definition— ring

A ring is a set $R$ with two operations $+$ and $\cdot$ such that $(R, +)$ is an abelian group with identity $0$ , multiplication is associative with identity $1$ , and the distributive laws $a(b + c) = ab + ac$ and $(a + b)c = ac + bc$ hold. $R$ is commutative if $ab = ba$ for all $a, b$ . A subring is a subset containing $1$ and closed under $+$ , $-$ and $\cdot$ .

Definition— units, zero divisors, domains and fields

A unit is an element $u$ with some $v$ such that $uv = vu = 1$ ; the units form a group $R^\times$ . A zero divisor is a non-zero $a$ with $ab = 0$ or $ba = 0$ for some non-zero $b$ . An integral domain is a commutative ring with $0 \ne 1$ and no zero divisors. A field is a commutative ring with $0 \ne 1$ in which every non-zero element is a unit. (A division ring drops commutativity.)

Definition— ring homomorphism, kernel

A ring homomorphism $f : R \to S$ satisfies $f(a + b) = f(a) + f(b)$ , $f(ab) = f(a)f(b)$ and $f(1) = 1$ . Its kernel is $\ker f = \{a \mid f(a) = 0\}$ .

Definition— ideal

A left ideal of $R$ is an additive subgroup $I$ with $ra \in I$ for all $r \in R$ , $a \in I$ ; a two-sided ideal also has $ar \in I$ . In a commutative ring the notions coincide and we just say ideal. The ideal generated by $a_1, \dots, a_n$ in a commutative ring is $(a_1, \dots, a_n) = \{r_1a_1 + \dots + r_na_n\}$ . An ideal is principal if it equals $(a)$ for one element $a$ .

Definition— prime and maximal ideals

In a commutative ring $R$ , an ideal $P \ne R$ is prime if $ab \in P$ implies $a \in P$ or $b \in P$ , and an ideal $M \ne R$ is maximal if there is no ideal strictly between $M$ and $R$ . (In quotients we prove that $R/P$ is a domain and $R/M$ a field exactly in these cases.)

Definition— divisibility, irreducible and prime elements

Let $R$ be an integral domain. Then $a \mid b$ if $b = ac$ for some $c$ ; $a$ and $b$ are associates if $b = ua$ for a unit $u$ . A non-zero non-unit $p$ is irreducible if $p = ab$ forces $a$ or $b$ to be a unit, and prime if $p \mid ab$ forces $p \mid a$ or $p \mid b$ .

Definition— Euclidean domain, PID, UFD

An integral domain $R$ is

a Euclidean domain if there is a function $\delta : R \setminus \{0\} \to \N$ such that for all $a$ and all $b \ne 0$ there are $q, r$ with $a = qb + r$ and either $r = 0$ or $\delta(r) \lt \delta(b)$ ;
a principal ideal domain (PID) if every ideal is principal;
a unique factorisation domain (UFD) if every non-zero non-unit is a product of irreducibles, uniquely up to the order of the factors and replacing factors by associates.

The hierarchy proved in this lesson, with an example in each layer that is not in the next one inside. Fields are Euclidean (with δ constant). ℤ[(1+√−19)/2] is a PID that is not Euclidean, ℤ[x] and k[x, y] are UFDs that are not PIDs, ℤ[√−5] is a domain that is not a UFD, and ℤ/6ℤ is not a domain.

Worked examplesH

A gallery of rings

Example— Numbers

$\Z \subset \Q \subset \R \subset \C$ are commutative rings. $\Q$ , $\R$ , $\C$ are fields; $\Z$ is a domain whose only units are $\pm 1$ . The Gaussian integers $\Z[i] = \{a + bi \mid a, b \in \Z\}$ and $\Z[\sqrt{-5}] = \{a + b\sqrt{-5}\}$ are subrings of $\C$ , hence domains. Each has a multiplicative norm $N(a + b\sqrt{d}) = (a + b\sqrt d)(a - b\sqrt d) = a^2 - db^2$ : so $N(a + bi) = a^2 + b^2$ and $N(a + b\sqrt{-5}) = a^2 + 5b^2$ . If $uv = 1$ then $N(u)N(v) = 1$ , so units have norm $1$ . The units of $\Z[i]$ are therefore $\pm 1, \pm i$ , and those of $\Z[\sqrt{-5}]$ are $\pm 1$ .

Example— Remainders

In $\Z/n\Z$ , a residue $a$ is a unit iff $\gcd(a, n) = 1$ . Otherwise, if $a \ne 0$ , it is a zero divisor: with $d = \gcd(a, n) \gt 1$ , we have $a \cdot \frac{n}{d} = \frac{a}{d}\, n \equiv 0$ . In $\Z/12\Z$ the units are $1, 5, 7, 11$ , and the other seven non-zero residues are zero divisors. Some elements are nilpotent ( $6^2 = 36 \equiv 0$ in $\Z/12\Z$ ) and some are idempotent ( $4^2 = 16 \equiv 4$ ). So $\Z/n\Z$ is a domain iff it is a field iff $n$ is prime. The field $\Z/p\Z$ is also written $\mathbb{F}_p$ .

Example— Polynomials

For a commutative ring $R$ , $R[x]$ is the ring of polynomials with coefficients in $R$ . If $R$ is a domain, then $\deg(fg) = \deg f + \deg g$ for non-zero $f, g$ , because the leading coefficients multiply. So $R[x]$ is a domain and its units are the units of $R$ (constants). For a field $k$ , $k[x]$ behaves remarkably like $\Z$ : there is long division, and its irreducible elements play the role of primes (see polynomials). Over a non-domain strange things happen: in $(\Z/4\Z)[x]$ , $(1 + 2x)^2 = 1 + 4x + 4x^2 = 1$ , so the non-constant polynomial $1 + 2x$ is a unit.

Example— Non-commutative rings

The matrix ring $M_n(k)$ ( $n \ge 2$ ) is not commutative and has zero divisors and nilpotents: $\left(\begin{smallmatrix} 0 & 1 \\ 0 & 0 \end{smallmatrix}\right)^2 = 0$ . Its two-sided ideals are only $0$ and $M_n(k)$ , although it has many left ideals. The quaternions $\mathbb{H} = \{a + bi + cj + dk\}$ with $i^2 = j^2 = k^2 = ijk = -1$ form a division ring that is not a field, since $ij = k = -ji$ .

Example— Products and functions

$\Z \times \Z$ with componentwise operations is a commutative ring with zero divisors: $(1, 0)(0, 1) = (0, 0)$ . The continuous functions $C([0, 1])$ form a commutative ring. It has zero divisors (two non-zero functions with disjoint supports multiply to $0$ ), and for each $c \in [0, 1]$ the functions vanishing at $c$ form a maximal ideal.

Example— Ideals, subrings and generators

The ideals of $\Z$ are the $n\Z = (n)$ . Every ideal of $\Z$ is an additive subgroup, and these are the $n\Z$ (see groups, Theorem 1). Similarly the ideals of $\Z/n\Z$ are the $(d)$ for divisors $d$ of $n$ .
$\Z$ is a subring of $\Q$ but not an ideal: $\frac12 \cdot 1 \notin \Z$ . In the other direction, $2\Z$ is an ideal of $\Z$ but not a subring (it does not contain $1$ ). A proper ideal never contains a unit.
In $\Z[x]$ : $(x)$ , the polynomials with constant term $0$ , is a prime ideal but not maximal, since $(x) \subsetneq (2, x) \subsetneq \Z[x]$ . The ideal $(2, x)$ , the polynomials with even constant term, is maximal and not principal (Theorem 12).
In $\Z$ , $(p)$ is maximal for $p$ prime, and $(0)$ is prime but not maximal. In $\C[x, y]$ , $(x)$ is prime and $(x, y)$ is maximal.

ProofH

Units, zero divisors and ideals

Theorem— Proposition 1 (first consequences of the axioms)

In every ring: (a) $0 \cdot a = a \cdot 0 = 0$ and $(-a)b = -(ab)$ ; (b) if $0 = 1$ then $R = \{0\}$ ; (c) $R^\times$ is a group under multiplication; (d) a unit is not a zero divisor.

Proof

(a) $0a = (0 + 0)a = 0a + 0a$ ; subtract $0a$ . Then $ab + (-a)b = (a + (-a))b = 0b = 0$ . (b) $a = a \cdot 1 = a \cdot 0 = 0$ . (c) $1$ is a unit, $(uv)(v^{-1}u^{-1}) = 1 = (v^{-1}u^{-1})(uv)$ , and $u^{-1}$ is a unit with inverse $u$ . (d) If $u$ is a unit and $ua = 0$ , then $a = u^{-1}(ua) = u^{-1} \cdot 0 = 0$ ; similarly if $au = 0$ .

∎

Theorem— Theorem 2 (finite domains are fields)

Every finite integral domain is a field.

Proof

Let $a \ne 0$ in the finite domain $R$ . The map $m_a : R \to R$ , $x \mapsto ax$ , is injective: $ax = ay$ gives $a(x - y) = 0$ , so $x = y$ , since there are no zero divisors. An injective map from a finite set to itself is surjective, so $ab = 1$ for some $b$ .

∎

The same argument shows that in a finite commutative ring every non-zero element is either a unit or a zero divisor: if $m_a$ is not injective, then $a(x - y) = 0$ with $x \ne y$ . (Wedderburn's little theorem, 1905, says more: a finite division ring is commutative, hence a field.) The first experiment checks the unit/zero-divisor dichotomy in every $\Z/n\Z$ with $n \le 60$ .

Theorem— Proposition 3 (kernels, units in ideals, fields)

Let $R$ and $S$ be rings.

If $f : R \to S$ is a ring homomorphism, then $\ker f$ is a two-sided ideal of $R$ and $f(R)$ is a subring of $S$ .
An ideal containing a unit is all of $R$ .
A commutative ring $R$ with $0 \ne 1$ is a field iff its only ideals are $(0)$ and $R$ .
Every ring homomorphism from a field to a non-zero ring is injective.

Proof

(1) $\ker f$ is an additive subgroup. If $f(a) = 0$ then $f(ra) = f(r) \cdot 0 = 0$ and $f(ar) = 0$ . The image contains $f(1) = 1$ and is closed under the operations. (2) If $u \in I$ is a unit, then $1 = u^{-1}u \in I$ and $r = r \cdot 1 \in I$ for all $r$ . (3) If $R$ is a field and $I \ne 0$ , then $I$ contains a non-zero element, which is a unit, so $I = R$ by (2). Conversely, if the only ideals are $0$ and $R$ and $a \ne 0$ , then $(a) = R \ni 1$ , so $a$ is a unit. (4) $\ker f$ is an ideal of the field and does not contain $1$ , since $f(1) = 1 \ne 0$ . So $\ker f = 0$ by (3).

∎

Conversely, every two-sided ideal is the kernel of some homomorphism, namely the quotient map $R \to R/I$ . That construction belongs to quotient rings. Together they give the key result: the kernels of ring homomorphisms are exactly the two-sided ideals, just as the kernels of group homomorphisms are exactly the normal subgroups.

Theorem— Proposition 4 (divisibility is containment)

In an integral domain $R$ : (a) $a \mid b \iff (b) \subseteq (a)$ ; (b) $(a) = (b) \iff a, b$ are associates; (c) $(u) = R \iff u$ is a unit; (d) a non-zero $p$ is prime iff $(p)$ is a prime ideal.

Proof

(a) $b = ac \iff b \in (a) \iff (b) \subseteq (a)$ . (b) If $(a) = (b)$ with $a \ne 0$ , write $b = ac$ and $a = bd$ . Then $a = acd$ , so $a(1 - cd) = 0$ , and $cd = 1$ since $R$ is a domain: $c$ is a unit. (If $a = 0$ then $b = 0$ .) The converse is clear. (c) is the case $b = 1$ of (b). (d) This is a restatement: $p \mid x \iff x \in (p)$ , and $(p) \ne R$ iff $p$ is not a unit.

∎

Theorem— Proposition 5 (prime implies irreducible)

In an integral domain every prime element is irreducible.

Proof

Let $p$ be prime and $p = ab$ . Then $p \mid ab$ , so (say) $p \mid a$ : $a = pc$ . Then $p = pcb$ , so $p(1 - cb) = 0$ , and $cb = 1$ because $p \ne 0$ . Hence $b$ is a unit.

∎

The converse fails in general, and it is exactly what fails in $\Z[\sqrt{-5}]$ (Theorem 11). In a UFD the converse holds. If $p$ is irreducible and $p \mid ab$ , factor $a$ , $b$ and $ab/p$ into irreducibles. By uniqueness, $p$ is associate to an irreducible factor of $a$ or of $b$ .

ProofH

Euclidean domain ⇒ PID ⇒ UFD

Theorem— Theorem 6 (three Euclidean domains)

$\Z$ with $\delta(a) = |a|$ , $k[x]$ for a field $k$ with $\delta(f) = \deg f$ , and $\Z[i]$ with $\delta = N$ are Euclidean domains.

Proof

For $\Z$ this is the division algorithm, and for $k[x]$ it is polynomial long division: if $\deg a \ge \deg b$ , subtract $\frac{\text{lead}(a)}{\text{lead}(b)}x^{\deg a - \deg b}\,b$ to lower the degree of $a$ , and repeat. This uses that the leading coefficient of $b$ is invertible, which is why $k$ must be a field.

For $\Z[i]$ , let $a, b \in \Z[i]$ with $b \ne 0$ , and compute the exact quotient $a/b = s + ti \in \Q(i)$ . Choose integers $m, n$ with $|s - m| \le \frac12$ and $|t - n| \le \frac12$ , and set $q = m + ni$ , $r = a - qb$ . Then $r \in \Z[i]$ and, with $N$ extended to $\Q(i)$ (still multiplicative),

N(r) = N(b)\, N\!\left(\tfrac{a}{b} - q\right) = N(b)\big((s - m)^2 + (t - n)^2\big) \le N(b)\left(\tfrac14 + \tfrac14\right) \lt N(b).

∎

Euclidean division in ℤ[i]: the exact quotient a/b (gold) lies in some unit square of the lattice ℤ[i], within distance √2/2 of a corner q. The remainder r = a − qb then has N(r) ≤ N(b)/2. For ℤ[√−5] the lattice is stretched vertically by √5 and the same argument fails: the centre of a box is too far from every corner.

Theorem— Theorem 7 (Euclidean domains are PIDs)

Every ideal of a Euclidean domain is principal.

Proof

Let $I$ be an ideal. If $I = 0$ then $I = (0)$ . Otherwise choose $b \in I \setminus \{0\}$ with $\delta(b)$ least, by well-ordering of $\N$ . For $a \in I$ write $a = qb + r$ with $r = 0$ or $\delta(r) \lt \delta(b)$ . Then $r = a - qb \in I$ , so minimality forces $r = 0$ . Hence $a \in (b)$ , and $I = (b)$ .

∎

Theorem— Theorem 8 (arithmetic in a PID)

Let $R$ be a PID. (a) Any $a, b$ have a gcd $d$ , with $(a, b) = (d)$ , and $d = ra + sb$ for some $r, s$ (Bézout). (b) Every irreducible element is prime (Euclid's lemma). (c) Every non-zero prime ideal is maximal.

Proof

(a) $(a, b)$ is principal, say $(d)$ . Since $a, b \in (d)$ , $d$ is a common divisor. Since $d \in (a, b)$ , $d = ra + sb$ , so every common divisor of $a$ and $b$ divides $d$ .

(b) Let $p$ be irreducible, $p \mid ab$ and $p \nmid a$ . Write $(p, a) = (d)$ . Then $p = dx$ , so $d$ or $x$ is a unit. If $x$ were a unit, $(d) = (p)$ would contain $a$ , giving $p \mid a$ . So $d$ is a unit, $(p, a) = R$ , and $1 = rp + sa$ . Multiplying by $b$ gives $b = rpb + s(ab)$ , a sum of two multiples of $p$ , so $p \mid b$ .

(c) Let $(p) \ne 0$ be prime, and $(p) \subseteq (m) \ne R$ . By Proposition 4(d) and Proposition 5, $p$ is irreducible. From $p = mx$ with $m$ not a unit, $x$ is a unit, so $(m) = (p)$ .

∎

Theorem— Theorem 9 (PIDs are UFDs)

Every principal ideal domain is a unique factorisation domain.

Proof

Chains stabilise. Let $I_1 \subseteq I_2 \subseteq \cdots$ be ideals. Their union $I$ is an ideal (any two elements lie in a common $I_n$ ), so $I = (d)$ . Then $d \in I_n$ for some $n$ , and $I \subseteq I_n \subseteq I_m \subseteq I$ for all $m \ge n$ .

Existence. Suppose a non-zero non-unit $a$ is not a product of irreducibles. Then $a$ is not irreducible, so $a = a_1b_1$ with neither factor a unit. If both $a_1$ and $b_1$ were products of irreducibles, so would $a$ be; say $a_1$ is not. Moreover $(a) \subsetneq (a_1)$ : equality would make $b_1$ a unit, by Proposition 4(b). Repeating with $a_1$ gives a strictly increasing chain $(a) \subsetneq (a_1) \subsetneq (a_2) \subsetneq \cdots$ , which contradicts the first step.

Uniqueness. Suppose $p_1 \cdots p_m = u\,q_1 \cdots q_n$ with all $p_i, q_j$ irreducible and $u$ a unit. We use induction on $m$ . If $m = 0$ , the right side is a unit, so it has no irreducible factors and $n = 0$ . If $m \ge 1$ : $p_1$ is prime by Theorem 8(b), so it divides some $q_j$ . Since $q_j$ is irreducible and $p_1$ is not a unit, $q_j = vp_1$ with $v$ a unit. Cancel $p_1$ (we are in a domain) and apply the induction hypothesis to $p_2 \cdots p_m = (uv)\,q_1 \cdots \widehat{q_j} \cdots q_n$ .

∎

So $\Z$ , $k[x]$ and $\Z[i]$ have unique factorisation. In $\Z[i]$ the prime $5 = (2 + i)(2 - i)$ splits, while $3$ stays prime. Which primes split is the question behind Fermat's theorem on sums of two squares, treated in number theory.

ProofH

Where the hierarchy breaks

Theorem— Theorem 10 (the norm on ℤ[√−5])

In $\Z[\sqrt{-5}]$ , $N(x + y\sqrt{-5}) = x^2 + 5y^2$ is multiplicative, $N(z) = 0$ only for $z = 0$ , the units are $\pm 1$ , and no element has norm $2$ or $3$ .

Proof

$N(z) = z\bar z$ , and complex conjugation is multiplicative, so $N(zw) = N(z)N(w)$ . A sum $x^2 + 5y^2$ of non-negative terms is $0$ only if $x = y = 0$ , and it is $1$ only if $y = 0$ and $x = \pm 1$ . If $x^2 + 5y^2 \in \{2, 3\}$ , then $y = 0$ (else the sum is at least $5$ ), and $x^2 \in \{2, 3\}$ is impossible.

∎

Theorem— Theorem 11 (ℤ[√−5] is not a UFD, and not a PID)

In $\Z[\sqrt{-5}]$ : (a) $2$ , $3$ , $1 + \sqrt{-5}$ and $1 - \sqrt{-5}$ are irreducible, and $2$ is associate to neither $1 \pm \sqrt{-5}$ , so $6 = 2 \cdot 3 = (1 + \sqrt{-5})(1 - \sqrt{-5})$ are two genuinely different factorisations; (b) $2$ is irreducible but not prime; (c) the ideal $(2, 1 + \sqrt{-5})$ is not principal.

Proof

(a) The norms are $4, 9, 6, 6$ . A factorisation $z = ab$ into non-units would need $N(a)$ to be a proper divisor of $N(z)$ greater than $1$ , that is $2$ or $3$ , which is impossible by Theorem 10. The units are $\pm 1$ , and $\pm 2 \ne 1 \pm \sqrt{-5}$ .

(b) $2 \mid 6 = (1 + \sqrt{-5})(1 - \sqrt{-5})$ . But $2 \mid x + y\sqrt{-5}$ requires $x, y$ even, so $2$ divides neither factor.

(c) Let $J = \{x + y\sqrt{-5} \mid x \equiv y \pmod 2\}$ . It is closed under addition, and under multiplication by $\sqrt{-5}$ , since $\sqrt{-5}(x + y\sqrt{-5}) = -5y + x\sqrt{-5}$ and $-5y \equiv y \equiv x$ . So $J$ is an ideal. It contains $2$ and $1 + \sqrt{-5}$ but not $1$ , so $(2, 1 + \sqrt{-5}) \subseteq J \ne R$ . If $(2, 1 + \sqrt{-5}) = (g)$ , then $g \mid 2$ and $g \mid 1 + \sqrt{-5}$ , so $N(g)$ divides $\gcd(4, 6) = 2$ . Thus $N(g) = 1$ , since no norm is $2$ , and $g$ is a unit — contradicting $(g) \subseteq J \ne R$ . (Alternatively: a PID is a UFD, and (a) shows $\Z[\sqrt{-5}]$ is not.)

∎

Ideals restore uniqueness here. With $P = (2, 1 + \sqrt{-5})$ , $Q = (3, 1 + \sqrt{-5})$ and $\bar Q = (3, 1 - \sqrt{-5})$ , one checks that $P^2 = (2)$ , $Q\bar Q = (3)$ , $PQ = (1 + \sqrt{-5})$ and $P\bar Q = (1 - \sqrt{-5})$ . So both factorisations of $6$ refine to the same factorisation into prime ideals, $(6) = P^2 Q \bar Q$ . Dedekind proved that in the ring of integers of any number field, every non-zero ideal factors uniquely into prime ideals (see algebraic number theory).

Theorem— Theorem 12 (neither implication reverses)

(a) $\Z[x]$ is a UFD but not a PID: the ideal $(2, x)$ is not principal. (b) $\Z\big[\frac{1 + \sqrt{-19}}{2}\big]$ is a PID but not a Euclidean domain (for any function $\delta$ ).

Proof

(a) That $\Z[x]$ is a UFD is Gauss's lemma: if $R$ is a UFD, so is $R[x]$ (Dummit and Foote, §9.3). Suppose $(2, x) = (f)$ . Since $f \mid 2$ , degrees give $\deg f = 0$ , so $f = c \in \Z$ . Since $c \mid x$ , $c = \pm 1$ . But every element $2g + xh$ of $(2, x)$ has even constant term, and $f$ is such an element, so $c$ is even. Contradiction.

(b) We only sketch this; full proofs are in Dummit and Foote, §8.1–8.2. The ring is not Euclidean (Motzkin, 1949): in a Euclidean domain that is not a field, an element $u$ of least size among non-zero non-units has the property that every element is congruent modulo $u$ to $0$ or a unit, and in this ring (whose units are $\pm 1$ ) no such $u$ exists. It is a PID because it has a weaker "Dedekind–Hasse" norm property, and because the class number of $\Q(\sqrt{-19})$ is $1$ .

∎

Formal mathematicsF

Rings in Lean and Mathlib

Mathlib's Ring, CommRing, IsDomain and Field classes match the lesson's conventions: rings have a $1$ , and ring homomorphisms R →+* S preserve it. Ideal R is defined as a submodule of $R$ over itself, which is exactly "an additive subgroup that absorbs multiplication". Prime p and Irreducible p are the lesson's definitions. IsPrincipalIdealRing R, EuclideanDomain R and UniqueFactorizationMonoid R are the three layers of the hierarchy.

Units and zero divisors (Proposition 1(d), the $\Z/6\Z$ example and Theorem 2):

unit_mul_eq_zeroLean 4Proved here from basic factsFormally verified

/-- A unit is never a zero divisor: if `u` is a unit and `u * a = 0` then `a = 0`, because
`a = u⁻¹ * (u * a) = u⁻¹ * 0 = 0`. (This works in every ring, commutative or not.) -/
theorem unit_mul_eq_zero {R : Type*} [Ring R] {u a : R} (hu : IsUnit u) (h : u * a = 0) :
    a = 0 := by
  obtain ⟨v, rfl⟩ := hu
  calc a = (↑v⁻¹ * ↑v) * a := by simp
    _ = ↑v⁻¹ * (↑v * a) := mul_assoc _ _ _
    _ = 0 := by rw [h, mul_zero]

Axioms used: propextformal/Lumenary/Rings.leanTry it in the Lean web editor

zmod_six_zero_divisorsLean 4Proved here from basic factsFormally verified

/-- `ℤ/6ℤ` is not an integral domain: `2 · 3 = 0` although neither factor is `0`.
`decide` computes in `ZMod 6`. -/
theorem zmod_six_zero_divisors : (2 : ZMod 6) * 3 = 0 ∧ (2 : ZMod 6) ≠ 0 ∧ (3 : ZMod 6) ≠ 0 := by
  decide

Axioms used: propext, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

finite_domain_inverseLean 4Proved here from basic factsFormally verified

/-- In a finite integral domain every non-zero `a` has an inverse. Multiplication by `a` is
injective (cancellation: `a * x = a * y` and `a ≠ 0` give `x = y`); an injective map from a
finite set to itself is surjective; so some `b` has `a * b = 1`. -/
theorem finite_domain_inverse {R : Type*} [CommRing R] [IsDomain R] [Finite R] (a : R)
    (ha : a ≠ 0) : ∃ b : R, a * b = 1 := by
  have inj : Function.Injective (fun x : R => a * x) := fun x y h => mul_left_cancel₀ ha h
  exact Finite.injective_iff_surjective.mp inj 1

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

finite_domain_is_fieldLean 4Applies a library theoremFormally verified

/-- Every finite integral domain is a field. Mathlib's `Finite.isDomain_to_isField` proves this
even without commutativity — that stronger statement includes Wedderburn's little theorem that
finite division rings are commutative. -/
theorem finite_domain_is_field (R : Type*) [CommRing R] [IsDomain R] [Finite R] : IsField R :=
  Finite.isDomain_to_isField R

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

Kernels and ideals (Proposition 3). The kernel is built by hand and then identified with Mathlib's RingHom.ker:

kerIdealLean 4Formally verified

/-- The kernel of a ring homomorphism, built by hand as an ideal: it contains `0`, is closed
under addition, and absorbs multiplication, since `f (r * x) = f r * 0 = 0`. -/
def kerIdeal {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) : Ideal R where
  carrier := {x | f x = 0}
  zero_mem' := by simp
  add_mem' {x y} hx hy := by simp_all
  smul_mem' r x hx := by simp_all

Axioms used: propextformal/Lumenary/Rings.leanTry it in the Lean web editor

kerIdeal_eqLean 4Proved here from basic factsFormally verified

/-- The hand-built kernel is Mathlib's `RingHom.ker f`: both are `{x | f x = 0}`. -/
theorem kerIdeal_eq {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) :
    kerIdeal f = RingHom.ker f := by
  ext x
  simp [kerIdeal, RingHom.mem_ker]

Axioms used: propext, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

eq_top_of_unit_memLean 4Proved here from basic factsFormally verified

/-- An ideal that contains a unit `u` is the whole ring: it contains `u⁻¹ * u = 1`, and then
`r = r * 1` for every `r`. -/
theorem eq_top_of_unit_mem {R : Type*} [CommRing R] (I : Ideal R) {u : R} (hu : IsUnit u)
    (h : u ∈ I) : I = ⊤ := by
  rw [Ideal.eq_top_iff_one]
  obtain ⟨v, rfl⟩ := hu
  have : (↑v⁻¹ * ↑v : R) ∈ I := I.mul_mem_left _ h
  simpa using this

Axioms used: propext, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

field_idealsLean 4Proved here from basic factsFormally verified

/-- A field has exactly two ideals, `0` and the whole field: a non-zero ideal contains a non-zero
element, which is a unit. -/
theorem field_ideals {K : Type*} [Field K] (I : Ideal K) : I = ⊥ ∨ I = ⊤ := by
  by_cases h : I = ⊥
  · exact Or.inl h
  · obtain ⟨x, hx, hx0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot h
    exact Or.inr (eq_top_of_unit_mem I (IsUnit.mk0 x hx0) hx)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

Prime and irreducible elements: Proposition 5, and Theorem 8(b), which is the heart of "PID ⇒ UFD". The Lean proof follows the human one line by line, using Ideal.mem_span_pair for the Bézout step:

prime_irreducibleLean 4Proved here from basic factsFormally verified

/-- In an integral domain every prime element is irreducible. If `p = a * b`, then `p ∣ a` or
`p ∣ b`; say `a = p * c`. Then `p = p * c * b`, and cancelling `p ≠ 0` gives `1 = c * b`, so `b`
is a unit. -/
theorem prime_irreducible {R : Type*} [CommRing R] [IsDomain R] {p : R} (hp : Prime p) :
    Irreducible p := by
  refine ⟨hp.not_isUnit, fun a b hab => ?_⟩
  rcases hp.dvd_or_dvd ⟨1, by rw [← hab, mul_one]⟩ with ⟨c, hc⟩ | ⟨c, hc⟩
  · right
    have h : p * 1 = p * (c * b) := by
      calc p * 1 = a * b := by rw [mul_one, hab]
        _ = p * (c * b) := by rw [hc, mul_assoc]
    exact IsUnit.of_mul_eq_one_right c (mul_left_cancel₀ hp.ne_zero h).symm
  · left
    have h : p * 1 = p * (c * a) := by
      calc p * 1 = a * b := by rw [mul_one, hab]
        _ = p * (c * a) := by rw [hc, mul_comm a, mul_assoc]
    exact IsUnit.of_mul_eq_one_right c (mul_left_cancel₀ hp.ne_zero h).symm

Axioms used: No axiomsformal/Lumenary/Rings.leanTry it in the Lean web editor

pid_irreducible_primeLean 4Proved here from basic factsFormally verified

/-- **Euclid's lemma in a principal ideal domain**: irreducible elements are prime. Let `p` be
irreducible with `p ∣ a * b` and `p ∤ a`. The ideal `(p, a)` is principal, say `(d)`. From
`p = d * x`, either `x` is a unit — then `(d) = (p)` contains `a`, so `p ∣ a`, impossible — or `d`
is a unit, so `(p, a)` is everything: `1 = r * p + s * a`. Then `b = r * p * b + s * (a * b)` is
divisible by `p`. -/
theorem pid_irreducible_prime {R : Type*} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R]
    {p : R} (hp : Irreducible p) : Prime p := by
  refine ⟨hp.ne_zero, hp.not_isUnit, fun a b hab => ?_⟩
  by_cases hpa : p ∣ a
  · exact Or.inl hpa
  right
  obtain ⟨d, hd⟩ := (IsPrincipalIdealRing.principal (Ideal.span {p, a})).principal
  have hd' : Ideal.span {p, a} = Ideal.span {d} := hd
  have hpd : p ∈ Ideal.span {d} := by rw [← hd']; exact Ideal.subset_span (by simp)
  have had : a ∈ Ideal.span {d} := by rw [← hd']; exact Ideal.subset_span (by simp)
  obtain ⟨x, hx⟩ := Ideal.mem_span_singleton'.mp hpd
  have hpdx : p = d * x := by rw [← hx, mul_comm]
  rcases hp.isUnit_or_isUnit hpdx with hdu | hxu
  · -- `d` is a unit, so `1 ∈ (p, a)`.
    have h1 : (1 : R) ∈ Ideal.span {p, a} := by
      rw [hd', eq_top_of_unit_mem _ hdu (Ideal.mem_span_singleton_self d)]
      exact Submodule.mem_top
    obtain ⟨r, s, hrs⟩ := Ideal.mem_span_pair.mp h1
    obtain ⟨c, hc⟩ := hab
    exact ⟨r * b + s * c, by
      calc b = (r * p + s * a) * b := by rw [hrs, one_mul]
        _ = p * (r * b + s * c) := by rw [add_mul, mul_assoc s, hc]; ring⟩
  · -- `x` is a unit, so `d` divides `p` and `p` divides `d ∣ a`: contradiction.
    exfalso
    apply hpa
    obtain ⟨y, hy⟩ := Ideal.mem_span_singleton'.mp had
    obtain ⟨u, rfl⟩ := hxu
    exact ⟨y * ↑u⁻¹, by rw [← hy, ← hx]; linear_combination (-(y * d)) * Units.mul_inv u⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

The hierarchy itself (Theorems 6, 7 and 9) is in Mathlib as instances, so these proofs are just inferInstance. The real content is in the cited library proofs:

ed_is_pidLean 4Applies a library theoremFormally verified

/-- Every Euclidean domain is a principal ideal domain: a non-zero ideal is generated by any of
its elements of least size. This is Mathlib's instance `EuclideanDomain.instIsPrincipalIdealRing`. -/
theorem ed_is_pid (R : Type*) [EuclideanDomain R] : IsPrincipalIdealRing R :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

pid_is_ufdLean 4Applies a library theoremFormally verified

/-- Every principal ideal domain is a unique factorisation domain. Mathlib's instance
`PrincipalIdealRing.to_uniqueFactorizationMonoid` combines Euclid's lemma (`pid_irreducible_prime`
above) with the ascending chain condition on principal ideals. -/
theorem pid_is_ufd (R : Type*) [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] :
    UniqueFactorizationMonoid R :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

polynomial_pidLean 4Applies a library theoremFormally verified

/-- For a field `K`, the polynomial ring `K[X]` is Euclidean (divide with remainder, measuring
size by degree), hence a principal ideal domain. Mathlib: `Polynomial.instEuclideanDomain`. -/
theorem polynomial_pid (K : Type*) [Field K] : IsPrincipalIdealRing K[X] :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

gaussian_pidLean 4Applies a library theoremFormally verified

/-- The Gaussian integers `ℤ[i]` are Euclidean for the norm `a² + b²` (round the exact quotient
in `ℚ(i)` to the nearest lattice point), hence a principal ideal domain. Mathlib: the
`EuclideanDomain` instance on `GaussianInt`. -/
theorem gaussian_pid : IsPrincipalIdealRing GaussianInt :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

int_poly_ufdLean 4Applies a library theoremFormally verified

/-- `ℤ[X]` is a unique factorisation domain (Gauss's lemma: `R[X]` is a UFD when `R` is).
Mathlib: `Polynomial.uniqueFactorizationMonoid`. -/
theorem int_poly_ufd : UniqueFactorizationMonoid ℤ[X] :=
  inferInstance

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

Theorem 12(a), proved here: $(2, x)$ is not principal in $\Z[x]$ . The proof compares degrees, then the coefficient of $x$ , then constant terms, exactly as in the lesson:

int_poly_not_pidLean 4Proved here from basic factsFormally verified

/-- `ℤ[X]` is **not** a principal ideal domain: the ideal `(2, X)` is not principal. If
`(2, X) = (f)`, then `f ∣ 2` forces `f` to be a constant `c`; `f ∣ X` forces `c ∣ 1`; but every
element `2g + Xh` of `(2, X)` has an even constant term, so `c` is even. -/
theorem int_poly_not_pid : ¬ IsPrincipalIdealRing ℤ[X] := by
  intro h
  obtain ⟨f, hf⟩ := (h.principal (Ideal.span {(2 : ℤ[X]), X})).principal
  have hfs : Ideal.span {(2 : ℤ[X]), X} = Ideal.span {f} := hf
  have h2 : (2 : ℤ[X]) ∈ Ideal.span {f} := by rw [← hfs]; exact Ideal.subset_span (by simp)
  have hX : (X : ℤ[X]) ∈ Ideal.span {f} := by rw [← hfs]; exact Ideal.subset_span (by simp)
  have hf' : f ∈ Ideal.span {(2 : ℤ[X]), X} := by rw [hfs]; exact Ideal.mem_span_singleton_self f
  -- The constant term of `f` is even.
  obtain ⟨a, b, hab⟩ := Ideal.mem_span_pair.mp hf'
  have heven : f.coeff 0 = 2 * a.coeff 0 := by
    rw [← hab]
    simp [mul_comm]
  -- `f` is constant, because it divides `2`.
  obtain ⟨g, hg⟩ := Ideal.mem_span_singleton'.mp h2
  have hf0 : f ≠ 0 := by rintro rfl; simp at hg
  have hg0 : g ≠ 0 := by rintro rfl; simp at hg
  have hdeg : f.natDegree = 0 := by
    have := congrArg natDegree hg
    rw [natDegree_mul hg0 hf0] at this
    have h2deg : (2 : ℤ[X]).natDegree = 0 := natDegree_ofNat 2
    omega
  rw [eq_C_of_natDegree_eq_zero hdeg] at hX
  -- `C c ∣ X` gives `c * q₁ = 1`, so `c ∣ 1`; but `c` is even.
  obtain ⟨q, hq⟩ := Ideal.mem_span_singleton'.mp hX
  have h1 := congrArg (fun p : ℤ[X] => p.coeff 1) hq
  simp only [coeff_mul_C, coeff_X_one] at h1
  rw [heven] at h1
  have h21 : (2 : ℤ) ∣ 1 := ⟨q.coeff 1 * a.coeff 0, by rw [← h1]; ring⟩
  omega

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

Finally $\Z[\sqrt{-5}]$ , which Mathlib writes ℤ√(-5), with elements ⟨x, y⟩ meaning $x + y\sqrt{-5}$ . Mathlib provides the multiplicative norm but no domain instance for negative $d$ , so we prove one ourselves from the norm. We then prove Theorems 10 and 11(a, b) and conclude that $\Z[\sqrt{-5}]$ is not a UFD:

norm_formulaLean 4Proved here from basic factsFormally verified

/-- The norm on `ℤ[√−5]` is `N(x + y√−5) = (x + y√−5)(x − y√−5) = x² + 5y²`. It is
multiplicative (Mathlib's `Zsqrtd.norm_mul`). -/
theorem norm_formula (z : ℤ√(-5)) : z.norm = z.re ^ 2 + 5 * z.im ^ 2 := by
  rw [Zsqrtd.norm_def]
  ring

Axioms used: propext, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

norm_eq_zeroLean 4Proved here from basic factsFormally verified

/-- Only `0` has norm `0`: `x² + 5y² = 0` forces `x = y = 0`. -/
theorem norm_eq_zero (z : ℤ√(-5)) (h : z.norm = 0) : z = 0 := by
  rw [norm_formula] at h
  have hre : z.re ^ 2 = 0 := by nlinarith [sq_nonneg z.re, sq_nonneg z.im]
  have him : z.im ^ 2 = 0 := by nlinarith [sq_nonneg z.re, sq_nonneg z.im]
  ext
  · simpa using hre
  · simpa using him

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

isDomainLean 4Formally verified

/-- `ℤ[√−5]` is an integral domain: if `a * b = 0` then `N(a) N(b) = N(a * b) = 0`, so one of
the norms is `0`, and only `0` has norm `0`. (Mathlib provides this instance for `ℤ[√d]` with
`d` a positive non-square; here `d = −5`.) -/
instance isDomain : IsDomain (ℤ√(-5)) :=
  @NoZeroDivisors.to_isDomain _ _ _ ⟨fun {a b} h => by
    have hn := congrArg Zsqrtd.norm h
    rw [Zsqrtd.norm_mul, Zsqrtd.norm_zero] at hn
    rcases mul_eq_zero.mp hn with ha | hb
    · exact Or.inl (norm_eq_zero a ha)
    · exact Or.inr (norm_eq_zero b hb)⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

norm_ne_twoLean 4Proved here from basic factsFormally verified

/-- No element of `ℤ[√−5]` has norm `2`: `x² + 5y² = 2` forces `y = 0` and then `x² = 2`. -/
theorem norm_ne_two (z : ℤ√(-5)) : z.norm ≠ 2 := by
  rw [norm_formula]
  intro h
  have him : z.im = 0 := by nlinarith [sq_nonneg z.re, sq_nonneg z.im]
  rw [him] at h
  have hle : z.re ≤ 1 := by nlinarith
  have hge : -1 ≤ z.re := by nlinarith
  interval_cases z.re <;> simp at h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

two_mul_threeLean 4Proved here from basic factsFormally verified

/-- Two factorisations of `6`: `2 · 3 = (1 + √−5)(1 − √−5)`. -/
theorem two_mul_three : (2 : ℤ√(-5)) * 3 = ⟨1, 1⟩ * ⟨1, -1⟩ := by
  decide

Axioms used: propextformal/Lumenary/Rings.leanTry it in the Lean web editor

two_irreducibleLean 4Proved here from basic factsFormally verified

/-- `2` is irreducible in `ℤ[√−5]`. It is not a unit (its norm is `4`, units have norm `1`). If
`2 = a * b` then `N(a) N(b) = 4`; neither norm is `2` (`norm_ne_two`), so one of them is `1`, and
that factor is a unit. -/
theorem two_irreducible : Irreducible (2 : ℤ√(-5)) := by
  have hunit : ∀ z : ℤ√(-5), z.norm = 1 → IsUnit z :=
    fun z hz => (Zsqrtd.norm_eq_one_iff' (by norm_num) z).mp hz
  refine ⟨fun h => ?_, fun a b hab => ?_⟩
  · have := (Zsqrtd.norm_eq_one_iff' (by norm_num) 2).mpr h
    rw [norm_formula] at this
    norm_num at this
  · have hn := congrArg Zsqrtd.norm hab
    rw [Zsqrtd.norm_mul, norm_formula 2] at hn
    norm_num at hn
    have ha0 := Zsqrtd.norm_nonneg (by norm_num) a
    have hb0 := Zsqrtd.norm_nonneg (by norm_num) b
    have ha2 := norm_ne_two a
    have hb2 := norm_ne_two b
    have hapos : 0 < a.norm := by
      rcases ha0.lt_or_eq with h | h
      · exact h
      · rw [← h] at hn; simp at hn
    have hbpos : 0 < b.norm := by
      rcases hb0.lt_or_eq with h | h
      · exact h
      · rw [← h] at hn; simp at hn
    have hale : a.norm ≤ 4 := by
      have := mul_le_mul_of_nonneg_left (show (1 : ℤ) ≤ b.norm by omega) ha0
      linarith
    interval_cases hna : a.norm
    · exact Or.inl (hunit a hna)
    · exact absurd rfl ha2
    · omega
    · exact Or.inr (hunit b (by omega))

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

two_not_primeLean 4Proved here from basic factsFormally verified

/-- `2` is not prime in `ℤ[√−5]`: it divides `(1 + √−5)(1 − √−5) = 6` but neither factor, since
`2 * c` always has even real part while `1 ± √−5` has real part `1`. -/
theorem two_not_prime : ¬ Prime (2 : ℤ√(-5)) := by
  intro hp
  rcases hp.dvd_or_dvd ⟨3, two_mul_three.symm⟩ with ⟨c, hc⟩ | ⟨c, hc⟩
  · have := congrArg Zsqrtd.re hc
    simp at this
    omega
  · have := congrArg Zsqrtd.re hc
    simp at this
    omega

Axioms used: propext, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

not_ufdLean 4Proved here from basic factsFormally verified

/-- **`ℤ[√−5]` is not a unique factorisation domain.** In a UFD every irreducible element is
prime, but `2` is irreducible (`two_irreducible`) and not prime (`two_not_prime`). -/
theorem not_ufd : ¬ UniqueFactorizationMonoid (ℤ√(-5)) := fun h =>
  two_not_prime (h.irreducible_iff_prime.mp two_irreducible)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/Rings.leanTry it in the Lean web editor

What is and is not formalised. Proved independently here: Proposition 1(d), Theorem 2, Proposition 3(2, 3) and the kernel ideal, Proposition 5, Theorem 8(b), Theorem 12(a) (non-principality of $(2, x)$ ), and Theorems 10 and 11(a, b) — that $\Z[\sqrt{-5}]$ is a domain but not a UFD. Cited from Mathlib: Theorems 6, 7 and 9, Gauss's lemma for $\Z[x]$ , and the finite-domain theorem in its non-commutative (Wedderburn) form. Not formalised: Theorem 11(c) and the ideal factorisation of $(6)$ , and Theorem 12(b). As far as we know, Mathlib does not contain the fact that $\Z\big[\frac{1+\sqrt{-19}}{2}\big]$ is a non-Euclidean PID.

ComputationC

Census and factorisation by computer

The first program sorts every residue of $\Z/n\Z$ into units, zero divisors and $0$ , counts nilpotents, idempotents and ideals, and checks the general statements of the lesson for every $n \le 60$ .

Units, zero divisors and ideals of Z/nZPythonExact computationExhaustive finite checkComputationally tested

"""Units, zero divisors, nilpotents and ideals in the rings Z/nZ.

For each n the program sorts the residues 0, ..., n - 1 into units (elements
with a multiplicative inverse) and zero divisors (non-zero a with ab = 0 for
some non-zero b), finds the nilpotent elements (a^k = 0) and the idempotents
(e^2 = e), and lists all ideals by brute force. It confirms, for every n up to
60, that each non-zero residue is exactly one of unit or zero divisor, that the
units number phi(n) = #{a : gcd(a, n) = 1}, that the ideals correspond to the
divisors of n, and that Z/nZ is a domain exactly when it is a field, exactly
when n is prime. Exact and exhaustive for these n only.
"""

from math import gcd

def units(n):
    """Residues a in Z/nZ with some b such that a * b = 1 (mod n)."""
    return [a for a in range(n) if any(a * b % n == 1 % n for b in range(n))]

def zero_divisors(n):
    """Non-zero residues a with a * b = 0 (mod n) for some non-zero b."""
    return [a for a in range(1, n) if any(a * b % n == 0 for b in range(1, n))]

def nilpotents(n):
    """Residues a with a^k = 0 (mod n) for some k >= 1 (k = n suffices)."""
    return [a for a in range(n) if pow(a, n, n) == 0]

def idempotents(n):
    """Residues e with e * e = e (mod n)."""
    return [e for e in range(n) if e * e % n == e]

def ideals(n):
    """All ideals of Z/nZ, found by brute force as sorted tuples.

    An ideal is an additive subgroup closed under multiplication by every
    residue. Every subset generated by one element is checked, and the ideal
    generated by a set is the one generated by the gcd, so this is complete;
    the test file also checks completeness against all subsets for small n.
    """
    found = set()
    for a in range(n):
        ideal = tuple(sorted({a * r % n for r in range(n)}))
        found.add(ideal)
    return sorted(found, key=len)

def is_ideal(subset, n):
    """True when subset is non-empty, closed under +, and absorbs products."""
    s = set(subset)
    return bool(s) and all((x + y) % n in s and x * r % n in s
                           for x in s for y in s for r in range(n))

def is_prime(n):
    """Trial division."""
    return n >= 2 and all(n % p for p in range(2, int(n ** 0.5) + 1))

def main():
    print(" n  units  zero divisors  ideals  idempotents  non-zero nilpotents")
    for n in (2, 4, 6, 7, 8, 9, 10, 12, 15, 30):
        u, z = units(n), zero_divisors(n)
        nil = [a for a in nilpotents(n) if a]
        print(f"{n:>2}  {len(u):>5}  {len(z):>13}  {len(ideals(n)):>6}  "
              f"{len(idempotents(n)):>11}  {nil}")
    split = phi = divisors = domain = True
    for n in range(2, 61):
        u, z = set(units(n)), set(zero_divisors(n))
        split &= u.isdisjoint(z) and u | z == set(range(1, n))
        phi &= len(u) == sum(gcd(a, n) == 1 for a in range(n))
        divisors &= len(ideals(n)) == sum(n % d == 0 for d in range(1, n + 1))
        domain &= (not z) == (len(u) == n - 1) == is_prime(n)
    print("For every n from 2 to 60:")
    print(f"  each non-zero residue is a unit or a zero divisor, not both: {split}")
    print(f"  number of units = phi(n) = #{{a : gcd(a, n) = 1}}: {phi}")
    print(f"  number of ideals = number of divisors of n: {divisors}")
    print(f"  no zero divisors <=> every non-zero a a unit <=> n prime: {domain}")
    print()
    print("Epistemic status: exact, exhaustive checks for n <= 60. In a finite")
    print("commutative ring every non-zero element is a unit or a zero divisor,")
    print("and Z/nZ is a field exactly when n is prime: those are theorems, proved")
    print("in the lesson; the table is evidence and illustration, not proof.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Notice the patterns. Nilpotents appear exactly when $n$ has a repeated prime factor. There are $2^{\omega(n)}$ idempotents, where $\omega(n)$ is the number of distinct prime factors; this reflects the Chinese remainder theorem $\Z/n\Z \cong \prod \Z/p^k\Z$ of the next lesson. The table is exact evidence for these $n$ . The statements that hold for all $n$ are the theorems proved above.

The norm makes factorisation in $\Z[i]$ and $\Z[\sqrt{-5}]$ a finite search. A factor of $z$ has norm dividing $N(z)$ , and there are finitely many elements of each norm. The second program lists every factorisation into irreducibles of the integers $2, \dots, 30$ in both rings.

Unique factorisation in Z[i], and its failure in Z[sqrt(-5)]PythonExact computationExhaustive finite checkCounterexampleComputationally tested

"""Factorisation by norms in Z[i] and Z[sqrt(-5)].

An element x + y*sqrt(d) (d = -1 or -5) has norm N = x^2 - d*y^2, and the norm is
multiplicative, so a factor of z has a norm dividing N(z). That makes an exact
search possible: list the elements of each smaller norm and test divisibility.
The program finds every factorisation of 2, ..., 30 into irreducibles (up to
order and units) in both rings, shows that Euclidean division by 2 fails in
Z[sqrt(-5)] (every remainder has norm at least 6 > N(2) = 4), and checks that
rounding the exact quotient always works in Z[i] on a box of examples.
"""

from fractions import Fraction
from functools import lru_cache
from itertools import product

def norm(z, d):
    """N(x + y sqrt(d)) = x^2 - d y^2 (positive for d < 0, z != 0)."""
    x, y = z
    return x * x - d * y * y

def mul(z, w, d):
    """(a + b r)(c + e r) with r^2 = d."""
    return (z[0] * w[0] + d * z[1] * w[1], z[0] * w[1] + z[1] * w[0])

def divide(z, w, d):
    """Return z / w if it lies in Z[sqrt(d)], else None (uses z * conj(w))."""
    n = norm(w, d)
    x, y = mul(z, (w[0], -w[1]), d)
    if x % n or y % n:
        return None
    return (x // n, y // n)

def of_norm(n, d):
    """All elements of norm n (finitely many, since d < 0)."""
    bound = int(n ** 0.5) + 1
    return [(x, y) for x in range(-bound, bound + 1)
            for y in range(-bound, bound + 1) if norm((x, y), d) == n]

def units(d):
    """The units: the elements of norm 1."""
    return of_norm(1, d)

def canonical(z, d):
    """A fixed representative of z up to multiplication by units."""
    return max(mul(z, u, d) for u in units(d))

def proper_divisors(z, d):
    """Divisors a of z with 1 < N(a) < N(z), one per associate class."""
    n = norm(z, d)
    found = set()
    for m in range(2, n):
        if n % m == 0:
            for a in of_norm(m, d):
                if divide(z, a, d) is not None:
                    found.add(canonical(a, d))
    return sorted(found)

def is_irreducible(z, d):
    """Not zero, not a unit, and no factor of intermediate norm."""
    return norm(z, d) > 1 and not proper_divisors(z, d)

@lru_cache(maxsize=None)
def factorisations(z, d):
    """All factorisations of z into irreducibles, as sorted tuples of
    canonical representatives (so order and units are ignored)."""
    if is_irreducible(z, d):
        return frozenset({(canonical(z, d),)})
    result = set()
    for a in proper_divisors(z, d):
        if is_irreducible(a, d):
            for rest in factorisations(divide(z, a, d), d):
                result.add(tuple(sorted(rest + (a,))))
    return frozenset(result)

def show(z, d):
    """Format x + y*sqrt(d) compactly, e.g. 1+r or 2 or -r."""
    x, y = z
    if y == 0:
        return str(x)
    r = "i" if d == -1 else "r"
    coef = "" if abs(y) == 1 else str(abs(y))
    if x == 0:
        return f"{'-' if y < 0 else ''}{coef}{r}"
    return f"{x}{'-' if y < 0 else '+'}{coef}{r}"

def best_remainder(a, b, d, box=6):
    """Least N(a - q b) over q = (s, t) with |s|, |t| <= box."""
    return min(norm((a[0] - p[0], a[1] - p[1]), d)
               for p in (mul(q, b, d) for q in product(range(-box, box + 1),
                                                         repeat=2)))

def gaussian_rounding_works(limit=6):
    """Check N(a - q b) < N(b) with q = a/b rounded, for a, b in a box."""
    rng = range(-limit, limit + 1)
    for a in product(rng, repeat=2):
        for b in product(rng, repeat=2):
            if b == (0, 0):
                continue
            n = norm(b, -1)
            x, y = mul(a, (b[0], -b[1]), -1)
            q = (round(Fraction(x, n)), round(Fraction(y, n)))
            r = (a[0] - mul(q, b, -1)[0], a[1] - mul(q, b, -1)[1])
            if norm(r, -1) >= n:
                return False
    return True

def main():
    for d, name in ((-1, "Z[i]"), (-5, "Z[sqrt(-5)]  (r = sqrt(-5))")):
        print(f"{name}: integers 2..30 with more than one factorisation")
        several = []
        for n in range(2, 31):
            facs = factorisations((n, 0), d)
            if len(facs) > 1:
                several.append(n)
                first, second = sorted(facs, key=len)[:2]
                shown = "  =  ".join(" ".join(f"({show(p, d)})" for p in f)
                                     for f in (first, second))
                print(f"  {n:>2}: {len(facs)} ways, e.g. {shown}")
        if not several:
            print("  none: every factorisation is unique up to order and units")
    print("Irreducible but not prime in Z[sqrt(-5)]: 2 divides (1+r)(1-r) = 6,")
    print(f"  2 irreducible: {is_irreducible((2, 0), -5)}; 2 divides 1+r: "
          f"{divide((1, 1), (2, 0), -5) is not None}")
    print(f"Euclid fails in Z[sqrt(-5)]: least N((1+r) - 2q) = "
          f"{best_remainder((1, 1), (2, 0), -5)} >= N(2) = 4")
    print(f"Z[i]: rounding a/b gives N(remainder) < N(b) for all a, b with")
    print(f"  coordinates in -6..6: {gaussian_rounding_works()}")
    print()
    print("Epistemic status: exact searches, justified by the multiplicative")
    print("norm, for the integers 2..30 only. They illustrate, but do not prove,")
    print("that Z[i] is a UFD (proved via its Euclidean algorithm) and exhibit a")
    print("genuine counterexample to unique factorisation in Z[sqrt(-5)].")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

In $\Z[i]$ every factorisation is unique, as Theorem 9 guarantees. In $\Z[\sqrt{-5}]$ ten of the integers up to $30$ factor in more than one way, and $18$ factors in five different ways. The searches are exact, and the failure of Euclidean division by $2$ is a proved counterexample: $(1 - 2s) + (1 - 2t)\sqrt{-5}$ has norm at least $1 + 5 = 6 \gt 4$ for all integers $s, t$ , because odd numbers have odd squares.

Explore

Explore: units and zero divisors on a clock

Switch the clock to the multiplication tab and search for multiplicative partners. For a prime number of hours, every non-zero residue has a partner, so $\Z/p\Z$ is a field. For $k = 12$ , only $1, 5, 7, 11$ do. Each of the others times some non-zero residue lands on $0$ , so those are zero divisors. Try $k = 8$ , $9$ , $10$ and $15$ , and predict which residues will have partners before you look: exactly those coprime to $k$ .

The clock laboratory

On a clock with k hours, counting wraps around. Explore adding and multiplying.

Hours on the clock k = 12

Start at 9Move forward 5

9 + 5 = 14 ≡ 2 (mod 12)

14 hours forward on a 12-hour clock lands on 2: the remainder when 14 is divided by 12.

Exercises

1. Rings, ideals and fields

Warm-upHuman

How many units does the ring $\Z/12\Z$ have?

2. Rings, ideals and fields

Warm-upHuman

Which of these rings are integral domains? (Select all that apply.)

Choose all that apply

3. Rings, ideals and fields

CoreHuman

Which of these subsets of $\Z[x]$ are ideals? (Select all that apply.)

Choose all that apply

the constant polynomials

\Z

(x)

: the polynomials with constant term

0

the polynomials of degree at most

1

, with

0

the polynomials whose constant term is even

4. Rings, ideals and fields

CoreHuman

$\Q[x]$ is a principal ideal domain. Which polynomial generates the ideal $I = (x^2 - 1,\; x^2 - 3x + 2)$ ?

Choose one

x - 1

(x - 1)(x + 1)(x - 2)

1

x + 1

5. Rings, ideals and fields

CoreHuman

In the proof that a Euclidean domain is a PID, we take a non-zero ideal $I$ , choose $b \in I \setminus \{0\}$ of least size $\delta(b)$ , and divide any $a \in I$ as $a = qb + r$ with $r = 0$ or $\delta(r) \lt \delta(b)$ . Why must $r = 0$ ?

Choose one

Because

r = a - qb

lies in

I

, and

b

has the least size among non-zero elements of

I

.Because

b

divides

a

by assumption.Because

\delta(r) \lt \delta(b)

and sizes are never negative.Because a Euclidean domain is a field.

6. Rings, ideals and fields

CoreHuman

In $\Z[\sqrt{-5}]$ the element $3$ is irreducible. Which of these products show that $3$ is not prime — that is, $3$ divides the product but divides neither factor? (Select all that apply.)

Choose all that apply

(1 + \sqrt{-5})(1 - \sqrt{-5}) = 6

(2 + \sqrt{-5})(2 - \sqrt{-5}) = 9

3 \cdot 3 = 9

2 \cdot 5 = 10

7. Rings, ideals and fields

CoreHuman

How many Gaussian integers $x + yi$ have norm $x^2 + y^2 = 25$ ?

8. Rings, ideals and fields

CoreFormal

Which Lean statement formalises “every finite integral domain is a field”?

Choose one

theorem t (R : Type*) [CommRing R] [IsDomain R] [Finite R] : IsField Rtheorem t (R : Type*) [Field R] [Finite R] : IsDomain Rtheorem t (R : Type*) [CommRing R] [Finite R] : IsField Rtheorem t (R : Type*) [CommRing R] [IsDomain R] : IsField R

9. Rings, ideals and fields

StretchComputational

Write classify(n) returning a pair (units, zero_divisors) of sorted lists for the ring $\Z/n\Z$ ( $n \ge 2$ ): units are the $a$ with $ab \equiv 1$ for some $b$ , and zero_divisors the non-zero $a$ with $ab \equiv 0$ for some non-zero $b$ . Then check that together they contain every non-zero residue exactly once.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Every ring is commutative and has a $1$ ." Matrix rings and the quaternions are not commutative, and some authors do not require a $1$ (then $2\Z$ is a ring and homomorphisms need not preserve $1$ ). State your conventions. In this lesson rings have $1$ , homomorphisms preserve it, and commutativity is assumed only when said.

Misconception

"Ideals are subrings" (or the reverse). A subring contains $1$ ; a proper ideal never does, since an ideal containing a unit is everything. $\Z \subset \Q$ is a subring that is not an ideal, and $2\Z \subset \Z$ is an ideal that is not a subring. Ideals are the kernels of homomorphisms; subrings are their images.

Misconception

"Irreducible and prime mean the same thing." In $\Z$ , in $k[x]$ and in every UFD they coincide. In general, prime implies irreducible (Proposition 5) but not conversely: $2$ is irreducible in $\Z[\sqrt{-5}]$ and divides $(1 + \sqrt{-5})(1 - \sqrt{-5})$ without dividing either factor.

Misconception

"A domain in which every element factors into irreducibles has unique factorisation." Existence and uniqueness are separate. In $\Z[\sqrt{-5}]$ every non-zero non-unit does factor into irreducibles (induct on the norm), but not uniquely. Uniqueness needs Euclid's lemma, that is, irreducibles must be prime.

Misconception

"Every PID is Euclidean" and "every UFD is a PID". $\Z\big[\frac{1 + \sqrt{-19}}{2}\big]$ is a PID that is not Euclidean, and $\Z[x]$ and $k[x, y]$ are UFDs that are not PIDs. The hierarchy is strict.

Misconception

" $\Z/n\Z$ is always a field" or "a ring without zero divisors is a field". $\Z/6\Z$ has zero divisors. $\Z$ has none and is not a field. Finiteness is what turns "no zero divisors" into "every non-zero element is a unit" (Theorem 2).

ViewpointsH

Many ways of seeing

Geometry— Ideals are shapes

In the polynomial ring $\C[x_1, \dots, x_n]$ , an ideal $I$ cuts out a shape, the variety $V(I) = \{p \in \C^n \mid f(p) = 0 \text{ for all } f \in I\}$ . Bigger ideals give smaller shapes: $(x^2 + y^2 - 1)$ is the circle, $(x^2 + y^2 - 1, y)$ is the two points $(\pm 1, 0)$ , and $(x - a, y - b)$ is the single point $(a, b)$ . Hilbert's Nullstellensatz (1893) makes the dictionary exact. The maximal ideals of $\C[x_1, \dots, x_n]$ are exactly the ideals $(x_1 - a_1, \dots, x_n - a_n)$ of points. Prime ideals correspond to irreducible varieties, and $V(I) = V(J)$ iff $I$ and $J$ have the same radical. Ring theory becomes geometry: this is the starting point of commutative algebra and algebraic geometry. Unique factorisation also has a geometric meaning: in a UFD, every hypersurface is cut out by a single equation.

Topology— The space of primes

Grothendieck made every commutative ring $R$ into a space. Its points are the prime ideals, forming $\operatorname{Spec} R$ . Its closed sets are the sets $V(I) = \{P \mid P \supseteq I\}$ ; this is the Zariski topology. $\operatorname{Spec} \Z$ has a closed point for each prime $p$ , and one generic point $(0)$ , whose closure is the whole space. Its proper closed sets are the finite sets of primes. The space is connected, and that is the topological form of the fact that $\Z$ has no idempotents other than $0$ and $1$ . In general $\operatorname{Spec} R$ is disconnected iff $R \cong R_1 \times R_2$ with both factors non-zero. This explains the idempotents counted by the first experiment: $\operatorname{Spec}(\Z/n\Z)$ is a finite discrete set with one point for each prime dividing $n$ .

Number theory— Ideal numbers and the class group

For a number field $K$ , its ring of integers $\mathcal{O}_K$ need not be a UFD. It is always a Dedekind domain: non-zero ideals factor uniquely into prime ideals. The failure of unique factorisation of elements is measured by the class group, the group of ideals modulo principal ideals. It is finite, and its order is the class number. For $\Q(\sqrt{-5})$ the class number is $2$ : the non-principal ideal $P = (2, 1 + \sqrt{-5})$ has $P^2 = (2)$ principal. By the Baker–Heegner–Stark theorem (1952–1967), the imaginary quadratic fields with class number $1$ are exactly $\Q(\sqrt{-d})$ for $d = 1, 2, 3, 7, 11, 19, 43, 67, 163$ . Kummer proved Fermat's Last Theorem for every prime $p$ that does not divide the class number of $\Q(e^{2\pi i/p})$ (the regular primes). See algebraic number theory.

Analysis— Rings of functions

Analysts meet rings of functions everywhere. For a compact Hausdorff space $X$ , the maximal ideals of $C(X, \R)$ are exactly the ideals $M_x = \{f \mid f(x) = 0\}$ of points (Gelfand–Kolmogorov, 1939). So $X$ can be recovered from the ring. For commutative C*-algebras, Gelfand duality makes this an equivalence between compact Hausdorff spaces and rings with extra analytic structure. Locally, the ring of convergent power series $\C\{z\}$ (germs of holomorphic functions at $0$ ) is a PID with essentially one prime, $z$ . Every non-zero germ is $z^k$ times a unit, where $k$ is its order of vanishing, so it is a discrete valuation ring. In several variables the ring of germs is still a UFD (a consequence of the Weierstrass preparation theorem), but no longer a PID.

Category theory— The category of rings

Rings and homomorphisms form a category $\mathbf{Ring}$ , with commutative rings forming $\mathbf{CRing}$ . $\Z$ is initial: every ring receives exactly one homomorphism from $\Z$ , determined by $1 \mapsto 1$ . The zero ring is terminal. Kernels in the categorical sense are subtle, because $\mathbf{Ring}$ is not additive; ideals are best seen as the kernel pairs of homomorphisms, and quotients as coequalisers (limits and colimits). $\operatorname{Spec}$ is a contravariant functor: a homomorphism $f : R \to S$ pulls prime ideals back to prime ideals, giving a continuous map $\operatorname{Spec} S \to \operatorname{Spec} R$ . The category of Grothendieck's affine schemes is equivalent to $\mathbf{CRing}^{\mathrm{op}}$ — algebra read backwards as geometry.

Wonder Trails

Rings grow out of clock arithmetic and the search for inverses. These optional trails start there.

Wonder Trail · Optional · never gradedInverses and structureEvery integer can be added to another integer to get

0

. So why can almost no integer be multiplied by another integer to get

1

?Follow the trail Wonder Trail · Optional · never gradedClock arithmeticIt's 9 o'clock. What time will it be in 5 hours — and in 29 hours? Can a clock teach us a whole new kind of arithmetic?Follow the trail

History & global context

History and global context

Division and Euclid's lemma. Euclid's Elements (Book VII, c. 300 BCE) contains the Euclidean algorithm and the lemma that a prime dividing a product divides a factor (VII.30). Unique factorisation of integers was first stated and proved explicitly by Carl Friedrich Gauss in the Disquisitiones Arithmeticae (1801).
Arithmetic with $\sqrt{N}$ . Brahmagupta (628 CE) discovered the composition identity $(x^2 - Ny^2)(z^2 - Nw^2) = (xz + Nyw)^2 - N(xw + yz)^2$ , which is the multiplicativity of the norm on $\Z[\sqrt N]$ . Bhāskara II (12th century) used it in the chakravāla method for $x^2 - Ny^2 = 1$ . In Baghdad, al-Samawʾal (12th century) developed the arithmetic of polynomials, including long division.
New integers. Euler (1770) worked with numbers $a + b\sqrt{-2}$ and $a + b\sqrt{-3}$ , assuming unique factorisation. Gauss (1832) introduced the Gaussian integers to state biquadratic reciprocity and proved that they factor uniquely.
Failure and repair. Lamé's 1847 attempt on Fermat's Last Theorem assumed unique factorisation in cyclotomic integers, and Liouville objected at once. Ernst Kummer had found failures in 1844 and introduced "ideal complex numbers" (1847), which let him prove the theorem for regular primes. Richard Dedekind (1871) replaced ideal numbers by ideals, sets of actual numbers, and proved unique factorisation of ideals. Leopold Kronecker developed a parallel theory of divisors.
Abstraction. David Hilbert's Zahlbericht (1897) used the word Zahlring. Abraham Fraenkel gave axioms for rings in 1914. Emmy Noether's Idealtheorie in Ringbereichen (1921) founded modern ring theory, with chain conditions (Noetherian rings) like the one in the proof of Theorem 9. Wolfgang Krull, Emil Artin, B. L. van der Waerden's Moderne Algebra (1930–31) and later Alexander Grothendieck's schemes (1960s) shaped the subject as it is taught today.

When factorisation stops being unique

Two operations, and the multiples of a number

Rings, ideals and the factorisation hierarchy

A gallery of rings

Units, zero divisors and ideals

Euclidean domain ⇒ PID ⇒ UFD

Where the hierarchy breaks

Rings in Lean and Mathlib

Census and factorisation by computer

Explore: units and zero divisors on a clock

Exercises

Common misconceptions

Many ways of seeing

Wonder Trails

History and global context

Further reading