Number theory

TheoremSum of two squares#

Fermat's theorem on sums of two squares says that an odd prime number \(p\) can be written as \(p = a^2 + b^2\) with integers \(a\) and \(b\) if and only if \(p \equiv 1 \pmod 4\). Together with \(2 = 1^2 + 1^2\), this settles which primes are sums of two squares, and because such sums are closed under multiplication it leads to a description of every sum of two squares through its prime factorization. The theorem is a basic result in the arithmetic of quadratic forms and describes how ordinary primes factor in the Gaussian integers.

Statement

Let \(p\) be a prime. If \(p\) is not congruent to \(3\) modulo \(4\), that is, if \(p = 2\) or \(p \equiv 1 \pmod 4\), then there are natural numbers \(a\) and \(b\) with \(a^2 + b^2 = p\). Conversely, a prime \(p \equiv 3 \pmod 4\) is never a sum of two squares: every square is congruent to \(0\) or \(1\) modulo \(4\), so a sum of two squares is congruent to \(0\), \(1\) or \(2\) modulo \(4\).

The representation is essentially unique: if \(p = a^2 + b^2 = c^2 + d^2\) with \(a, b, c, d \ge 0\), then \(\{a, b\} = \{c, d\}\). The reason is unique factorization in the Gaussian integers: an element of norm \(p\) is irreducible, so \(p = (a + bi)(a - bi)\) is a factorization into Gaussian primes, and \(c + di\), which also has norm \(p\) and divides \(p\), must be an associate of \(a + bi\) or of \(a - bi\). These associates are \(\pm a \pm bi\) and \(\pm b \pm ai\).

Examples

The primes below \(50\) that are congruent to \(1\) modulo \(4\) decompose as

\[5 = 1^2 + 2^2, \quad 13 = 2^2 + 3^2, \quad 17 = 1^2 + 4^2, \quad 29 = 2^2 + 5^2, \quad 37 = 1^2 + 6^2, \quad 41 = 4^2 + 5^2.\]

The primes \(3, 7, 11, 19, 23, 31, 43, 47\) are congruent to \(3\) modulo \(4\) and are not sums of two squares.

Proof

The case \(p = 2\) is \(1^2 + 1^2\), so let \(p \equiv 1 \pmod 4\).

Step 1: \(-1\) is a square modulo \(p\). For a prime \(p\), \(-1\) is a square modulo \(p\) if and only if \(p\) is not congruent to \(3\) modulo \(4\). The direction needed here follows from Wilson's theorem, \((p-1)! \equiv -1 \pmod p\). Pairing each factor \(j \le (p-1)/2\) with \(p - j \equiv -j\) gives

\[(p-1)! \equiv (-1)^{(p-1)/2} \left( \left( \tfrac{p-1}{2} \right)! \right)^2 \pmod p,\]

and since \((p-1)/2\) is even, \(k = \left( \tfrac{p-1}{2} \right)!\) satisfies \(k^2 \equiv -1 \pmod p\).

Step 2: \(p\) is not prime in the Gaussian integers. The Gaussian integers \(\mathbb{Z}[i] = \{x + yi : x, y \in \mathbb{Z}\}\) form a Euclidean domain for the norm \(N(x + yi) = x^2 + y^2\), which is multiplicative. Hence \(\mathbb{Z}[i]\) is a principal ideal domain, and in it every irreducible element is prime. Now \(p\) divides \(k^2 + 1 = (k + i)(k - i)\) but divides neither factor, since \((k \pm i)/p\) has imaginary part \(\pm 1/p\), which is not an integer. So \(p\) is not prime in \(\mathbb{Z}[i]\), and therefore not irreducible. More precisely, a prime number stays prime in \(\mathbb{Z}[i]\) if and only if it is congruent to \(3\) modulo \(4\).

Step 3: taking norms. Since \(N(p) = p^2 \ne 1\), the element \(p\) is neither zero nor a unit, and since it is not irreducible it can be written as \(p = \alpha \beta\) with neither \(\alpha\) nor \(\beta\) a unit. Then \(N(\alpha) N(\beta) = N(p) = p^2\), and neither norm is \(1\), because the elements of norm \(1\) are exactly the units. So \(N(\alpha) = p\), and writing \(\alpha = a + bi\) gives \(a^2 + b^2 = p\). This step is the statement that a prime number that is not irreducible in \(\mathbb{Z}[i]\) is a sum of two squares.

Consequences
In Mathlib

Mathlib states the theorem for a natural number \(p\) assumed to be prime, with the single hypothesis that \(p\) leaves a remainder other than \(3\) on division by \(4\); this covers \(p = 2\) and the primes congruent to \(1\) modulo \(4\) in one statement. The squares are squares of natural numbers, which loses nothing, since an integer and its absolute value have the same square. The theorem itself gives only the existence direction; the impossibility for primes congruent to \(3\) modulo \(4\) appears in the proof that such primes stay prime in the Gaussian integers and as a special case of the factorization criterion. The uniqueness of the representation is not stated in Mathlib. The Gaussian integers are the case \(d = -1\) of Mathlib's rings \(\mathbb{Z}[\sqrt{d}]\), made into a Euclidean domain through the norm. The factorization criterion is stated for every natural number, including \(0\): the number \(0\) is \(0^2 + 0^2\), it has no prime factors, and its \(q\)-adic valuation is defined to be \(0\), so both sides hold. Mathlib also uses the criterion to decide by computation whether a given number is a sum of two squares.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibNat.Prime.sq_add_sq
Uses 7
Statement usesPrime numbers · Integer · Congruence in \(\Z\)
Proof usesWilson’s Lemma · Euclidean domain · Principal ideal domain · Irreducible element

TheoremSum of four squares#

Lagrange's four-square theorem says that every natural number is a sum of four squares of natural numbers. Four is the least number that works for all natural numbers, since \(7\) is not a sum of three squares, so the theorem settles completely which count of squares suffices. It is a model case of an additive problem in number theory, and its proof combines an algebraic identity with a descent argument on prime numbers.

Statement

For every natural number \(n\) there are natural numbers \(a, b, c, d\) with

\[n = a^2 + b^2 + c^2 + d^2\]

(the four-square theorem). Zero is allowed among \(a, b, c, d\), so the theorem equivalently says that every natural number is a sum of at most four nonzero squares. Since natural numbers are integers, and an integer and its negative have the same square, the statement is equivalent to its version with \(a, b, c, d\) ranging over the integers.

Examples
  • \(0 = 0^2 + 0^2 + 0^2 + 0^2\) and \(1 = 1^2 + 0^2 + 0^2 + 0^2\).
  • \(7 = 2^2 + 1^2 + 1^2 + 1^2\), and three squares do not suffice: every square is congruent to \(0\), \(1\) or \(4\) modulo \(8\), and no sum of three of these residues is congruent to \(7\) modulo \(8\).
  • \(15 = 3^2 + 2^2 + 1^2 + 1^2\) and \(23 = 3^2 + 3^2 + 2^2 + 1^2\), two more numbers that need four nonzero squares.
  • A representation need not be unique: \(28 = 4^2 + 2^2 + 2^2 + 2^2 = 5^2 + 1^2 + 1^2 + 1^2\).
Proof

The proof has three steps.

Euler's four-square identity. In every commutative ring,

\[\begin{aligned} (a^2+b^2+c^2+d^2)(x^2+y^2+z^2+w^2) &= (ax-by-cz-dw)^2 + (ay+bx+cw-dz)^2 \\ &\quad + (az-bw+cx+dy)^2 + (aw+bz-cy+dx)^2 \end{aligned}\]

(the identity), which is checked by expanding both sides. So a product of two sums of four squares is again one. Since \(0\) and \(1\) are sums of four squares and every integer \(n \ge 2\) is a product of primes, it suffices to treat primes.

A first multiple of \(p\). Let \(p\) be a prime. Every residue class modulo \(p\) is a sum of two squares of residues. For \(p = 2\) this is clear from \(0 = 0^2 + 0^2\) and \(1 = 1^2 + 0^2\). For odd \(p\) and a residue \(c\), the \((p+1)/2\) residues \(x^2\) with \(0 \le x \le (p-1)/2\) are distinct, as are the \((p+1)/2\) residues \(c-y^2\) with \(0 \le y \le (p-1)/2\), so the two lists, with \(p+1\) entries among \(p\) classes, share a value, and \(x^2 + y^2 \equiv c\). Taking \(c = -1\), with \(x\) and \(y\) at most \(p/2\), shows that there are natural numbers \(a, b, k\) with \(0 < k < p\) and \(a^2 + b^2 + 1 = kp\). Hence some multiple \(mp\) with \(0 < m < p\) is a sum of four squares.

Descent. Let \(m\) be the least positive integer such that \(mp\) is a sum of four squares \(a^2+b^2+c^2+d^2\), and suppose \(m > 1\); then \(m < p\).

So \(m = 1\), and every prime is a sum of four squares.

In Mathlib

Mathlib states the theorem for natural numbers, with the four squares taken of natural numbers and zero allowed among them. Euler's identity is proved for an arbitrary commutative ring, and a separate version for natural numbers replaces each of the four bracketed integers by its absolute value, so that the product of two sums of four squares of natural numbers is a sum of four squares of natural numbers. The prime case is proved first by the descent above, and the general case follows by induction over products of primes. The fact that every residue modulo a prime is a sum of two squares is deduced, for odd primes, from a general counting lemma about two quadratic polynomials over a finite field of odd order.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibNat.sum_four_squares
Uses 4
Statement usesNatural number
Proof usesPrime numbers · Integer · Congruence in \(\Z\)

TheoremQuadratic reciprocity#

Quadratic reciprocity is a theorem of elementary number theory relating two questions that look unrelated: whether an odd prime \(q\) is a square modulo a different odd prime \(p\), and whether \(p\) is a square modulo \(q\). It says the two answers agree unless both primes are congruent to \(3\) modulo \(4\), in which case they are opposite. Together with two supplementary laws it gives an efficient way, especially in its Jacobi-symbol form, to decide whether an equation \(x^2 \equiv a \pmod p\) has a solution, and it is the simplest case of the reciprocity laws of algebraic number theory.

Statement

Let \(p\) be a prime and \(a\) an integer. The Legendre symbol \(\left(\frac{a}{p}\right)\) is \(0\) if \(p\) divides \(a\), \(1\) if \(a\) is congruent modulo \(p\) to the square of an integer not divisible by \(p\), and \(-1\) otherwise. In the last two cases \(a\) is called a quadratic residue or a quadratic nonresidue modulo \(p\). For fixed \(p\) the symbol is multiplicative in \(a\).

The law of quadratic reciprocity: if \(p\) and \(q\) are distinct odd primes, then \(\left(\frac{p}{q}\right)\left(\frac{q}{p}\right) = (-1)^{\frac{p-1}{2}\cdot\frac{q-1}{2}}\). The exponent is even unless \(p \equiv q \equiv 3 \pmod 4\). Equivalently, for odd primes \(p\) and \(q\), \(\left(\frac{q}{p}\right) = (-1)^{\frac{p-1}{2}\cdot\frac{q-1}{2}}\left(\frac{p}{q}\right)\), a form that also holds trivially when \(p = q\), since both sides are \(0\). Stated without symbols: if \(p \equiv 1 \pmod 4\) and \(q\) is an odd prime, then \(q\) is a square modulo \(p\) if and only if \(p\) is a square modulo \(q\); if \(p\) and \(q\) are distinct primes both congruent to \(3\) modulo \(4\), then \(q\) is a square modulo \(p\) if and only if \(p\) is not a square modulo \(q\).

The supplementary laws treat \(-1\) and \(2\): \(-1\) is a square modulo a prime \(p\) exactly when \(p\) is not congruent to \(3\) modulo \(4\), and for an odd prime \(p\), \(2\) is a square modulo \(p\) exactly when \(p \equiv 1\) or \(p \equiv 7 \pmod 8\).

Examples
  • Since \(5 \equiv 1 \pmod 4\), \(\left(\frac{3}{5}\right) = \left(\frac{5}{3}\right) = \left(\frac{2}{3}\right) = -1\): the nonzero squares modulo \(5\) are \(1\) and \(4\), and \(3\) is not among them.
  • Both \(3\) and \(7\) are congruent to \(3\) modulo \(4\), so \(\left(\frac{3}{7}\right) = -\left(\frac{7}{3}\right) = -\left(\frac{1}{3}\right) = -1\). Indeed the nonzero squares modulo \(7\) are \(1\), \(2\) and \(4\).
  • To decide whether \(37\) is a square modulo the prime \(101\), flip and reduce repeatedly, using multiplicativity and \(37 \equiv 1 \pmod 4\): $\(\left(\frac{37}{101}\right) = \left(\frac{101}{37}\right) = \left(\frac{27}{37}\right) = \left(\frac{3}{37}\right)^3 = \left(\frac{37}{3}\right)^3 = \left(\frac{1}{3}\right)^3 = 1.\)$ So \(x^2 \equiv 37 \pmod{101}\) has a solution; one is \(x = 21\), since \(21^2 = 441 = 4 \cdot 101 + 37\).
  • For a prime \(p > 3\), reciprocity gives \(\left(\frac{3}{p}\right) = (-1)^{\frac{p-1}{2}}\left(\frac{p}{3}\right)\), and checking the residues of \(p\) modulo \(12\) shows that \(3\) is a square modulo \(p\) if and only if \(p \equiv \pm 1 \pmod{12}\).
Consequences

The law turns a question about \(p\) modulo \(q\) into a question about \(q\) modulo \(p\), and the second number can be reduced modulo \(p\). Alternating flips and reductions, after factoring out powers of \(2\) and signs with the supplementary laws, computes any Legendre symbol, although each step may require factoring a number; the Jacobi symbol described below removes that need. The law also shows that for a fixed odd prime \(q\) the value \(\left(\frac{q}{p}\right)\), as \(p\) ranges over the odd primes other than \(q\), depends only on \(p\) modulo \(4q\), so the primes modulo which \(q\) is a square are described by congruence conditions. The first supplementary law is the starting point of several proofs of the theorem that a prime \(p \equiv 1 \pmod 4\) is a sum of two squares.

Proof

A short proof goes through Gauss's lemma and a refinement of it known as Eisenstein's lemma. Let \(p\) be an odd prime. For an odd natural number \(a\) not divisible by \(p\), Eisenstein's lemma gives

\[\left(\frac{a}{p}\right) = (-1)^{S(a,p)}, \qquad S(a,p) = \sum_{x=1}^{(p-1)/2} \left\lfloor \frac{xa}{p} \right\rfloor .\]

It follows from Gauss's lemma, which expresses \(\left(\frac{a}{p}\right)\) as \((-1)^{\mu}\), where \(\mu\) counts the \(x\) among \(1, \dots, \frac{p-1}{2}\) for which the remainder of \(ax\) on division by \(p\) exceeds \(p/2\). Gauss's lemma in turn compares the product of the numbers \(ax\) with \(\left(\frac{p-1}{2}\right)!\) and uses Euler's criterion, \(\left(\frac{a}{p}\right) \equiv a^{(p-1)/2} \pmod p\), which is proved from Fermat's little theorem and the fact that a polynomial of degree \(d\) has at most \(d\) roots modulo \(p\).

Now let \(p\) and \(q\) be distinct odd primes. The sum \(S(q,p)\) counts the lattice points \((x, y)\) with \(1 \le x \le \frac{p-1}{2}\) and \(1 \le y \le \frac{q-1}{2}\) lying below the line \(py = qx\), and \(S(p,q)\) counts those above it. No lattice point of the rectangle lies on the line, since \(qx = py\) would force \(p\) to divide \(x\). Hence \(S(q,p) + S(p,q) = \frac{p-1}{2}\cdot\frac{q-1}{2}\), and multiplying the two instances of Eisenstein's lemma proves the theorem.

A second proof works in a field of characteristic \(q\) containing a primitive \(p\)-th root of unity \(\zeta\). The Gauss sum \(g = \sum_{a=1}^{p-1} \left(\frac{a}{p}\right)\zeta^a\) satisfies \(g^2 = (-1)^{\frac{p-1}{2}} p\), while raising to the \(q\)-th power, the Frobenius map, which is additive in characteristic \(q\), gives \(g^q = \left(\frac{q}{p}\right) g\); here one uses that \(\left(\frac{a}{p}\right)^q = \left(\frac{a}{p}\right)\) because \(q\) is odd. Since \(g^2 = \pm p\) is nonzero in characteristic \(q \ne p\), \(g\) is invertible, so \(g^{q-1} = \left(\frac{q}{p}\right)\). Comparing this with Euler's criterion for \((-1)^{\frac{p-1}{2}} p\) modulo \(q\), using the first supplementary law for \(q\) and the fact that \(1 \ne -1\) in characteristic \(q\), yields the law.

Generalizations

The Jacobi symbol extends the Legendre symbol to an odd positive modulus \(b\) by multiplying the Legendre symbols over the prime factors of \(b\), counted with multiplicity. Reciprocity carries over: for odd natural numbers \(a\) and \(b\), the Jacobi symbols satisfy \(\left(\frac{a}{b}\right) = (-1)^{\frac{a-1}{2}\cdot\frac{b-1}{2}}\left(\frac{b}{a}\right)\). This allows symbols to be computed without factoring. Further generalizations include cubic and biquadratic reciprocity, the Hilbert reciprocity law for Hilbert symbols over the rationals, and the Artin reciprocity law of class field theory.

In Mathlib

Mathlib writes the prime first, so the symbol \(\left(\frac{a}{p}\right)\) is a function of \(a\) for each fixed \(p\), and it defines this function as the quadratic character of the field of integers modulo \(p\). The exponent in the law is written with natural-number division rounding down, as the product of \(\lfloor p/2 \rfloor\) and \(\lfloor q/2 \rfloor\); for odd primes this equals \(\frac{p-1}{2}\cdot\frac{q-1}{2}\). The proof does not use lattice points. It derives the law from a statement about arbitrary finite fields: for two finite fields \(F\) and \(F'\) of distinct odd characteristics, the quadratic character of \(F\) at the number of elements of \(F'\) equals the quadratic character of \(F'\) at \(\chi_F(-1)\) times the number of elements of \(F\), where \(\chi_F\) is the quadratic character of \(F\); this rests on quadratic Gauss sums. Gauss's and Eisenstein's lemmas are proved separately. The Jacobi symbol is defined for every natural number modulus, taking value \(1\) at modulus \(0\), and its reciprocity law needs no coprimality hypothesis, since both sides vanish when \(a\) and \(b\) share a factor.

Written for Trough, under CC BY-SA 4.0.

Sources
MathliblegendreSym.quadratic_reciprocity
Uses 6 · Used by 1
Statement usesPrime numbers · Congruence in \(\Z\)
Proof usesFermat's little theorem · Field · Characteristic of a ring · Frobenius morphism
Used byLucas-Lehmer primality test

DefinitionSolutions to Pell's equation (Number theory)#

The solutions to Pell's equation \(x^2 - dy^2 = 1\) in the special case \(d = a^2 - 1\), for an integer \(a > 1\), can be written down completely: the solutions in natural numbers form a single sequence of pairs, the Pell sequence, generated from the obvious solution \((a, 1)\) by a linear recursion, and the integer solutions are these up to sign. In this case the fundamental solution is evident, and the case serves as a model for the general theory of Pell's equation; its explicit recursion makes the solutions easy to compute and to reason about. Their growth, divisibility and congruence properties are the main ingredients of Matiyasevič's theorem that exponentiation is Diophantine.

Definition

Fix a natural number \(a > 1\) and put \(d = a^2 - 1\). Then \(a^2 - d \cdot 1^2 = 1\), so \((a, 1)\) solves the equation. The Pell sequence \((x_n, y_n)\) is defined by the recursion

\[(x_0, y_0) = (1, 0), \qquad (x_{n+1}, y_{n+1}) = (a x_n + d y_n,\; x_n + a y_n).\]

In the ring \(\mathbb{Z}[\sqrt d]\) of numbers \(u + v\sqrt d\) with \(u, v\) integers, the recursion says that \(x_{n+1} + y_{n+1}\sqrt d\) equals \((x_n + y_n\sqrt d)(a + \sqrt d)\), so by induction

\[x_n + y_n \sqrt d = \left(a + \sqrt d\right)^n .\]

The number \(d\) is never a perfect square, because \((a-1)^2 < a^2 - 1 < a^2\); Mathlib records that \(d\) is not the square of a natural number.

Every term is a solution, and every solution is a term

For any integer \(d\), if \((x, y)\) and \((u, v)\) solve \(x^2 - dy^2 = 1\) then so does \((xu + dyv,\; xv + yu)\), since in \(\mathbb{Z}[\sqrt d]\) the product of two solutions is a solution. Starting from \((1, 0)\) and multiplying repeatedly by \((a, 1)\) therefore gives solutions only: \(x_n^2 - d y_n^2 = 1\) for every \(n\).

Conversely, every solution in natural numbers is \((x_n, y_n)\) for some \(n\). A sketch: write \(\varepsilon = a + \sqrt d > 1\), and let \(\beta = x + y\sqrt d\) come from a solution with \(x, y \ge 0\), so \(x \ge 1\) and \(\beta \ge 1\). Choose \(n\) with \(\varepsilon^n \le \beta < \varepsilon^{n+1}\). Since \((a + \sqrt d)(a - \sqrt d) = 1\), the number \(\gamma = \beta (a - \sqrt d)^n = u + v\sqrt d\) lies in \(\mathbb{Z}[\sqrt d]\), solves the equation, and satisfies \(1 \le \gamma < \varepsilon\). Its conjugate \(u - v\sqrt d = \gamma^{-1}\) lies in \((0, 1]\), so \(u > 0\) and \(v \ge 0\). If \(v \ge 1\), then \(u^2 = 1 + dv^2 \ge a^2\) gives \(\gamma \ge a + \sqrt d = \varepsilon\), a contradiction; hence \(v = 0\), \(u = 1\), and \(\beta = \varepsilon^n\). Since \(\sqrt d\) is irrational, comparing coordinates gives \((x, y) = (x_n, y_n)\). Allowing signs, the integer solutions are exactly the pairs \((\pm x_n, \pm y_n)\).

Examples
  • For \(a = 2\), \(d = 3\), the sequence begins \((1, 0), (2, 1), (7, 4), (26, 15), (97, 56)\); for instance \(97^2 - 3 \cdot 56^2 = 9409 - 9408 = 1\).
  • For \(a = 3\), \(d = 8\), it begins \((1, 0), (3, 1), (17, 6), (99, 35)\), and \(99^2 - 8 \cdot 35^2 = 9801 - 9800 = 1\).
Properties

The growth, divisibility and congruence properties are what make the sequence useful in logic: they let a system of polynomial equations in natural numbers express that a pair of variables is the \(k\)-th term of the sequence, which is the key step in Matiyasevič's theorem.

Generalizations

For a general positive integer \(d\) that is not a square, Pell's equation still has a solution with \(y \neq 0\), and for every integer \(d\) the integer solutions form an abelian group under the multiplication of \(\mathbb{Z}[\sqrt d]\). When a fundamental solution exists (the solution with \(y > 0\) whose \(x\) is least among all solutions with \(x > 1\)), every solution is, up to sign, an integer power of it. For \(d = a^2 - 1\) the fundamental solution is \((a, 1)\): a solution with \(y \ge 1\) has \(x^2 = 1 + dy^2 \ge a^2\). In general the fundamental solution can be far larger than \(d\), and it is found from the continued fraction expansion of \(\sqrt d\). For positive non-square \(d\), the solution group is an infinite cyclic group times \(\{\pm 1\}\), which parallels the Dirichlet unit theorem for real quadratic fields.

In Mathlib

Mathlib treats the case \(d = a^2 - 1\) separately from general \(d\). The sequence takes as input a natural number \(a\) together with a proof that \(a > 1\), and returns pairs of natural numbers; its coordinates are named separately as the \(x\)-sequence and the \(y\)-sequence, with integer copies and a copy in \(\mathbb{Z}[\sqrt d]\) for algebraic manipulation. Statements in natural numbers use truncated subtraction, where \(m - k\) is \(0\) when \(k > m\). The equation is therefore written as \(x^2 - dy^2 = 1\) in natural numbers, which is still equivalent to \(x^2 = dy^2 + 1\) because the right side is not \(0\); this is the form of the hypothesis in the completeness theorem. The general theory, for every integer \(d\), works with a bundled type of integer solutions carrying its group structure, and shows that for positive \(d\) a solution with \(y \neq 0\) exists exactly when \(d\) is not a square.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPell.pell
Uses 3 · Used by 2
Statement usesNatural number · Integer
Proof usesReal number
Used bySolutions to Pell’s Equation (Freek Wiedijk's 100 theorems) · Matiyasevič's theorem

TheoremMatiyasevič's theorem#

Matiyasevič's theorem, also called the MRDP theorem (after Matiyasevič, Robinson, Davis and Putnam), says that every recursively enumerable set of natural numbers (one whose members some algorithm can list) is Diophantine: it is the set of parameter values for which some polynomial equation with integer coefficients has a solution in natural numbers. Since some recursively enumerable sets cannot be decided by any algorithm, no algorithm can decide whether an arbitrary polynomial equation with integer coefficients has a solution in natural numbers (and hence, by a reduction given below, in integers), which is the negative answer to Hilbert's tenth problem. The decisive number-theoretic step is that exponentiation is Diophantine, and the standard route to it runs through the solutions of Pell's equation \(x^2 - (a^2 - 1)y^2 = 1\). Mathlib formalizes this step, and its theorem under this name is a Diophantine description of those solutions.

Statement

A set \(S\) of \(n\)-tuples of natural numbers is Diophantine if there is a polynomial \(P(x_1, \dots, x_n, y_1, \dots, y_m)\) with integer coefficients such that a tuple \(x\) lies in \(S\) exactly when \(P(x, y) = 0\) for some natural numbers \(y_1, \dots, y_m\). A function is Diophantine when its graph is a Diophantine set. The full theorem says that the Diophantine sets are exactly the recursively enumerable sets, those whose members some algorithm lists. One direction is easy: an algorithm can search through all candidate witnesses \(y\).

The key step concerns Pell's equation. Fix a natural number \(a > 1\) and put \(x_0 = 1\), \(y_0 = 0\) and

\[x_{n+1} = a x_n + (a^2 - 1) y_n, \qquad y_{n+1} = x_n + a y_n,\]

so that \(x_n + y_n \sqrt{a^2 - 1} = (a + \sqrt{a^2 - 1})^n\); this is the recursive definition. Each pair \((x_n, y_n)\) satisfies \(x_n^2 - (a^2 - 1) y_n^2 = 1\), and every solution of \(x^2 - (a^2 - 1)y^2 = 1\) in natural numbers is one of these pairs.

The theorem states that, for natural numbers \(a, k, x, y\), \(a > 1\) with \(x = x_k\) and \(y = y_k\) holds if and only if \(a > 1\), \(k \le y\), and either \(x = 1\) and \(y = 0\), or there are natural numbers \(u, v, s, t, b\) with

\[x^2 - (a^2 - 1) y^2 = 1, \qquad u^2 - (a^2 - 1) v^2 = 1, \qquad s^2 - (b^2 - 1) t^2 = 1,\]
\[b > 1, \qquad v > 0, \qquad y^2 \mid v,\]
\[b \equiv 1 \pmod{4y}, \qquad b \equiv a \pmod{u}, \qquad s \equiv x \pmod{u}, \qquad t \equiv k \pmod{4y}.\]

Each condition is a polynomial equation, an inequality, a divisibility or a congruence, and each of these can be written as a polynomial equation after adding a variable. Since Diophantine sets are closed under intersection, union and existential quantification over some of the variables, it follows that the set of quadruples \((a, k, x, y)\) with \(a > 1\), \(x = x_k\) and \(y = y_k\) is Diophantine.

Examples

For \(a = 2\) the pairs \((x_n, y_n)\) begin \((1, 0), (2, 1), (7, 4), (26, 15), (97, 56)\), and \(97^2 - 3 \cdot 56^2 = 9409 - 9408 = 1\). Continuing, \(y_8 = 10864 = 16 \cdot 679\) is divisible by \(y_2^2 = 16\), an instance of a divisibility used in the proof. For \(a = 3\) the \(y_n\) begin \(0, 1, 6, 35, 204\): here \(y_2 = 6\) divides \(y_4 = 204\), while \(y_3 = 35\) does not.

Proof

The proof rests on properties of the sequences, each proved by induction or from the addition formulas:

Suppose \(x = x_k\) and \(y = y_k\) with \(k > 0\) (the case \(k = 0\) is the alternative \(x = 1\), \(y = 0\)). Put \(m = 2ky\), \(u = x_m\) and \(v = y_m\). Then \(y^2\) divides \(y_{ky}\), which divides \(v\). Here \(k \le y_k = y\), and \(v > 0\) because \(m > 0\). Because \(m\) is even, \(v\) is even, and \(x_m\) is coprime to \(y_m\), so \(u\) is coprime to \(4y\). The Chinese remainder theorem gives \(b\) with \(b \equiv a \pmod u\) and \(b \equiv 1 \pmod{4y}\), and \(b > 1\) because \(a < u\). Take \(s\) and \(t\) to be the \(k\)-th terms of the sequences built from \(b\); all three Pell equations hold because each pair is a term of a Pell sequence. Then \(s \equiv x \pmod u\), and \(t \equiv k \pmod{b - 1}\), hence modulo \(4y\).

Conversely, the three Pell equations make \((x, y) = (x_i, y_i)\) and \((u, v) = (x_n, y_n)\) for \(a\), and \((s, t)\) the \(j\)-th pair for \(b\). The first alternative, \(x = 1\) and \(y = 0\), gives \(k = 0\) directly, since \(k \le y\), and \((1, 0) = (x_0, y_0)\). If \(i = 0\) then \(y = 0\) and \(k = 0\). Otherwise \(v > 0\) and \(y^2 \mid v\) give \(i \le n\) and \(y \mid n\). From \(b \equiv 1 \pmod{4y}\) one gets \(j \equiv t \equiv k \pmod{4y}\), and from \(b \equiv a \pmod u\) one gets \(x_j \equiv s \equiv x_i \pmod{x_n}\), so \(j \equiv \pm i \pmod{4n}\), hence modulo \(4y\). Since \(0 < i \le y\) and \(k \le y\), the sum \(k + i\) lies strictly between \(0\) and \(4y\), which excludes the minus sign, and \(k \equiv i \pmod{4y}\) then forces \(k = i\).

Consequences
In Mathlib

The Pell sequences and the theorem are stated in the natural numbers, while the polynomials that define Diophantine sets take integer values on natural-number arguments. The Pell sequences take a natural number \(a\) together with a proof that \(a > 1\), so the left side of the theorem asserts that such a proof exists along with the two equalities. Subtraction of natural numbers is truncated at zero, but each Pell equation in the statement asks for a difference equal to \(1\), which rules out truncation, so the equations mean what they say; a congruence modulo \(0\) is equality. Diophantine sets are sets of functions from an arbitrary index type to the natural numbers, with witnesses indexed by an arbitrary type as well, defined with Mathlib's own type of integer polynomial functions rather than its general multivariate polynomials. Diophantine functions and partial functions are those with Diophantine graphs, and the partial map sending \((a, k)\) with \(a > 1\) to \(x_k\) is Diophantine. Mathlib stops at exponentiation: it contains neither the theorem that every recursively enumerable set is Diophantine nor the negative solution of Hilbert's tenth problem.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPell.matiyasevic
Uses 6
Statement usesNatural number · Polynomial in several indeterminates · Congruence in \(\Z\) · Solutions to Pell's equation (Number theory)
Proof usesSolutions to Pell’s Equation (Freek Wiedijk's 100 theorems) · Chinese remainder theorem

DefinitionArithmetic functions#

An arithmetic function is a function defined on the positive integers, usually with integer, real or complex values, that records some arithmetic property of its argument: the number of divisors of \(n\), the sum of those divisors, or the count of integers up to \(n\) coprime to \(n\). Arithmetic functions are among the basic objects of elementary and analytic number theory. A product on them, Dirichlet convolution, mirrors the multiplicative structure of the integers, and through Dirichlet series it connects divisor sums with analytic functions such as the Riemann zeta function.

Definition

Let \(R\) be a semiring; for most of this article \(R\) is a commutative ring, often \(\mathbb{Z}\), \(\mathbb{R}\) or \(\mathbb{C}\). An arithmetic function with values in \(R\) is a function \(f\) from the positive integers to \(R\). Mathlib formalizes this as a function from the natural numbers to \(R\) that takes the value \(0\) at \(0\).

Two arithmetic functions are added pointwise. Their Dirichlet convolution is

\[(f * g)(n) = \sum_{ab = n} f(a)\,g(b) = \sum_{d \mid n} f(d)\,g(n/d),\]

the sum of \(f(a)\,g(b)\) over all factorizations \(n = ab\) into positive integers. The neutral element for convolution is the function \(\varepsilon\) with \(\varepsilon(1) = 1\) and \(\varepsilon(n) = 0\) for \(n \neq 1\). With these operations, the arithmetic functions with values in \(R\) form a semiring; when \(R\) is a commutative ring they form a commutative ring, the Dirichlet ring. Over a commutative ring, \(f\) has an inverse under convolution exactly when \(f(1)\) is a unit of \(R\). The inverse \(g\) is computed recursively from \(g(1) = f(1)^{-1}\) and

\[g(n) = -f(1)^{-1} \sum_{d \mid n,\ d < n} f(n/d)\,g(d) \qquad (n > 1),\]

and this function satisfies \(f * g = \varepsilon\).

An arithmetic function \(f\) is multiplicative if \(f(1) = 1\) and \(f(mn) = f(m)\,f(n)\) whenever \(m\) and \(n\) are coprime, that is, whenever their greatest common divisor is \(1\). It is completely multiplicative if \(f(1) = 1\) and \(f(mn) = f(m)\,f(n)\) for all \(m\) and \(n\).

Examples
Properties

Multiplicative functions. A multiplicative function is determined by its values at prime powers: for \(n \ge 1\) with prime factorization \(n = p_1^{k_1} \cdots p_r^{k_r}\), \(f(n) = f(p_1^{k_1}) \cdots f(p_r^{k_r})\). Hence two multiplicative functions are equal exactly when they agree at every prime power. Over a commutative ring, the convolution of two multiplicative functions is multiplicative. This is how one proves that \(\sigma_k\) is multiplicative, and it reduces many identities between multiplicative functions to a check at prime powers.

Möbius inversion. The Möbius function is the convolution inverse of \(\zeta\): \(\mu * \zeta = \varepsilon\) over any ring. Unwinding the convolution, \(\sum_{d \mid n} \mu(d)\) equals \(1\) for \(n = 1\) and \(0\) for \(n > 1\). Convolving with \(\mu\) or with \(\zeta\) therefore undoes the other, which gives the Möbius inversion formula: for functions \(f\) and \(g\) on the positive integers with values in a ring, \(g(n) = \sum_{d \mid n} f(d)\) for every positive \(n\) if and only if \(f(n) = \sum_{ab = n} \mu(a)\,g(b)\) for every positive \(n\). Applied to the totient identity above it gives \(\varphi(n) = \sum_{d \mid n} \mu(d)\, n/d\). Writing \(\log\) also for the arithmetic function \(n \mapsto \log n\), the von Mangoldt identity reads \(\Lambda * \zeta = \log\), and inversion gives \(\Lambda = \mu * \log\).

Dirichlet series. To a complex-valued arithmetic function \(f\) one attaches the Dirichlet series

\[L(f, s) = \sum_{n=1}^{\infty} \frac{f(n)}{n^s}.\]

Convolution becomes multiplication: at every complex \(s\) where both series converge absolutely, \(L(f * g, s) = L(f, s)\,L(g, s)\). The series of \(\zeta\) is the Riemann zeta function, so the identity \(\mu * \zeta = \varepsilon\) says that the series of \(\mu\) is the reciprocal of the zeta function for real part of \(s\) greater than \(1\).

The Dirichlet ring is an analogue of the ring of formal power series: there the coefficients of a product are summed over pairs of indices with a given sum, here over pairs with a given product. By unique factorization, sending \(n = \prod_p p^{k_p}\) to the monomial \(\prod_p x_p^{k_p}\) identifies the Dirichlet ring over a commutative ring \(R\) with a ring of formal power series over \(R\) in countably many variables \(x_p\), one for each prime \(p\). Dirichlet characters are completely multiplicative arithmetic functions, and their Dirichlet series are the Dirichlet \(L\)-functions.

In Mathlib

Mathlib takes the domain to be all natural numbers and forces the value at \(0\) to be \(0\), so that an arithmetic function is a function on the natural numbers rather than on the positive integers; the convolution only ever evaluates its factors at positive integers. The values may lie in any type with a zero, and each operation asks only for the structure it needs: pointwise addition needs an additive monoid, convolution a semiring. Standard functions are defined with their natural codomain, \(\zeta\), \(\sigma_k\), \(\Omega\) and \(\omega\) with natural number values, \(\mu\) with integer values and \(\Lambda\) with real values, and are carried into other rings by coercion, which is why the identity \(\mu * \zeta = \varepsilon\) is proved over the integers first and then over every ring. Being multiplicative is a property of a function rather than a separate structure. Euler's totient function is defined as a plain function on the natural numbers rather than as an arithmetic function, so the identity \(\varphi * \zeta = \mathrm{id}\) appears in Mathlib only as the divisor sum above. Dirichlet series are defined for arbitrary complex sequences, ignoring the term at \(0\), and convolution of sequences is obtained by passing through arithmetic functions.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibArithmeticFunction
Uses 4 · Used by 2
Statement usesNatural number · Prime numbers · Greatest common divisor · Ring
Used byDirichlet’s Theorem · The Perfect Number Theorem

DefinitionBernoulli numbers#

The Bernoulli numbers \(B_0, B_1, B_2, \dots\) are a sequence of rational numbers defined by a power series identity, beginning \(1, -\tfrac12, \tfrac16, 0, -\tfrac1{30}, 0, \tfrac1{42}, \dots\). They appear throughout number theory and analysis: they give closed formulas for sums of powers of consecutive integers, up to explicit factors they are the values of the Riemann zeta function at the negative integers and at the positive even integers, and their denominators and numerators carry arithmetic information about primes.

Definition

The Bernoulli numbers are the coefficients of the exponential generating function

\[\frac{t}{e^t - 1} = \sum_{n=0}^{\infty} B_n \frac{t^n}{n!}.\]

Since \((e^t - 1)/t\) has constant term \(1\), it is invertible as a power series, so this defines every \(B_n\). Equivalently, the series \(\sum_n B_n t^n/n!\) multiplied by \(e^t - 1\) equals \(t\) as formal power series. Comparing coefficients of \(t^n/n!\) on both sides gives a recurrence that determines the Bernoulli numbers \(B_n\) one at a time: for every \(n \ge 0\), the sum \(\sum_{k=0}^{n-1} \binom{n}{k} B_k\) equals \(1\) if \(n = 1\) and \(0\) otherwise. Starting from \(B_0 = 1\), the case \(n = 2\) reads \(B_0 + 2B_1 = 0\), the case \(n = 3\) reads \(B_0 + 3B_1 + 3B_2 = 0\), and so on.

Two conventions

Some authors use instead the numbers \(B_n^+ = (-1)^n B_n\), whose generating function is \(t/(1 - e^{-t}) = t e^t/(e^t - 1)\); the only difference is the sign of the term of index \(1\), since \(B_1^+ = \tfrac12\) while \(B_n^+ = B_n\) for every \(n \ne 1\). The convention \(B_1 = -\tfrac12\) is the one used in this article.

Examples

The first values are \(B_0 = 1\), \(B_1 = -\tfrac12\) and \(B_2 = \tfrac16\). Continuing,

\[B_4 = -\tfrac1{30},\quad B_6 = \tfrac1{42},\quad B_8 = -\tfrac1{30},\quad B_{10} = \tfrac5{66},\quad B_{12} = -\tfrac{691}{2730},\quad B_{14} = \tfrac76.\]
Properties

$\(\sum_{k=0}^{n-1} k^p = \frac{1}{p+1}\sum_{i=0}^{p} \binom{p+1}{i} B_i\, n^{p+1-i}.\)$

For \(p = 2\) this gives \(0^2 + 1^2 + \dots + (n-1)^2 = n^3/3 - n^2/2 + n/6\). With the numbers \(B_i^+\) in place of \(B_i\), the same right-hand side gives the sum \(1^p + 2^p + \dots + n^p\). - Zeta values at even integers. For every integer \(k \ge 1\), the value \(\zeta(2k) = \sum_{m \ge 1} m^{-2k}\) of the Riemann zeta function is a rational multiple of \(\pi^{2k}\) given by

$\(\zeta(2k) = (-1)^{k+1}\frac{2^{2k-1}\pi^{2k} B_{2k}}{(2k)!}.\)$

The case \(k = 1\) is the sum of the reciprocals of the squares, \(\zeta(2) = \pi^2/6\). Since \(\zeta(2k) > 0\), the sign of \(B_{2k}\) is \((-1)^{k+1}\), so \(B_2, B_4, B_6, \dots\) are all nonzero and alternate in sign, and since \(\zeta(2k)\) tends to \(1\), their absolute values grow roughly like \(2\,(2k)!/(2\pi)^{2k}\). - Zeta values at negative integers. For every natural number \(k\), \(\zeta(-k) = (-1)^k B_{k+1}/(k+1)\). For example \(\zeta(0) = -\tfrac12\) and \(\zeta(-1) = -\tfrac1{12}\), while \(\zeta(-2k) = 0\) for \(k \ge 1\) because \(B_{2k+1} = 0\). - Denominators. The von Staudt–Clausen theorem states that for every \(k \ge 1\) the following number is an integer:

$\(B_{2k} + \sum_{p \text{ prime},\ (p-1) \mid 2k} \frac1p.\)$

Consequently, for \(k \ge 1\) and a prime \(p\) with \(p - 1\) dividing \(2k\), \(p\) divides the denominator of \(B_{2k}\) but \(p^2\) does not, and, since \(B_{2k}\) differs from an integer by the sum of the \(1/p\), no other prime divides it. So the denominator of \(B_{2k}\) is the product of the primes \(p\) with \((p - 1) \mid 2k\); in particular it is always divisible by \(6\).

Bernoulli polynomials

The Bernoulli numbers are the constant terms of the Bernoulli polynomials

\[B_n(x) = \sum_{i=0}^{n} \binom{n}{i} B_i\, x^{n-i},\]

a family of polynomials with rational coefficients: \(B_n(0) = B_n\), while \(B_n(1) = B_n^+\). For \(n \ge 1\) and every rational \(x\), \(B_n(x + 1) = B_n(x) + n x^{n-1}\), which turns sums of powers into differences of values of \(B_{p+1}\). The polynomials also give the values at the negative integers of the Hurwitz zeta function \(\zeta(s, x)\), which for \(0 < x \le 1\) is the meromorphic continuation of \(\sum_{m \ge 0} (m + x)^{-s}\): for every integer \(k \ge 1\) and \(0 < x \le 1\), \(\zeta(-k, x) = -B_{k+1}(x)/(k+1)\). Taking \(x = 1\) recovers the values of the Riemann zeta function.

In Mathlib

Mathlib defines the numbers \(B_n^+\) first, by the recursion \(B_n^+ = 1 - \sum_{k=0}^{n-1} \binom{n}{k} B_k^+/(n - k + 1)\), and then sets \(B_n = (-1)^n B_n^+\); both are rational numbers; the unprimed name denotes the numbers \(B_n\) with \(B_1 = -\tfrac12\) used here, and the primed name the numbers \(B_n^+\). The generating function identity is stated for formal power series with coefficients in any commutative algebra over the rationals, and there is a matching identity for \(B_n^+\) with right-hand side \(t e^t\). In the von Staudt–Clausen theorem the sum runs over the primes below \(2k + 2\), which for \(k \ge 1\) is no restriction, and for \(k = 0\) makes the sum empty, so the statement holds for every \(k\) since \(B_0 = 1\). The facts about denominators assume \(k \ge 1\), a prime \(p\) and \((p - 1) \mid 2k\). The zeta values are stated for the Riemann zeta function on the complex numbers, with the even-integer formula assuming \(k \ne 0\). The Hurwitz zeta formula is stated for \(0 \le x \le 1\) and assumes \(k \ne 0\).

Written for Trough, under CC BY-SA 4.0.

Sources
Mathlibbernoulli
Uses 3 · Used by 3
Statement usesRational number · Power series · Exponential
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Sum of kth powers · Von Staudt–Clausen theorem

TheoremChevalley-Warning theorem (Number theory)#

The Chevalley–Warning theorem says that a polynomial equation over a finite field whose degree is smaller than its number of variables has a number of solutions divisible by the characteristic of the field. It turns a bound on degrees into a congruence on a count, and so yields existence results directly: if such an equation has one obvious solution, the count cannot be \(1\), so it has another. This is the standard route to the fact that every quadratic form in three or more variables over a finite field has a nontrivial zero, and to the Erdős–Ginzburg–Ziv theorem of additive combinatorics.

Statement

Let \(K\) be a finite field with \(q\) elements and characteristic \(p\); then \(p\) is prime and \(q\) is a power of \(p\). Let \(f\) be a polynomial in \(n\) variables \(x_1, \dots, x_n\) with coefficients in \(K\), and let \(d\) be its total degree, the largest degree of a monomial occurring in \(f\). If \(d < n\), then \(p\) divides the number of points \(x \in K^n\) with \(f(x) = 0\).

The same conclusion holds for several polynomials at once. If \(f_1, \dots, f_r\) have total degrees \(d_1, \dots, d_r\) with

\[d_1 + d_2 + \cdots + d_r < n,\]

then \(p\) divides the number of common zeros of \(f_1, \dots, f_r\) in \(K^n\) (see the version for a family of polynomials). The single-polynomial statement is the case \(r = 1\).

Examples
  • A sum of three squares. Over the field with \(3\) elements, the equation \(x^2 + y^2 + z^2 = 0\) has degree \(2 < 3\). Each square is \(0\) or \(1\), so a solution has either all coordinates zero (\(1\) point) or all coordinates nonzero (\(2^3 = 8\) points), for \(9\) solutions in total, a multiple of \(3\).
  • Nontrivial zeros. If \(f\) has no constant term and degree less than \(n\), then \(f(0, \dots, 0) = 0\), so the number of zeros is a positive multiple of \(p\), hence at least \(p \ge 2\), and \(f\) has a zero other than the origin. In particular every quadratic form in at least three variables over a finite field has a nontrivial zero.
  • The degree bound is sharp. For \(n \ge 1\) the product \(x_1 x_2 \cdots x_n\) has degree exactly \(n\). Its zeros are the points with some coordinate zero, so there are \(q^n - (q-1)^n\) of them, which is congruent to \(\pm 1\) modulo \(p\) because \(q \equiv 0 \pmod p\). So the hypothesis \(d < n\) cannot be weakened to \(d \le n\): the conclusion can fail when \(d = n\).
Proof

The argument works with values in \(K\) and compares them with the count at the end.

An indicator polynomial. For every nonzero \(a \in K\), \(a^{q-1} = 1\), the finite-field form of Fermat's little theorem. So \(1 - a^{q-1}\) equals \(1\) when \(a = 0\) and \(0\) otherwise. Hence the polynomial

\[F = \prod_{i=1}^{r} \bigl(1 - f_i^{\,q-1}\bigr)\]

takes the value \(1\) at common zeros of the \(f_i\) and \(0\) elsewhere, and the sum of \(F(x)\) over all \(x \in K^n\) is the number \(N\) of common zeros, read as an element of \(K\).

Power sums vanish. For \(0 \le k < q - 1\), the sum of \(a^k\) over all \(a \in K\) is \(0\) (with \(0^0 = 1\), the case \(k = 0\) is the sum of \(q\) ones). A monomial \(x_1^{e_1} \cdots x_n^{e_n}\) of total degree less than \((q-1)n\) has some exponent \(e_j < q - 1\), and summing over the coordinate \(x_j\) first makes its total sum vanish. Therefore every polynomial of total degree less than \((q-1)n\) sums to \(0\) over \(K^n\).

Conclusion. The total degree of \(F\) is at most \((q-1)(d_1 + \cdots + d_r)\), which is less than \((q-1)n\). So \(N = 0\) in \(K\), and since a natural number maps to \(0\) in a ring of characteristic \(p\) exactly when \(p\) divides it, \(p\) divides \(N\).

Consequences and generalizations
  • Erdős–Ginzburg–Ziv theorem. For every positive integer \(m\), any \(2m - 1\) integers, repetitions allowed, include \(m\) whose sum is divisible by \(m\). For \(m = p\) prime, given integers \(a_1, \dots, a_{2p-1}\), the proof applies the theorem for two polynomials to \(\sum_i x_i^{p-1} = 0\) and \(\sum_i a_i x_i^{p-1} = 0\) (coefficients read modulo \(p\)) in \(2p - 1\) variables over the field with \(p\) elements; the general case follows by induction on the prime factors of \(m\).
  • Lower bound. Warning's second theorem adds that if the \(f_i\) have at least one common zero and \(d_1 + \cdots + d_r < n\), then they have at least \(q^{\,n - (d_1 + \cdots + d_r)}\) common zeros.
  • Higher divisibility. The Ax–Katz theorem sharpens the congruence: for polynomials of positive degree, the number of common zeros is divisible by \(q^{\mu}\), where \(\mu\) is the least integer that is at least \((n - d_1 - \cdots - d_r)/\max_i d_i\). Under the Chevalley–Warning hypothesis \(\mu \ge 1\), so even \(q\) divides the count.
In Mathlib

Mathlib indexes the variables by an arbitrary finite type rather than by \(1, \dots, n\), so \(n\) is the number of elements of that type and points are functions from it to \(K\). The characteristic enters as any natural number \(p\) for which \(K\) has characteristic \(p\); for a finite field this forces \(p\) to be prime, so the statement is the classical one. The total degree of the zero polynomial is \(0\), where many texts leave it undefined or set it to \(-\infty\); this is harmless: when \(f = 0\) and \(n \ge 1\) every one of the \(q^n\) points is a zero, and \(p\) divides \(q^n\). Besides the single-polynomial form, Mathlib proves the theorem for a family of polynomials indexed by a finite set, for a family indexed by a finite type, and for a pair of polynomials, the form its proof of the Erdős–Ginzburg–Ziv theorem uses.

Written for Trough, under CC BY-SA 4.0.

Sources
Mathlibchar_dvd_card_solutions
Uses 4
Statement usesFinite fields · Characteristic p · Polynomial in several indeterminates
Proof usesFermat's little theorem

TheoremHensel's lemma (for \(\mathbb{Z}_p\))#

Hensel's lemma for the \(p\)-adic integers \(\mathbb{Z}_p\) says that an approximate root of a polynomial can be refined to an exact root, provided the approximation is good compared with the size of the derivative at that point. In its most used form it says that a root modulo a prime \(p\) at which the derivative is nonzero modulo \(p\) lifts to a unique root in \(\mathbb{Z}_p\) congruent to it modulo \(p\), and so to a root modulo every power of \(p\). It is the basic tool for deciding which polynomial equations have \(p\)-adic solutions, and the model for the notion of a Henselian ring.

Statement

Let \(p\) be a prime, let \(|\cdot|\) be the \(p\)-adic norm on \(\mathbb{Z}_p\), normalized so that \(|p| = 1/p\), and let \(F\) be a polynomial with coefficients in \(\mathbb{Z}_p\), with derivative \(F'\). Suppose \(a \in \mathbb{Z}_p\) satisfies

\[|F(a)| < |F'(a)|^2.\]

Then there is a \(z \in \mathbb{Z}_p\) with \(F(z) = 0\), \(|z - a| < |F'(a)|\) and \(|F'(z)| = |F'(a)|\), and \(z\) is the only root of \(F\) with \(|z - a| < |F'(a)|\). The hypothesis forces \(F'(a) \neq 0\). A sharper bound also holds: \(|z - a| = |F(a)|/|F'(a)|\).

Simple roots modulo \(p\). Every \(p\)-adic integer has norm at most \(1\), and an element of \(\mathbb{Z}_p\) has norm less than \(1\) exactly when it is divisible by \(p\). So if \(F(a) \equiv 0 \pmod p\) and \(F'(a) \not\equiv 0 \pmod p\), then \(|F(a)| < 1 = |F'(a)|^2\), and the theorem gives a unique root \(z\) of \(F\) with \(z \equiv a \pmod p\). When \(F\) has integer coefficients, reducing \(z\) modulo \(p^k\) gives a solution of \(F(x) \equiv 0 \pmod{p^k}\) for every \(k \ge 1\), all congruent to \(a\) modulo \(p\).

Examples
  • Square roots for odd \(p\). Let \(p\) be odd and \(u \in \mathbb{Z}_p\) not divisible by \(p\) that is a square modulo \(p\), say \(a^2 \equiv u \pmod p\) with \(a \in \mathbb{Z}\). For \(F = X^2 - u\) the derivative \(F'(a) = 2a\) is not divisible by \(p\), so \(u\) has a square root in \(\mathbb{Z}_p\) congruent to \(a\). For instance \(3^2 \equiv 2 \pmod 7\), so \(2\) is a square in \(\mathbb{Z}_7\). Hence for odd \(p\) a unit of \(\mathbb{Z}_p\) is a square exactly when it is a square modulo \(p\).
  • Square roots in \(\mathbb{Z}_2\). For \(p = 2\) the derivative \(2X\) is always divisible by \(2\), so the simple-root form never applies, but the general form does. If \(u \equiv 1 \pmod 8\) and \(a = 1\), then \(|F(1)| = |1 - u| \le 1/8 < 1/4 = |2|^2\), so \(u\) has a square root \(z\) in \(\mathbb{Z}_2\) with \(z \equiv 1 \pmod 4\).
  • Roots of unity. Take \(F = X^{p-1} - 1\) and \(a \in \{1, \dots, p-1\}\). By Fermat's little theorem \(F(a) \equiv 0 \pmod p\), while \(F'(a) = (p-1)a^{p-2}\) is not divisible by \(p\). Each \(a\) therefore lifts to a root of \(F\), and the \(p - 1\) lifts lie in different residue classes. So \(\mathbb{Z}_p\) contains \(p - 1\) distinct \((p-1)\)-th roots of unity, one in each nonzero residue class modulo \(p\).
  • A failure. The polynomial \(X^2 - 3\) has the root \(1\) modulo \(2\), but \(3\) is not a square in \(\mathbb{Z}_2\), since the square of a unit of \(\mathbb{Z}_2\) is congruent to \(1\) modulo \(8\). The hypothesis fails at every \(a\): for odd \(a\) one has \(|a^2 - 3| = 1/2\), which is not less than \(|2a|^2 = 1/4\), and for even \(a\) one has \(|a^2 - 3| = 1\).
Proof

The proof is Newton's method in the \(p\)-adic metric. Put \(a_0 = a\) and \(t = |F(a)|/|F'(a)|^2 < 1\), and define

\[a_{n+1} = a_n - \frac{F(a_n)}{F'(a_n)}.\]

Expanding \(F\) around \(x\) gives \(F(x + h) = F(x) + F'(x)h + h^2 G(x, h)\), where \(G\) is a polynomial with coefficients in \(\mathbb{Z}_p\), so \(|G(x, h)| \le 1\) for \(x, h \in \mathbb{Z}_p\). Likewise \(|F'(x) - F'(y)| \le |x - y|\), an instance of the fact that a polynomial over \(\mathbb{Z}_p\) does not increase \(p\)-adic distances. By induction on \(n\) one shows that \(a_n \in \mathbb{Z}_p\), that \(|F'(a_n)| = |F'(a)|\), and that \(|F(a_n)| \le |F'(a)|^2 t^{2^n}\): the step \(h = -F(a_n)/F'(a_n)\) kills the linear term, leaving \(|F(a_{n+1})| \le |h|^2\), and the derivative keeps its norm because it moves by less than its own size, by the ultrametric inequality \(|x + y| \le \max(|x|, |y|)\), which gives \(|x + y| = |x|\) whenever \(|y| < |x|\).

The steps satisfy \(|a_{n+1} - a_n| \le |F'(a)|\, t^{2^n}\), which tends to \(0\). In an ultrametric space this makes \((a_n)\) a Cauchy sequence, and since \(\mathbb{Z}_p\) is complete it converges to some \(z\). By continuity \(F(z) = 0\) and \(|F'(z)| = |F'(a)|\), and the ultrametric inequality bounds \(|z - a|\) by the first step \(|F(a)|/|F'(a)|\), which is less than \(|F'(a)|\).

For uniqueness, let \(z'\) be another root with \(|z' - a| < |F'(a)|\) and put \(h = z' - z\), so that \(|h| < |F'(a)| = |F'(z)|\). Then \(0 = F(z + h) = h\,(F'(z) + h\,G(z, h))\), and the second factor is nonzero because \(|h\,G(z, h)| \le |h| < |F'(z)|\). Hence \(h = 0\).

Generalizations

The same argument works over the valuation ring \(\{x : |x| \le 1\}\) of any field complete for a nonarchimedean absolute value. Abstracting the simple-root form leads to Henselian rings. A commutative ring \(R\) is Henselian at an ideal \(I\) if \(I\) is contained in the Jacobson radical of \(R\) and, for every monic polynomial \(f\) over \(R\) and every \(a_0 \in R\) with \(f(a_0) \in I\) and \(f'(a_0)\) invertible modulo \(I\), there is a root \(a\) of \(f\) with \(a - a_0 \in I\). A local ring is a Henselian local ring when this holds for its maximal ideal. Every ring that is complete and Hausdorff for the \(I\)-adic topology is Henselian at \(I\); in particular \(\mathbb{Z}_p\), complete for the \(p\mathbb{Z}_p\)-adic topology, is a Henselian local ring. Stronger versions of the lemma lift factorizations of monic polynomials into coprime factors, not just simple roots, from the residue field to the ring.

In Mathlib

Mathlib proves the lemma in the general form above, with all four conclusions (existence, distance to \(a\), norm of the derivative, uniqueness) packaged in one statement, which needs no separate case for \(F(a) = 0\) (the root is then \(a\) itself). The polynomial may have coefficients in any commutative semiring that maps into \(\mathbb{Z}_p\) as an algebra, such as the integers or \(\mathbb{Z}_p\) itself, and it is evaluated at \(p\)-adic integers through that map. The norm is the \(p\)-adic norm with \(|p| = 1/p\). The published statement records only the strict bound \(|z - a| < |F'(a)|\), not the sharper equality. Separately, Mathlib's theory of Henselian rings states its conditions for monic polynomials, and records that fields are Henselian local rings and that adically complete rings are Henselian, which covers \(\mathbb{Z}_p\) as well.

Written for Trough, under CC BY-SA 4.0.

Sources
Mathlibhensels_lemma
Uses 7
Statement uses\(p\)-adic integer · Polynomial in one indeterminate · Polynomial derivative · Prime numbers
Proof usesCauchy sequence · Completeness · Continuous function

StructureRing of Witt vectors#

For a prime number \(p\) and a commutative ring \(R\), the ring of (\(p\)-typical) Witt vectors \(W(R)\) is a ring whose elements are infinite sequences \((a_0, a_1, a_2, \dots)\) of elements of \(R\), added and multiplied by universal polynomial rules that imitate carrying digits. Its basic use is to produce rings of characteristic zero out of rings of characteristic \(p\): applied to the field with \(p\) elements it gives the \(p\)-adic integers, and applied to any perfect field \(k\) of characteristic \(p\) it gives a complete discrete valuation ring with residue field \(k\) in which \(p\) generates the maximal ideal. Witt vectors are a standard tool in number theory, algebraic geometry in characteristic \(p\), and \(p\)-adic Hodge theory.

Definition

Fix a prime \(p\). The \(n\)-th Witt polynomial is the polynomial with integer coefficients

\[w_n = \sum_{i=0}^{n} p^i X_i^{p^{n-i}} = X_0^{p^n} + p X_1^{p^{n-1}} + \cdots + p^n X_n\]

in the variables \(X_0, X_1, \dots\) (the definition); for instance \(w_0 = X_0\) and \(w_1 = X_0^p + p X_1\). For a sequence \(a = (a_0, a_1, \dots)\) in \(R\), the elements \(w_n(a)\) of \(R\), obtained by evaluating \(w_n\) at \(a\) with its integer coefficients read in \(R\), are its ghost components.

The key fact is the Witt structure theorem: for every polynomial \(\Phi\) with integer coefficients there is a unique family of polynomials \(\varphi_0, \varphi_1, \dots\) with integer coefficients such that \(w_n(\varphi_0, \varphi_1, \dots) = \Phi(w_n, w_n, \dots)\) for every \(n\), where the copies of \(w_n\) on the right are taken in separate sets of variables. Taking \(\Phi = X + Y\) and \(\Phi = XY\) gives polynomials \(S_n\) and \(P_n\), each involving only the first \(n + 1\) coordinates of each argument, and one defines

\[a + b = (S_0(a, b), S_1(a, b), \dots), \qquad a \cdot b = (P_0(a, b), P_1(a, b), \dots).\]

So the zeroth coordinate of a sum is the sum of zeroth coordinates and likewise for products, but the higher coordinates involve carries:

\[S_1 = X_1 + Y_1 + \frac{X_0^p + Y_0^p - (X_0 + Y_0)^p}{p}, \qquad P_1 = X_0^p Y_1 + X_1 Y_0^p + p X_1 Y_1.\]

With these operations the set of sequences becomes a commutative ring, the ring of Witt vectors \(W(R)\), and by construction the ghost map \(a \mapsto (w_0(a), w_1(a), \dots)\) is a ring homomorphism from \(W(R)\) to the product ring \(R^{\mathbb{N}}\). The ring axioms are polynomial identities with integer coefficients; they can be checked after inverting \(p\), where the ghost map identifies Witt vectors with ordinary sequences under coordinatewise operations.

Examples
Properties

Functoriality. A ring homomorphism \(f\colon R \to S\) induces a ring homomorphism \(W(R) \to W(S)\) that applies \(f\) to every coordinate, and it is injective when \(f\) is.

Teichmüller representatives. The map \(r \mapsto [r] = (r, 0, 0, \dots)\) is multiplicative and sends \(1\) to \(1\), though not additive, and the ghost components of \([r]\) are \(r, r^p, r^{p^2}, \dots\).

Frobenius and Verschiebung. Each \(W(R)\) carries a ring endomorphism \(F\), the Witt vector Frobenius, and an additive map \(V\), the Verschiebung, which shifts coordinates and inserts a zero: \(V(a_0, a_1, \dots) = (0, a_0, a_1, \dots)\). They satisfy \(F(V(x)) = px\) and the projection formula \(V(x \cdot F(y)) = V(x) \cdot y\). When \(R\) has characteristic \(p\), \(F\) raises every coordinate to the \(p\)-th power, so it is induced by the Frobenius morphism of \(R\), and \(V(F(x)) = px\) as well. In particular, in characteristic \(p\), the element \(p\) of \(W(R)\) is \((0, 1, 0, 0, \dots)\).

Characteristic zero. If \(R\) has characteristic \(p\), then the \(n\)-th coordinate of \(p^n\) is \(1\), so \(p\) is not nilpotent in \(W(R)\). In fact \(W(R)\) has characteristic zero, since the inclusion of \(\mathbb{F}_p\) into \(R\) induces an injective ring homomorphism from \(W(\mathbb{F}_p) \cong \mathbb{Z}_p\) into \(W(R)\) (the inclusion is injective because \(R \neq 0\), and functoriality preserves injectivity). If \(R\) is moreover an integral domain, so is \(W(R)\).

Perfect fields. A ring of characteristic \(p\) is perfect if its Frobenius map \(x \mapsto x^p\) is bijective, so that every element \(x\) has a unique \(p^i\)-th root, written \(x^{p^{-i}}\), for each \(i\). Let \(k\) be a perfect field of characteristic \(p\). Then \(W(k)\) is a discrete valuation ring, that is, a principal ideal domain with exactly one nonzero prime ideal, and \(p\) is an irreducible element of it, hence a uniformizer (a generator of that maximal ideal); every nonzero element has the form \(p^m u\) with \(u\) a unit. More generally, for a perfect ring \(k\) of characteristic \(p\), the quotient \(W(k)/pW(k)\) is isomorphic to \(k\), \(W(k)\) is complete for the \(p\)-adic topology, and every Witt vector \(x = (x_0, x_1, \dots)\) has a Teichmüller expansion: for each \(n\), \(x\) is congruent modulo \(p^{n+1}\) to \(\sum_{i=0}^{n} [x_i^{p^{-i}}]\, p^i\). For \(k = \mathbb{F}_p\) this writes every \(p\)-adic integer as a series \(\sum_i \tau_i\, p^i\) whose digits \(\tau_i\) are Teichmüller representatives, that is, \(0\) or a \((p-1)\)-st root of unity, instead of the integers \(0, 1, \dots, p - 1\).

The perfection of a ring of characteristic \(p\) is often combined with Witt vectors, since \(W\) behaves best on perfect rings. The ring \(W(k)\) for a perfect field \(k\) is, up to isomorphism, the only complete discrete valuation ring of characteristic zero in which \(p\) generates the maximal ideal and whose residue field is \(k\); its fraction field carries the Frobenius semilinear structure used to define isocrystals. There is also a ring of big Witt vectors, indexed by all positive integers rather than by powers of \(p\), of which the \(p\)-typical ring is a quotient.

In Mathlib

Mathlib defines Witt vectors for any natural number \(p\) and any type \(R\) as a structure wrapping a sequence indexed by the natural numbers, whose terms it calls coefficients rather than coordinates. The ring structure is provided only when \(p\) is known to be prime and \(R\) is a commutative ring. Addition, multiplication and the other operations are defined by evaluating the integral structure polynomials on the coefficients, and the ring axioms are proved first for Witt vectors over polynomial rings with rational coefficients, where the ghost map is bijective, then carried to polynomial rings with integer coefficients, whose Witt vectors map injectively into the rational case, and finally transferred to an arbitrary commutative ring \(R\) along the surjective map onto \(W(R)\) induced by evaluating such polynomials at elements of \(R\). Truncated Witt vectors of a fixed length are a separate type with its own ring structure.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibWittVector
Uses 4
Statement usesRing · Prime numbers · Polynomial in several indeterminates · Ring morphism

DefinitionPerfection of a ring#

The perfection of a commutative ring \(R\) of prime characteristic \(p\) is the ring of sequences \((x_0, x_1, x_2, \dots)\) of elements of \(R\) in which each term is a \(p\)-th root of the one before it. On this ring the Frobenius map \(x \mapsto x^p\) is bijective, and it is the universal perfect commutative ring of characteristic \(p\) mapping to \(R\): every homomorphism to \(R\) from a perfect commutative ring of characteristic \(p\) passes through it in exactly one way. The construction is basic in \(p\)-adic geometry, where the perfection of a quotient \(\mathcal{O}/p\mathcal{O}\) produces the ring whose field of fractions is the tilt of a valued field.

Definition

Let \(p\) be a prime and \(R\) a commutative ring of characteristic \(p\). The perfection of \(R\) is

\[R^{\mathrm{perf}} = \{ (x_n)_{n \ge 0} : x_n \in R \text{ and } x_{n+1}^p = x_n \text{ for all } n \}.\]

A sequence satisfying this condition is called compatible. Because Frobenius is a ring homomorphism in characteristic \(p\), these sequences are closed under termwise addition, multiplication and negation, and they form a subring of the ring of all sequences in \(R\). Equivalently, \(R^{\mathrm{perf}}\) is the inverse limit of the tower

\[\cdots \xrightarrow{\ \varphi\ } R \xrightarrow{\ \varphi\ } R \xrightarrow{\ \varphi\ } R\]

in which every map is the Frobenius \(\varphi(x) = x^p\).

For each \(n\), the \(n\)-th coordinate \((x_m) \mapsto x_n\) is a ring homomorphism from \(R^{\mathrm{perf}}\) to \(R\), and an element of \(R^{\mathrm{perf}}\) is determined by its coordinates. Write \(\pi \colon R^{\mathrm{perf}} \to R\) for the zeroth coordinate.

A ring of characteristic \(p\) is perfect when its Frobenius map is bijective. The perfection is perfect. Frobenius sends \((x_0, x_1, x_2, \dots)\) to \((x_0^p, x_0, x_1, \dots)\), and the shift \((x_0, x_1, x_2, \dots) \mapsto (x_1, x_2, \dots)\) undoes it: the shift after Frobenius is the identity, and so is Frobenius after the shift.

Universal property

Let \(P\) be a perfect commutative ring of characteristic \(p\). Then composing with \(\pi\) gives a bijection from ring homomorphisms \(P \to R^{\mathrm{perf}}\) to ring homomorphisms \(P \to R\). The inverse sends \(f \colon P \to R\) to the map

\[y \mapsto \bigl( f(y), f(y^{1/p}), f(y^{1/p^2}), \dots \bigr),\]

where \(y^{1/p^n}\) is the unique \(p^n\)-th root of \(y\) in \(P\). In particular, two homomorphisms \(P \to R^{\mathrm{perf}}\) that agree after composing with \(\pi\) are equal.

The construction is functorial: a ring homomorphism \(g \colon R \to S\) between rings of characteristic \(p\) induces a ring homomorphism \(R^{\mathrm{perf}} \to S^{\mathrm{perf}}\), which applies \(g\) to each coordinate. In categorical language, perfection is right adjoint to the inclusion of perfect rings of characteristic \(p\) into commutative rings of characteristic \(p\).

Examples
  • Perfect rings. If \(R\) is already perfect, then \(R\), with the identity map, is its own perfection: in a compatible sequence, \(x_n\) must be the unique \(p^n\)-th root of \(x_0\). This applies to finite fields and to algebraically closed fields of characteristic \(p\).
  • A polynomial ring. Let \(R = \mathbb{F}_p[t]\) be the polynomial ring. Let \((x_n)\) be a compatible sequence. If \(x_0 = 0\), then every \(x_n\) is \(0\), because \(\mathbb{F}_p[t]\) has no nonzero nilpotent elements. If \(x_0 \neq 0\), then \(x_0 = x_n^{p^n}\) has degree divisible by \(p^n\) for every \(n\), so \(x_0\) and then every \(x_n\) is constant. Frobenius fixes every element of \(\mathbb{F}_p\), so the sequence is constant, and \(\mathbb{F}_p[t]^{\mathrm{perf}} \cong \mathbb{F}_p\). The perfection keeps only what already has all \(p\)-power roots.
  • Nilpotents disappear. A perfect ring has no nonzero nilpotent elements, since Frobenius is injective. For \(R = \mathbb{F}_p[t]/(t^2)\), Frobenius sends \(a + bt\) to \(a^p = a\), so every term \(x_n = x_{n+1}^p\) lies in \(\mathbb{F}_p\), the sequence is constant, and \(R^{\mathrm{perf}} \cong \mathbb{F}_p\).
  • Surjective Frobenius. When Frobenius on \(R\) is surjective, every coordinate map \(R^{\mathrm{perf}} \to R\) is surjective, and the perfection can be large. Let \(A = \mathbb{F}_p[t^{1/p^\infty}]\) be the perfect ring obtained from \(\mathbb{F}_p[t]\) by adjoining all \(p\)-power roots of \(t\), and let \(R = A/tA\). Frobenius on \(R\) is surjective but not injective, since it kills the class of \(t^{1/p}\). The isomorphisms \(A/t^{p^n}A \cong A/tA\) given by taking \(p^n\)-th roots identify the Frobenius tower of \(R\) with the tower of quotients \(A/t^{p^n}A\), so \(R^{\mathrm{perf}}\) is the \(t\)-adic completion of \(A\).
Tilting

Let \(K\) be a field with a nonarchimedean absolute value \(v \colon K \to \mathbb{R}_{\ge 0}\), let \(\mathcal{O} = \{ x \in K : v(x) \le 1 \}\) be its valuation ring, and let \(p\) be a prime with \(v(p) < 1\). Then the quotient ring \(\mathcal{O}/p\mathcal{O}\) has characteristic \(p\), and its perfection is the pre-tilt \(\mathcal{O}^\flat\). Under these hypotheses \(\mathcal{O}^\flat\) is an integral domain, and the tilt \(K^\flat\) is its field of fractions (see field of fractions), a field of characteristic \(p\). For the completion \(\mathbb{C}_p\) of an algebraic closure of the \(p\)-adic numbers, the tilt carries an absolute value induced from \(v\), for which it is a complete algebraically closed field of characteristic \(p\). This passage from mixed characteristic to characteristic \(p\) is the starting point of the theory of perfectoid fields.

When \(\mathcal{O}\) is \(p\)-adically complete, reduction modulo \(p\) gives a bijection, compatible with multiplication, from sequences \((y_n)\) in \(\mathcal{O}\) with \(y_{n+1}^p = y_n\) to elements of \(\mathcal{O}^\flat\). This is how elements of the tilt are compared with elements of \(\mathcal{O}\) itself.

  • The perfect closure is the dual construction: the direct limit of \(R \xrightarrow{\varphi} R \xrightarrow{\varphi} \cdots\), which adjoins \(p\)-th roots instead of selecting them. It is the universal homomorphism from \(R\) to a perfect ring, the left adjoint of the same inclusion.
  • The multiplicative part of the definition needs neither addition nor a characteristic: for any commutative monoid \(M\) and any natural number \(p\), the sequences with \(x_{n+1}^p = x_n\) form a submonoid of the monoid of all sequences in \(M\).
  • The ring of Witt vectors of a perfect ring of characteristic \(p\), such as \(W(\mathcal{O}^\flat)\), leads back from characteristic \(p\) to mixed characteristic.
In Mathlib

Mathlib defines the perfection for any type with natural-number powers and any natural number \(p\), as the sequences with \(x_{n+1}^p = x_n\). For a commutative monoid this is a commutative monoid on which the \(p\)-th power map is bijective; the ring structure and characteristic \(p\) arrive when \(p\) is prime and the input is a commutative semiring of characteristic \(p\), so semirings are allowed throughout. Mathlib's notion of a perfect ring asks only that \(x \mapsto x^p\) be bijective, without a characteristic hypothesis. The universal property is an explicit bijection between sets of homomorphisms. A separate predicate says when a homomorphism \(P \to R\) from a perfect ring is a perfection map: every compatible sequence of \(p\)-power roots in \(R\) arises from exactly one \(y\) in \(P\) as the images of \(y, y^{1/p}, y^{1/p^2}, \dots\). Such a map yields an isomorphism from \(P\) to \(R^{\mathrm{perf}}\), and the zeroth coordinate \(R^{\mathrm{perf}} \to R\) is itself a perfection map. The tilt is defined for any field with a valuation valued in the nonnegative reals and any prime \(p\) with \(v(p) \neq 1\), with no completeness or perfectoid hypothesis; the ring \(\mathcal{O}\) may be any ring mapping isomorphically onto the valuation ring.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPerfection
Uses 4
Statement usesRing · Characteristic p · Frobenius morphism · Ring morphism

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.