Field theory

ClassField#

A field is a set with an addition and a multiplication in which the usual rules of arithmetic hold and division by any nonzero element is possible. The rational, real and complex numbers are the familiar examples. Fields are where linear algebra takes place, since a vector space is a module over a field, and they are the setting for the theory of polynomial equations, from splitting fields to the Galois correspondence.

Definition

A field is a commutative ring \(K\) with identity in which \(1 \neq 0\) and every nonzero element \(a\) has a multiplicative inverse, an element \(a^{-1}\) with

\[a\,a^{-1} = a^{-1}a = 1.\]

The condition \(1 \neq 0\) excludes the zero ring, in which every nonzero element trivially has an inverse because there are none. Spelled out, \(K\) is an abelian group under addition with identity \(0\); the nonzero elements form an abelian group under multiplication with identity \(1\); and multiplication distributes over addition. The inverse of a nonzero element is unique, and division is defined by \(a / b = a\,b^{-1}\) for \(b \neq 0\).

Examples
Properties
Generalizations

Dropping commutativity of multiplication gives a division ring, also called a skew field; the quaternions are the standard example of one that is not a field. No finite example exists: Wedderburn's little theorem says that every finite division ring is a field. Dropping additive inverses instead gives a semifield, such as the nonnegative rational numbers.

In Mathlib

Mathlib defines a field as a commutative ring that is also a division ring, and the condition \(1 \neq 0\) is part of the definition. Inversion is a function on all of \(K\), so it must take a value at \(0\): by convention the inverse of \(0\) is \(0\), and consequently \(a / 0 = 0\) for every \(a\). The usual identity \(a\,a^{-1} = 1\) holds for every \(a \neq 0\). This convention makes division total without changing any statement about nonzero denominators. A field structure also carries a chosen map from the rationals into the field, which lets Mathlib control how \(\mathbb{Q}\) acts on it. Because these are data, Mathlib also has a property of a ring saying that it is a field, which makes no choice of inverse; every field has this property, and a ring with it can be given a field structure. Several of the facts above are proved in greater generality: the statement about ideals for every division semiring, the injectivity of homomorphisms for every simple ring, the embedding of a ring in its ring of fractions for every commutative ring, the dichotomy for the characteristic for every nonzero ring without zero divisors, and the bound on roots for every integral domain.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibField
Uses 2 · Used by 41
Statement usesGroup · Ring
Used byThe Solution of a Cubic · The Solution of the General Quartic Equation · Wilson’s Lemma · The Factor and Remainder Theorems · The Friendship Theorem · Carathéodory's theorem · Jensen's inequality (finite sum version) · Dirichlet unit theorem · Abel-Ruffini theorem (one direction) · Algebraic extension · Algebraically closed field · Existence of algebraic closure of a field · Field of fractions of an integral domain · Perfect closure · Rupture field · Splitting field · Subfield · Quadratic reciprocity · Complex number · Continued fraction · Hyper-real number · \(p\)-adic number · Real number · \(K[X]\) is Euclidean · Character · Representation · Chevalley–Warning theorem (1000+ theorems) · Wedderburn's little theorem · Birkhoff–Von Neumann theorem · Lie's theorem · Weierstrass preparation theorem · Helly's theorem · Radon's theorem · Fermat's little theorem · Adjoint endomorphism · Sylvester's law of inertia (uniqueness) · Maschke theorem · Gaussian elimination · Lagrange interpolation · Field \(\Q\) of rational numbers · Rational functions

StructureSubfield#

A subfield of a field \(K\) is a subset of \(K\) that contains \(0\) and \(1\) and is closed under addition, negation, multiplication and taking inverses of nonzero elements, so that it is itself a field under the operations of \(K\). Subfields are central to field theory: a field extension \(L/K\) can be viewed as a field \(L\) together with a subfield isomorphic to \(K\), and for a finite Galois extension the Galois correspondence describes the fields lying in between by means of subgroups of the Galois group.

Definition

Let \(K\) be a field. A subset \(F \subseteq K\) is a subfield if

  • \(F\) is a subring of \(K\): it contains \(0\) and \(1\) and is closed under \(+\), \(-\) and \(\times\);
  • \(F\) is closed under inverses: if \(x \in F\) and \(x \neq 0\), then \(x^{-1} \in F\).

Thus a subring that contains the inverse of each of its nonzero elements determines a subfield with the same elements. With the addition and multiplication of \(K\) restricted to it, a subfield is a field in its own right, and the inclusion \(F \hookrightarrow K\) is a ring homomorphism. If \(F\) is a subfield of \(K\), one also says that \(K\) is an extension field of \(F\).

The same definition makes sense in a division ring (a ring with \(1 \neq 0\) in which every nonzero element is invertible, but multiplication need not commute), and there a subfield is again a division ring. Such a subset is usually called a sub-division ring; Mathlib still calls it a subfield.

Examples
  • The rational numbers form a subfield of the real numbers, which form a subfield of the complex numbers.
  • The set \(\mathbb{Q}(\sqrt 2) = \{a + b\sqrt 2 : a, b \in \mathbb{Q}\}\) is a subfield of \(\mathbb{R}\). It is a subring, since \((a + b\sqrt 2)(c + d\sqrt 2) = (ac + 2bd) + (ad + bc)\sqrt 2\); if \(a + b\sqrt 2 \neq 0\) then \(a^2 - 2b^2 \neq 0\), because \(\sqrt 2\) is irrational, and
\[(a + b\sqrt 2)^{-1} = \frac{a}{a^2 - 2b^2} - \frac{b}{a^2 - 2b^2}\sqrt 2.\]
Properties

Intersections. The intersection of any family of subfields of \(K\) is a subfield: the infimum of a set of subfields has as underlying set the intersection of their underlying sets. A union of two subfields is usually not a subfield, but the supremum of a nonempty directed family of subfields is exactly their union.

Generated subfields. For a subset \(S \subseteq K\), the subfield generated by \(S\) is the intersection of all subfields containing \(S\). It is the smallest subfield containing \(S\): it is contained in a subfield \(F\) exactly when \(S \subseteq F\). Concretely, it consists of the quotients \(a b^{-1}\) of elements \(a, b\) of the subring generated by \(S\), with \(b \neq 0\). One consequence is that two ring homomorphisms out of \(K\) that agree on a set \(S\) generating \(K\) as a field are equal.

The prime subfield. The intersection of all subfields of \(K\) is the smallest subfield of \(K\), called its prime subfield. Since every subfield contains \(1\), it contains every integer multiple of \(1\) and every quotient of two such multiples with nonzero denominator; in a field of characteristic zero this says that every subfield contains the image of every rational number. The prime subfield is determined by the characteristic of \(K\):

In particular \(\mathbb{Q}\) and \(\mathbb{Z}/p\mathbb{Z}\) have no subfields other than themselves.

A subfield of \(K\) is the field analogue of a subgroup of a group or a subring of a ring. When a field \(L\) is an extension of a field \(K\), the subfields of \(L\) that contain the image of \(K\) are called intermediate fields; they are the objects of the Galois correspondence, and they appear throughout the theory of algebraic extensions and splitting fields. The finite fields give a clean picture: a field with \(p^n\) elements has exactly one subfield with \(p^m\) elements for each divisor \(m\) of \(n\), and no others.

In Mathlib

Mathlib defines subfields for any division ring, not only for fields, so its notion covers sub-division rings of noncommutative division rings such as the quaternions. A subfield is a bundled structure: a subring together with the condition that it is closed under inversion. Because Mathlib sets the inverse of \(0\) to be \(0\), this condition is stated for every element, with no exception for zero, and quotients by zero are likewise allowed in the description of generated subfields. The subfields of a division ring are ordered by inclusion and form a complete lattice, whose least element is the prime subfield and whose greatest element is the whole ring. Intermediate fields of an extension are a separate structure, each of which can be viewed as a subfield of the larger field.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibSubfield
Uses 3 · Used by 1
Statement usesField · Subring · Set
Used byPrimitive element theorem

DefinitionCharacteristic of a ring#

The characteristic of a ring is the least positive integer \(n\) for which adding the identity element \(1\) to itself \(n\) times gives \(0\), or \(0\) if no such integer exists. It measures how the integers sit inside the ring, and it separates rings of characteristic zero, such as the rational and real numbers, from rings of positive characteristic, such as the integers modulo \(n\) and the finite fields, where arithmetic behaves differently (for instance, \((x + y)^p = x^p + y^p\) can hold).

Definition

Let \(R\) be a ring with identity, and for a natural number \(n\) write \(n \cdot 1\) for the sum \(1 + 1 + \dots + 1\) of \(n\) copies of \(1\) (with \(0 \cdot 1 = 0\)). The set of \(n\) with \(n \cdot 1 = 0\) contains \(0\) and is closed under addition and under subtraction of a smaller element from a larger one, so it consists of the multiples of a single natural number \(c\): its least positive element, or \(0\) if it has none. This number \(c\) is the characteristic of \(R\), written \(\operatorname{char} R\). Equivalently, the characteristic is the unique natural number \(c\) such that for every natural number \(n\), \(n \cdot 1 = 0\) in \(R\) if and only if \(c\) divides \(n\). In particular \((\operatorname{char} R) \cdot 1 = 0\).

Two other descriptions are often useful. There is exactly one ring homomorphism from the integers to \(R\), and its kernel is the ideal of \(\mathbb{Z}\) generated by the characteristic. And the characteristic is the additive order of \(1\) when that order is finite, and \(0\) when \(1\) has infinite additive order; Mathlib assigns order \(0\) to an element of infinite order, so in its terms the characteristic is simply the additive order of \(1\). A ring with \(\operatorname{char} R = p\) is said to have characteristic \(p\).

Examples
Properties
In Mathlib

Mathlib defines the characteristic for any semiring, not necessarily commutative or even associative, and does not require subtraction. The basic notion is the predicate "\(R\) has characteristic \(p\)", which says that \(n \cdot 1 = 0\) exactly when \(p\) divides \(n\); every semiring satisfies it for exactly one \(p\), and the characteristic function returns that number, chosen noncomputably. The characteristic equals \(p\) precisely when this predicate holds for \(p\). The conventions match the textbook ones: characteristic \(0\) when no positive multiple of \(1\) vanishes, and characteristic \(1\) for the zero ring. For rings, characteristic \(0\) is equivalent to the injectivity of the map from the natural numbers, which Mathlib records as a separate characteristic-zero predicate; for semirings without subtraction the two can differ. Mathlib's integers modulo \(n\) are defined for every natural number \(n\), with modulus \(0\) giving the integers themselves, so the statement about their characteristic covers \(\mathbb{Z}\) as well.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibringChar
Uses 2 · Used by 4
Statement usesRing · Natural number
Used byQuadratic reciprocity · Orthogonality of characters · Ax–Grothendieck theorem · Maschke theorem

ClassCharacteristic zero#

A ring has characteristic zero when no positive multiple of its identity element vanishes: \(1 + 1 + \cdots + 1 \neq 0\) however many terms are added. The rational, real and complex numbers all have this property, while the integers modulo \(n\) for \(n \geq 1\) and every finite field do not. Characteristic zero is the setting in which the familiar arithmetic of the integers and the rationals survives inside a ring, so that distinct integers remain distinct in the ring and, in a field, one may divide by nonzero integers. It is one of the two cases in the classification of fields by their characteristic, the other being characteristic \(p\) for a prime \(p\).

Definition

For a ring \(R\) and a natural number \(n\), write \(n \cdot 1\) for the sum of \(n\) copies of the identity \(1\) of \(R\). The ring \(R\) has characteristic zero if the map \(n \mapsto n \cdot 1\) from the natural numbers to \(R\) is injective. In a ring this is the same as asking that \(n \cdot 1 \neq 0\) for every \(n \geq 1\): injectivity gives \(n \cdot 1 = 0\) exactly when \(n = 0\), and conversely, since \(m \cdot 1 = n \cdot 1\) with \(m \le n\) forces \((n - m) \cdot 1 = 0\) after subtracting, the condition \(n \cdot 1 \neq 0\) for all \(n \geq 1\) implies injectivity.

The characteristic of a ring is the least \(n \geq 1\) with \(n \cdot 1 = 0\), or \(0\) if there is no such \(n\). Thus a ring has characteristic zero exactly when its characteristic is \(0\).

Examples
Properties
In Mathlib

Mathlib defines characteristic zero as a property of any additive monoid with a distinguished element \(1\), not only of rings, and takes injectivity of the map from the natural numbers as the definition. For rings, and more generally whenever subtraction is available, this agrees with the condition that \(n \cdot 1 \neq 0\) for \(n \geq 1\), but without subtraction the two can differ. Take the two-element set \(\{0, 1\}\), with the maximum as addition and the minimum as multiplication. Every positive multiple of \(1\) equals \(1\), so \(0\) is the only natural number sent to \(0\), but distinct positive numbers have the same image; this semiring has characteristic \(0\) in the sense of the characteristic-\(p\) condition without having characteristic zero in Mathlib's sense. Characteristic zero is recorded as a class that the library finds automatically, so the facts above about \(\mathbb{Q}\)-algebras, separability and perfection apply to a field as soon as its characteristic is known to be zero. The integers modulo \(0\) are the integers themselves, and they have characteristic zero.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibCharZero
Uses 2 · Used by 91
Statement usesRing · Natural number
Used byDe Moivre’s Formula · Formula for Pythagorean Triples · Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · Sum of the Angles of a Triangle · The Area of a Circle · The Irrationality of the Square Root of 2 · The Non-Denumerability of the Continuum · Divergence of the Harmonic Series · Heron’s Formula · Königsberg Bridges Problem · Minkowski’s Fundamental Theorem · Product of Segments of Chords · Sum of the Reciprocals of the Triangular Numbers · The Ballot Problem · The Solution of the General Quartic Equation · Sum of kth powers · Bertrand’s Postulate · Buffon Needle Problem · Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) · Divergence of the Prime Reciprocal Series · Stirling’s Formula · The Birthday Problem · The Factor and Remainder Theorems · The Friendship Theorem · The Fundamental Theorem of Arithmetic · Jensen's inequality (finite sum version) · Eigenvalues from Rayleigh quotient · Regularization by convolution · Banach open mapping theorem · Behrend's construction · Cauchy-Davenport theorem · Erdős–Ginzburg–Ziv theorem · Small tripling implies small powers · Regularity lemma · Triangle counting lemma · Ahlswede-Zhang identity · LYM inequality · Translation numbers define a group action up to semiconjugacy · Multiplicity · Jacobi/Leibniz identity · Sphere · Uniform time existence · Chebyshev inequality · Mean of product of independent random variables · Stone-Weierstrass theorem · Urysohn's lemma · Arzela-Ascoli theorem · Krull's principal ideal theorem · Birkhoff–Von Neumann theorem · Dimension theorem for vector spaces · Lie's theorem · Abel's theorem · Besicovitch covering theorem · Rademacher's theorem · Fernique's theorem · Hahn decomposition theorem · Vitali convergence theorem · Vitali covering theorem · Fourier theorem · Akra–Bazzi theorem · Hahn embedding theorem · Apollonius's theorem · British flag theorem · Commandino's theorem · Intersecting secants theorem · Tangent-secant theorem · Thales's theorem · Lebesgue's decomposition theorem · Dirichlet's approximation theorem · Dirichlet's unit theorem · Glaisher's theorem · Mahler's theorem · Pentagonal number theorem · Poisson limit theorem · Slutsky's theorem · Sylvester's law of inertia (existence) · Partial derivatives commute · Taylor's theorem with integral form for remainder (Differential calculus) · Cos (power series expansion of elementary functions) · Log · Sin (power series expansion of elementary functions) · Cauchy formulas · Holomorphic stability under uniform convergence · Continuity (continuity and differentiability of convex functions) · Comparison of a series and an integral · Convergence of \(p\)-series for \(p>1\) · Differentiability of the limit of a sequence of functions · Taylor's theorem with Lagrange form for remainder · Completeness of \(l^2\) · Completeness of \(L^2\) · Hilbert projection theorem

ClassCharacteristic p#

A ring \(R\) has characteristic \(p\) when adding the identity element \(1\) to itself \(n\) times gives \(0\) exactly for the multiples \(n\) of \(p\). The characteristic measures how the integers sit inside a ring: in characteristic \(0\) they embed faithfully, while in a positive characteristic \(p\) the ring arithmetic of whole numbers wraps around modulo \(p\). Commutative rings and fields of prime characteristic have an algebra of their own, governed by the identity \((x + y)^p = x^p + y^p\), and they appear throughout number theory, algebraic geometry and coding theory.

Definition

For a natural number \(n\), write \(n \cdot 1\) for the sum \(1 + 1 + \dots + 1\) with \(n\) terms in a ring \(R\). A natural number \(p\) is the characteristic of \(R\) if, for every natural number \(n\), \(n \cdot 1 = 0\) in \(R\) if and only if \(p\) divides \(n\); this condition is the definition of characteristic \(p\).

Every ring has exactly one characteristic. If some positive \(n\) satisfies \(n \cdot 1 = 0\), the characteristic is the least such \(n\); otherwise it is \(0\), and the ring has characteristic zero. Equivalently, the characteristic is the nonnegative generator of the kernel of the unique ring homomorphism from the integers to \(R\): an integer \(m\) maps to \(0\) if and only if \(p\) divides \(m\). It is also the additive order of \(1\), with the convention that an element of infinite additive order has order \(0\). The number itself, as a function of the ring, is the subject of the article on the characteristic of a ring.

Many authors reserve the phrase "characteristic \(p\)" for a prime \(p\). For a prime \(p\) and a ring with \(1 \neq 0\), the condition simplifies: \(R\) has characteristic \(p\) if and only if \(p \cdot 1 = 0\).

Examples
Properties

Reduction modulo \(p\). In a ring of characteristic \(p\), \(k \cdot 1 = (k \bmod p) \cdot 1\) for every natural number \(k\), so the image of the natural numbers is a copy of \(\mathbb{Z}/p\mathbb{Z}\) (or of the natural numbers themselves when \(p = 0\)).

Domains and fields. The characteristic of a nonzero ring without zero divisors is either \(0\) or a prime number. This covers every integral domain and every field. The reason is short: if the characteristic were \(p = ab\) with \(1 < a, b < p\), then \((a \cdot 1)(b \cdot 1) = p \cdot 1 = 0\), so one factor would vanish, contradicting the minimality of \(p\). The value \(1\) is excluded because the ring is nonzero.

Finite rings. The natural numbers cannot inject into a finite set, so every finite ring has positive characteristic. Combined with the previous fact, a finite nonzero ring without zero divisors has prime characteristic. So the characteristic \(p\) of a finite field is prime, the field is a vector space over \(\mathbb{F}_p\) of some finite dimension \(n \ge 1\), and \(p\) is prime and the field has \(p^n\) elements for some positive integer \(n\) (see finite fields).

Homomorphisms. If \(f \colon R \to A\) is an injective ring homomorphism and \(R\) has characteristic \(p\), then \(A\) has characteristic \(p\). Thus a subring shares the characteristic of the ambient ring, and a field extension shares the characteristic of the base field.

The binomial identity. Let \(R\) be a commutative ring of prime characteristic \(p\). For \(0 < k < p\) the binomial coefficient \(\binom{p}{k}\) is divisible by \(p\), so every middle term of the binomial theorem vanishes and \((x + y)^p = x^p + y^p\) for all \(x, y\) in \(R\). Likewise \((x - y)^p = x^p - y^p\), and by induction \((x + y)^{p^n} = x^{p^n} + y^{p^n}\) for every natural number \(n\). Since \((xy)^p = x^p y^p\) and \(1^p = 1\) as well, the map \(x \mapsto x^p\) is a ring homomorphism from \(R\) to itself, the Frobenius morphism.

The characteristic of a ring is the number \(p\) viewed as a function of \(R\). Rings of characteristic zero are those in which the natural numbers embed. The Frobenius morphism leads to the notion of a perfect field (in prime characteristic, a field on which the Frobenius morphism is surjective) and to the perfect closure of a field of prime characteristic. Over a field of characteristic \(p\) that is not perfect, an irreducible polynomial can fail to be separable, as \(X^p - t\) does over the field of rational functions \(\mathbb{F}_p(t)\); in characteristic zero this cannot happen.

In Mathlib

Mathlib states "\(R\) has characteristic \(p\)" as a property of the pair \((R, p)\) rather than as a function of \(R\), and it does so for any additive structure with a \(1\), not only rings; the ring structure enters only in the theorems that need it. The number \(p\) is any natural number, so characteristic zero is the case \(p = 0\), and primality is a separate hypothesis wherever a theorem needs it. For rings, characteristic \(0\) in this sense agrees with the requirement that the map from the natural numbers be injective: a ring has characteristic \(0\) in this sense if and only if the natural numbers inject into it. For semirings without negation the two can differ. Mathlib defines the Frobenius map more generally, for the exponential characteristic, which is \(p\) in prime characteristic \(p\) and \(1\) in characteristic zero.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibCharP
Uses 3 · Used by 24
Statement usesRing · Natural number · Integer
Used byEuler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. · Formula for Pythagorean Triples · Dirichlet’s Theorem · The Ballot Problem · Sum of kth powers · Stirling’s Formula · Behrend's construction · Triangle removal lemma · Lucas-Lehmer primality test · Frobenius morphism · Perfect closure · Chevalley-Warning theorem (Number theory) · Perfection of a ring · Central limit theorem · Chevalley–Warning theorem (1000+ theorems) · Schwartz–Zippel theorem · Hadamard three-lines theorem · Ax–Grothendieck theorem · Lebesgue's decomposition theorem · Niven's theorem · Ostrowski's theorem · Taylor's theorem with integral form for remainder (Differential calculus) · Log · Comparison of a series and an integral

DefinitionFrobenius morphism#

The Frobenius morphism (or Frobenius endomorphism) of a commutative ring of prime characteristic \(p\) is the map that raises every element to its \(p\)-th power. In characteristic \(p\) this map preserves sums as well as products, so it is a ring homomorphism from the ring to itself. In characteristic zero no power map \(x \mapsto x^n\) with \(n > 1\) is additive, since \((1+1)^n = 2^n\) differs from \(1^n + 1^n = 2\). It is the basic tool for studying finite fields, whose Galois groups it generates, and it underlies the notion of a perfect field and much of arithmetic geometry in positive characteristic.

Definition

Let \(R\) be a commutative ring whose characteristic is a prime \(p\). The Frobenius morphism is the map \(F \colon R \to R\) given by \(F(x) = x^p\), and this map is a ring homomorphism. It sends \(1\) to \(1\) and, because \(R\) is commutative, satisfies \((xy)^p = x^p y^p\). Additivity is the key point: the binomial theorem gives

\[(x+y)^p = \sum_{k=0}^{p} \binom{p}{k} x^k y^{p-k},\]

and for \(0 < k < p\) the prime \(p\) divides \(\binom{p}{k} = \frac{p!}{k!\,(p-k)!}\), since it divides the numerator but not the denominator. Those terms vanish in \(R\), leaving \((x+y)^p = x^p + y^p\), sometimes called the freshman's dream. Applying additivity to \((x-y) + y\) gives \((x-y)^p = x^p - y^p\).

Iterating, the \(n\)-fold composite of \(F\) with itself is the map \(x \mapsto x^{p^n}\), which is again a ring homomorphism.

Examples
  • The field with \(p\) elements. On \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\), the Frobenius morphism is the identity. This is a restatement of Fermat's little theorem in the form \(a^p \equiv a \pmod p\).
  • Finite fields. If \(K\) is a finite field of characteristic \(p\) with \(p^n\) elements, then \(F^n\) is the identity of \(K\), because every element \(a\) of \(K\) satisfies \(a^{p^n} = a\).
  • Polynomials. On the polynomial ring \(\mathbb{F}_p[t]\) the coefficients are fixed, so \(F\) sends \(f(t)\) to \(f(t^p)\). More generally, if \(K\) is a finite field with \(q\) elements, then \(f(X)^q = f(X^q)\) for every polynomial \(f\) over \(K\). On \(\mathbb{F}_p[t]\), \(F\) is injective, since \(\mathbb{F}_p[t]\) is an integral domain, but not surjective: its image consists of the polynomials in \(t^p\).
  • A non-injective case. In \(\mathbb{F}_p[x]/(x^p)\) the class of \(x\) is nonzero but its \(p\)-th power is zero, so \(F\) has a nonzero kernel.
Properties
Galois groups of finite fields

Let \(L\) be a finite field and \(K\) a subfield with \(q\) elements, and let \(n = [L : K]\) be the degree of the extension. The map \(\sigma(x) = x^q\) is a power of the Frobenius morphism of \(L\) and fixes \(K\) pointwise. As a power of the injective Frobenius of a field it is injective, and an injective map from the finite set \(L\) to itself is bijective, so it is an automorphism of \(L\) over \(K\). Its order in the Galois group is \(n\), and every element of the Galois group equals \(\sigma^i\) for exactly one \(i\) with \(0 \le i < n\). So the Galois group of \(L\) over \(K\) is a cyclic group of order \(n\) generated by \(\sigma\). Since the Galois group has order \(n = [L : K]\), the extension is Galois, and the Galois correspondence gives exactly one intermediate field of degree \(d\) over \(K\) for each divisor \(d\) of \(n\).

The Frobenius automorphism of a finite field has a counterpart in Galois extensions of number fields. Each prime \(P\) of the upper field lying over a prime \(\mathfrak{p}\) of the lower field that does not ramify has a Frobenius element: the unique Galois automorphism that maps \(P\) to itself and induces \(x \mapsto x^{N}\) on the residue field at \(P\), where \(N\) is the number of elements of the residue field at \(\mathfrak{p}\). Primes over the same \(\mathfrak{p}\) give conjugate elements, so the Frobenius of \(\mathfrak{p}\) itself is defined only up to conjugacy. On a scheme over \(\mathbb{F}_p\), the absolute Frobenius acts as the identity on the underlying space and as the \(p\)-th power map on functions. The perfect closure and the perfection of a ring of characteristic \(p\) are the universal ways of making its Frobenius bijective.

In Mathlib

Mathlib defines the Frobenius morphism as a bundled ring homomorphism on any commutative semiring, with the exponent \(p\) given explicitly together with the hypothesis that \(p\) is the exponential characteristic of the ring. The exponential characteristic is the characteristic when that is prime and \(1\) when the characteristic is zero, so in characteristic zero the Frobenius morphism is the identity map, and for a ring such as \(\mathbb{Z}/6\mathbb{Z}\), whose characteristic is neither prime nor zero, it is not defined. The iterated map \(x \mapsto x^{p^n}\) has its own definition. A perfect ring is defined by bijectivity of the \(p\)-th power map, while a perfect field is defined separately by separability of irreducible polynomials, and the two are linked by the results above. For an extension of finite fields, the automorphism \(x \mapsto x^q\) with \(q\) the size of the base field is a separate object, built as an automorphism over the base field, and is defined more generally for any algebraic extension of a finite field.

Written for Trough, under CC BY-SA 4.0.

Sources
Mathlibfrobenius
Uses 5 · Used by 3
Statement usesRing · Ring morphism · Characteristic p · Prime numbers
Proof usesThe Binomial Theorem
Used byPerfect closure · Perfection of a ring · Quadratic reciprocity

ClassAlgebraically closed field#

An algebraically closed field is a field in which every nonconstant polynomial in one variable has a root. In such a field every polynomial breaks up completely into linear factors, so questions about polynomial equations reduce to questions about their roots. The complex numbers are the most familiar example. Algebraically closed fields are the natural setting for linear algebra over a field (every square matrix of positive size has an eigenvalue) and for classical algebraic geometry, where the Nullstellensatz needs them.

Definition

A field \(k\) is algebraically closed if every polynomial with coefficients in \(k\) is a product of a constant and linear factors:

\[f = c\,(x - a_1)(x - a_2)\cdots(x - a_n), \qquad c, a_1, \dots, a_n \in k.\]

Several conditions are equivalent to this.

Examples
Properties
Consequences
In Mathlib

Mathlib states algebraic closedness as a property of a field, defined by asking that every polynomial split, where a polynomial splits when it is a product of constants and monic linear polynomials. The zero polynomial and the nonzero constants split trivially, so the definition imposes no condition on them. The formulation through roots is a theorem, in both directions, and the converse only asks for roots of monic irreducible polynomials. The degree condition in the root statement only excludes the nonzero constants, so it also covers the zero polynomial, which has every element as a root. Being an algebraic closure is a separate property of an extension, defined over suitable commutative rings and not only over fields. Mathlib constructs one algebraic closure of each field, as a quotient of a polynomial ring in many variables by a maximal ideal, and records that the complex numbers are algebraically closed. The classification by cardinality is stated with the characteristic given as a natural number, which is \(0\) in characteristic zero.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibIsAlgClosed
Uses 3 · Used by 10
Statement usesField · Polynomial in one indeterminate · Roots of a polynomial
Used byFundamental theorem of algebra · \(\C\) is algebraically closed · Existence of algebraic closure of a field · Orthogonality of characters · Nullstellensatz · Existence of an eigenvalue · Schur's lemma (1000+ theorems) · Ax–Grothendieck theorem · Complex classification · Schur's lemma (Linear representations)

DefinitionExistence of algebraic closure of a field#

The existence of an algebraic closure is the theorem that every field \(k\) has an algebraic extension \(\bar k\) that is algebraically closed. Such a field \(\bar k\) is called an algebraic closure of \(k\); it is unique up to isomorphism over \(k\). The theorem supplies, for every field, one ambient field in which every polynomial over \(k\) splits into linear factors, so that roots, splitting fields and algebraic extensions of \(k\) can all be studied inside a single field.

Statement

A field is algebraically closed when every nonconstant polynomial over it has a root; equivalently, every nonzero polynomial over it is a constant times a product of linear factors. Over an algebraically closed field, every polynomial of nonzero degree has a root. An extension \(K\) of a field \(k\) is an algebraic closure of \(k\) when \(K\) is algebraically closed and algebraic over \(k\), that is, every element of \(K\) is a root of a nonzero polynomial with coefficients in \(k\).

Theorem. Every field \(k\) has an algebraic closure: there is a field \(\bar k\) containing \(k\) such that \(\bar k\) is algebraic over \(k\) and \(\bar k\) is algebraically closed. Mathlib constructs such a field, the algebraic closure of \(k\), for every field \(k\).

Examples
Properties
Proof

Mathlib follows a construction that builds \(\bar k\) in one step as a quotient of a polynomial ring, instead of applying Zorn's lemma to a collection of algebraic extensions of \(k\); Zorn's lemma still enters, through the maximal ideal. For each monic polynomial \(f\) over \(k\) of degree \(n\), introduce \(n\) new variables \(X_{f,1}, \dots, X_{f,n}\), and let \(A\) be the polynomial ring over \(k\) in all these variables, for all \(f\) at once. Let \(I\) be the ideal of \(A\) generated by the coefficients, as a polynomial in a further variable \(x\), of

\[f(x) - (x - X_{f,1})(x - X_{f,2})\cdots(x - X_{f,n})\]

for every monic \(f\). The quotient of \(A\) by an ideal containing \(I\) is a ring in which each such \(f\) factors as the product of the linear factors \(x - X_{f,i}\).

First, \(I\) is a proper ideal. If \(1\) lay in \(I\), it would be a finite combination of the generators, involving only finitely many polynomials \(f_1, \dots, f_m\). In a splitting field of the product \(f_1 \cdots f_m\), each \(f_j\) factors into linear factors; sending the variables \(X_{f_j,i}\) to the roots of \(f_j\), listed with multiplicity, and the remaining variables to any value gives a homomorphism from \(A\) that kills every generator involved, yet sends \(1\) to \(1\), a contradiction.

Next, every proper ideal lies in a maximal ideal, so \(I\) lies in a maximal ideal \(M\). Since an ideal is maximal exactly when the quotient by it is a field, the quotient ring \(\bar k = A/M\) is a field. It contains a copy of \(k\), and in it every monic polynomial over \(k\) splits. It is generated over \(k\) by the images of the variables, each a root of some polynomial over \(k\), so \(\bar k\) is algebraic over \(k\).

Finally, \(\bar k\) is algebraically closed. By a general criterion, a field in which every monic irreducible polynomial has a root is algebraically closed. Let \(g\) be such a polynomial over \(\bar k\) and \(\alpha\) a root of \(g\) in some extension field. Then \(\alpha\) is algebraic over \(\bar k\), which is algebraic over \(k\), so \(\alpha\) is algebraic over \(k\). Its minimal polynomial over \(k\) splits in \(\bar k\), so \(\alpha\) lies in \(\bar k\), and \(g\) has a root in \(\bar k\).

  • An algebraically closed field is the kind of field the theorem produces.
  • A rupture field adjoins one root of an irreducible polynomial, and a splitting field all roots of one polynomial; the algebraic closure does this for all polynomials at once.
  • The perfect closure of a field of characteristic \(p\) is, up to isomorphism, the smallest perfect extension of it, that is, the smallest extension in which every element of the extension has a \(p\)-th root; it embeds in \(\bar k\).
In Mathlib

Mathlib defines the algebraic closure of a field \(k\) as a specific field built by the construction above, a quotient of a polynomial ring in many variables by a maximal ideal chosen by the axiom of choice, and records as instances that it is a field, an algebra over \(k\), algebraic over \(k\) and algebraically closed, and that it is an algebraic closure of \(k\) in the sense of the separate property described next. For the last step of the proof, Mathlib argues by divisibility instead of passing to an extension field: an irreducible polynomial over \(\bar k\) divides the image of a monic irreducible polynomial over \(k\), which splits, so it splits too. The field lives in the same universe of types as \(k\). Being an algebraic closure is a separate property of an extension, stated for a commutative ring \(R\) and a field \(K\) that is a torsion-free algebra over it; the uniqueness theorem and the embedding theorem hold more generally for an integral domain in place of \(k\), with torsion-freeness conditions on the algebras that are automatic over a field.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibAlgebraicClosure
Uses 10 · Used by 1
Statement usesField · Polynomial in one indeterminate · Algebraic extension · Algebraically closed field
Proof usesPolynomial in several indeterminates · Maximal ideal · Quotient ring · Splitting field · Rupture field · Minimal polynomial
Used byAx–Grothendieck theorem

Theorem\(\C\) is algebraically closed#

The statement that \(\mathbb{C}\) is algebraically closed, usually called the fundamental theorem of algebra, says that every nonconstant polynomial with complex coefficients has a complex root. It means that the complex numbers need no further enlargement to solve polynomial equations: adjoining a square root of \(-1\) to the real numbers already produces a field in which every polynomial equation of positive degree has a solution. The result underlies the factorization of real and complex polynomials, the existence of eigenvalues in linear algebra, and much of algebraic geometry over \(\mathbb{C}\).

Statement

Let \(f(z) = a_n z^n + a_{n-1} z^{n-1} + \cdots + a_1 z + a_0\) be a polynomial with complex coefficients and \(a_n \neq 0\), where \(n \ge 1\). Then there is a complex number \(z_0\) with \(f(z_0) = 0\).

Applying this repeatedly, together with the fact that \(z_0\) is a root of \(f\) exactly when \(z - z_0\) divides \(f\), splits off one linear factor at a time. Hence every complex polynomial factors completely,

\[f(z) = a_n (z - z_1)(z - z_2) \cdots (z - z_n), \qquad z_1, \dots, z_n \in \mathbb{C},\]

which is to say that the field \(\mathbb{C}\) is algebraically closed in the sense of the article algebraically closed field. That formulation, as a property of the field, is treated in the article fundamental theorem of algebra; this article concerns the existence of a root for a single polynomial.

Examples
  • The polynomial \(z^2 + 1\) has no real root but has the complex roots \(i\) and \(-i\).
  • For every complex number \(a\) and every integer \(n \ge 1\), the polynomial \(z^n - a\) has a root, so every complex number has an \(n\)-th root; Mathlib proves this for any algebraically closed field. Writing \(a = r e^{i\theta}\) with \(r \ge 0\), one such root is \(r^{1/n} e^{i\theta/n}\).
  • A polynomial of degree \(5\) with integer coefficients may have roots that cannot be written using radicals, but it still has five complex roots counted with multiplicity. The theorem asserts existence, not a formula.
Proof

The proof in Mathlib uses complex analysis. Suppose that \(f\) has positive degree and no root. Then \(g = 1/f\) is defined on all of \(\mathbb{C}\), and it is complex differentiable everywhere, because polynomial functions are differentiable and \(f\) never vanishes. Since \(f\) has positive degree, \(|f(z)| \to \infty\) as \(|z| \to \infty\), so \(g(z) \to 0\) as \(|z| \to \infty\). A continuous function on \(\mathbb{C}\) that tends to \(0\) at infinity is bounded. By Liouville's theorem, a bounded function that is complex differentiable on the whole plane is constant, and a constant that tends to \(0\) is \(0\). But \(g = 1/f\) never takes the value \(0\), a contradiction.

A second classical argument avoids Liouville's theorem. Since \(|f(z)|\) grows without bound, \(|f|\) attains a minimum value at some point \(z_0\) of \(\mathbb{C}\). If \(f(z_0) \neq 0\), expand \(f\) around \(z_0\) as \(f(z_0 + w) = f(z_0) + c\,w^k + (\text{terms of degree} > k \text{ in } w)\) with \(c \neq 0\) and \(k \ge 1\). Choosing \(w\) small, with \(c\,w^k\) pointing in the direction opposite to \(f(z_0)\), makes \(|f(z_0 + w)| < |f(z_0)|\), contradicting minimality. So \(f(z_0) = 0\).

To pass from roots to algebraic closedness, it suffices that every monic irreducible polynomial has a root, and an irreducible polynomial has positive degree (see irreducible element), so the root statement applies to it.

Consequences
In Mathlib

Mathlib states the theorem for a single polynomial: if its degree is positive, it has a complex root. The degree of the zero polynomial is taken to be minus infinity rather than a natural number, so the hypothesis of positive degree excludes exactly the zero polynomial and the nonzero constants, and the root is expressed as a point where the polynomial evaluates to zero. The statement that \(\mathbb{C}\) is an algebraically closed field is recorded separately, derived from the root statement through the criterion on monic irreducible polynomials. Through it, every general theorem about algebraically closed fields, such as root counting and the existence of eigenvalues, applies to the complex numbers. The proof applies a corollary of Liouville's theorem, for differentiable functions that tend to a limit at infinity, directly to \(1/f\), so the boundedness step of the sketch above stays implicit. Mathlib proves Liouville's theorem for complex differentiable maps between complex normed spaces, not only for functions from \(\mathbb{C}\) to \(\mathbb{C}\), and it proves the growth of polynomials at infinity over any normed ring whose norm is multiplicative.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibComplex.exists_root
Uses 7 · Used by 1
Statement usesComplex number · Polynomial in one indeterminate · Polynomial functions · Algebraically closed field
Proof usesDifferentiable functions · Liouville theorem · Irreducible element
Used byFundamental theorem of algebra

AbbreviationField of fractions of an integral domain#

The field of fractions of an integral domain \(A\) is the smallest field in which \(A\) sits as a subring: its elements are quotients \(a/b\) of elements of \(A\) with \(b \neq 0\), added and multiplied by the rules of school arithmetic. The passage from the integers to the rational numbers is the model case, and the passage from polynomials to rational functions is another. The construction lets questions about a domain be asked inside a field, where linear algebra and the theory of field extensions are available, and it is the special case of localization in which every nonzero element is inverted.

Definition

Let \(A\) be an integral domain, that is, a nonzero commutative ring without zero divisors. On pairs \((a, b)\) with \(a, b \in A\) and \(b \neq 0\), call \((a, b)\) and \((c, d)\) equivalent when \(ad = bc\). Write \(a/b\) for the class of \((a, b)\) and define

\[\frac{a}{b} + \frac{c}{d} = \frac{ad + bc}{bd}, \qquad \frac{a}{b} \cdot \frac{c}{d} = \frac{ac}{bd}.\]

These operations are well defined, and the classes form the field of fractions of \(A\), written \(\operatorname{Frac}(A)\). The same classes arise from the general construction of a localization, in which \((a, b)\) and \((c, d)\) are related when \(u(ad) = u(bc)\) for some allowed denominator \(u\). There two fractions are equal exactly when their pairs are so related, and, because no allowed denominator is a zero divisor, the pairs \((a, b)\) and \((c, d)\) are related exactly when \(ad = bc\). The ring obtained is a field: a nonzero fraction \(a/b\) has \(a \neq 0\), and its inverse is \(b/a\). The map \(a \mapsto a/1\) is an injective ring homomorphism through which \(A\) is regarded as a subring.

Since many fields contain a copy of a given domain, it is useful to say when a given field \(K\), together with a ring homomorphism \(f\) from \(A\) to \(K\), is a field of fractions of \(A\). For a field \(K\) this happens exactly when \(f\) is injective and every element of \(K\) is a quotient \(f(a)/f(b)\): these two conditions suffice, and conversely, if \(K\) is a field of fractions, then \(f\) is injective and every element of \(K\) has the form \(f(a)/f(b)\) with \(b\) a non-zero-divisor, which in a domain means \(b \neq 0\).

Universal property

The field of fractions is the most economical field containing \(A\). Let \(K\) be a field of fractions of \(A\), let \(L\) be any field and \(g\) an injective ring homomorphism from \(A\) to \(L\). Then \(g\) extends to a ring homomorphism \(h\) from \(K\) to \(L\), so that \(h(f(a)) = g(a)\) for all \(a \in A\), namely \(h(f(a)/f(b)) = g(a)/g(b)\), and any ring homomorphism from \(K\) to \(L\) with this property equals \(h\). Moreover the image of \(h\) is the subfield of \(L\) generated by \(g(A)\). So whenever a domain is a subring of a field, the subfield it generates is a copy of its field of fractions; for instance the subfield of \(\mathbb C\) generated by the Gaussian integers \(\mathbb Z[i]\) is \(\mathbb Q(i)\).

It follows that the field of fractions is unique up to unique isomorphism: every field of fractions \(K\) of \(A\) is isomorphic, as an \(A\)-algebra, to the construction \(\operatorname{Frac}(A)\).

Examples
Properties

The field of fractions is the localization of \(A\) at the set of its nonzero elements; localizing at smaller multiplicative sets gives rings between \(A\) and \(\operatorname{Frac}(A)\), such as the ring of rationals with odd denominator. Fractional ideals of \(A\) are \(A\)-submodules of \(\operatorname{Frac}(A)\) that behave like ideals with a common denominator, and they are the setting for the ideal theory of Dedekind domains.

In Mathlib

Mathlib separates the property from the construction. The property says that a given algebra \(K\) over a commutative ring \(R\) is a ring of fractions of \(R\), and it is defined as being the localization of \(R\) at its non-zero-divisors; the construction is one particular such algebra, and any other is isomorphic to it, so results are stated for an arbitrary \(K\) with the property. Because the property is stated for any commutative ring, not only domains, it describes the total ring of fractions in general, and the field structure is proved, not assumed, when \(R\) is a domain. It is even stated for commutative semirings, which covers the nonnegative rationals as the semiring of fractions of the natural numbers. The criterion for a field to be a field of fractions phrases injectivity as faithfulness of the scalar action of \(R\) on \(K\), which for an algebra amounts to the same thing. Integral closedness is defined with respect to the standard construction, and Mathlib proves that any other field of fractions may be used instead.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibIsFractionRing
Uses 3 · Used by 7
Statement usesRing · Field · Ring morphism
Used byFractional ideal · \(A[{X_i}]\) is a UFD when \(A\) is a UFD · Eisenstein's criterion · Nullstellensatz · Integral root theorem · Rational root theorem · Ostrowski's theorem

ClassAlgebraic extension#

An algebraic extension is a field extension \(L/K\) in which every element of \(L\) is a root of some nonzero polynomial with coefficients in \(K\). Algebraic extensions are the setting of most of classical field theory: finite extensions, splitting fields and Galois extensions are all algebraic, and every algebraic extension of a field embeds into its algebraic closure, which is thus the largest algebraic extension up to isomorphism. The opposite behaviour, an element satisfying no nonzero polynomial relation over \(K\), is called transcendence.

Definition

Let \(K\) be a field and \(L\) an extension field of \(K\). An element \(\alpha \in L\) is algebraic over \(K\) if it is a root of a nonzero polynomial with coefficients in \(K\), and transcendental otherwise. The extension \(L/K\) is algebraic when every element of \(L\) is algebraic over \(K\).

Since \(K\) is a field, a nonzero polynomial can be divided by its leading coefficient, so an element is algebraic exactly when it is a root of a monic polynomial over \(K\), that is, when it is integral over \(K\). Hence an extension of a field is algebraic if and only if it is integral. For an algebraic element \(\alpha\), the monic polynomial of least degree with root \(\alpha\) is its minimal polynomial.

Examples
  • The extension \(\mathbb{Q}(\sqrt 2)/\mathbb{Q}\) is algebraic: it has dimension \(2\) over \(\mathbb{Q}\), and finite extensions are algebraic (see below). Directly, \(a + b\sqrt 2\) is a root of \(x^2 - 2ax + a^2 - 2b^2\).
  • The extension \(\mathbb{C}/\mathbb{R}\) is algebraic, since \(a + bi\) is a root of the real polynomial \(x^2 - 2ax + a^2 + b^2\).
  • The complex numbers that are algebraic over \(\mathbb{Q}\) form a field, and it is algebraic over \(\mathbb{Q}\) of infinite degree: it contains \(\sqrt[n]{2}\), whose minimal polynomial \(x^n - 2\) has degree \(n\), for every \(n \ge 1\). So an algebraic extension need not be finite.
  • The real numbers are not algebraic over the rational numbers. An algebraic extension of a countable field is countable (see the cardinality bound below), while \(\mathbb{R}\) is uncountable.
  • The field \(K(x)\) of rational functions in one variable is not algebraic over \(K\): no nonzero polynomial over \(K\) vanishes at \(x\).
Properties
  • Finite extensions are algebraic. If \(L\) is finite-dimensional over \(K\), then \(L/K\) is algebraic. If \([L : K] = n\) and \(\alpha \in L\), the \(n + 1\) elements \(1, \alpha, \dots, \alpha^n\) are linearly dependent over \(K\), and a dependence relation is a nonzero polynomial vanishing at \(\alpha\). The examples above show that the converse fails.
  • Generated extensions. For a subset \(S\) of \(L\), the field \(K(S)\) is algebraic over \(K\) if and only if every element of \(S\) is algebraic over \(K\). In particular \(K(\alpha)/K\) is algebraic whenever \(\alpha\) is, and it is then finite-dimensional of degree equal to the degree of the minimal polynomial of \(\alpha\).
  • Towers. Let \(K \subseteq M \subseteq L\) be fields. If \(L/K\) is algebraic, then \(L/M\) is algebraic and \(M/K\) is algebraic. Conversely, if \(L/M\) and \(M/K\) are both algebraic, then \(L/K\) is algebraic: an element of \(L\) satisfies a polynomial with finitely many coefficients in \(M\), these generate a finite extension of \(K\), and adjoining the element gives a larger finite extension of \(K\), which is algebraic.
  • Relative algebraic closure. For any extension \(L/K\), the elements of \(L\) algebraic over \(K\) form an intermediate field, the relative algebraic closure of \(K\) in \(L\): an element of \(L\) lies in it exactly when it is algebraic over \(K\), and this field is algebraic over \(K\). It is the largest intermediate field algebraic over \(K\).
  • Composita. The field generated by any family of intermediate fields of \(L/K\), each algebraic over \(K\), is again algebraic over \(K\).
  • Cardinality. An algebraic extension \(L\) of \(K\) has at most \(\max(|K|, \aleph_0)\) elements, because each element is one of the finitely many roots of one of the polynomials over \(K\).
  • Endomorphisms. If \(L/K\) is algebraic, then every homomorphism of \(K\)-algebras from \(L\) to itself is bijective. Such a map is injective, like every homomorphism of fields, and it sends each root in \(L\) of a nonzero polynomial over \(K\) to a root of the same polynomial; so it permutes the finite set of roots of the polynomial of each element, and in particular hits that element.

A field \(k\) is algebraically closed exactly when it has no proper algebraic extensions: if \(k\) is algebraically closed and \(K/k\) is any extension, the only intermediate field algebraic over \(k\) is \(k\) itself. An algebraic closure of \(K\) is an algebraic extension that is algebraically closed, and Mathlib's algebraic closure of a field is algebraic over it. The splitting field of a polynomial is a finite, hence algebraic, extension. Galois theory concerns algebraic extensions that are also normal and separable.

In Mathlib

Mathlib defines algebraicity for an arbitrary algebra \(A\) over a commutative ring \(R\), not only for field extensions: \(A\) is algebraic over \(R\) when each of its elements is a root of a nonzero polynomial with coefficients in \(R\). It is a property attached to the pair, recorded as a type class so that it can be found automatically, and a field extension \(L/K\) is treated as \(L\) viewed as an algebra over \(K\). Over a ring that is not a field, algebraic and integral differ, and some results need extra hypotheses: the transitivity theorem asks the middle ring to have no zero divisors, and the cardinality bound and the result on endomorphisms are stated for an integral domain acting without torsion on a larger integral domain (for endomorphisms, a field), which covers every field extension. One consequence of the definition is that no algebra over the zero ring is algebraic, since the zero ring has no nonzero polynomials.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibAlgebra.IsAlgebraic
Uses 3 · Used by 4
Statement usesField · Polynomial in one indeterminate · Algebraic elements
Used byExistence of algebraic closure of a field · Galois correspondence · Nullstellensatz · Gelfand–Mazur theorem

DefinitionRupture field#

A rupture field of an irreducible polynomial \(f\) over a field \(K\) is an extension of \(K\) generated by a single root of \(f\). The standard model is the quotient ring \(K[X]/(f)\), in which the class of \(X\) is a root of \(f\) by construction. Applied to an irreducible factor, this quotient construction is how one proves that every nonconstant polynomial over a field has a root in some extension, and iterating it produces splitting fields. The same quotient makes sense for any polynomial over any commutative ring, and is then called adjoining a root.

Definition

Let \(R\) be a commutative ring and \(f\) a polynomial in \(R[X]\). The ring obtained by adjoining a root of \(f\) to \(R\) is the quotient of \(R[X]\) by the principal ideal generated by \(f\):

\[R[X]/(f).\]

It comes with a ring homomorphism \(R \to R[X]/(f)\) sending a constant to its class, and with a distinguished element \(\alpha\), the class of \(X\). Every element is the class of some polynomial, and two polynomials have the same class exactly when \(f\) divides their difference. Since \(f\) itself has class zero, \(\alpha\) is a root of \(f\), where the coefficients of \(f\) are read in the new ring.

When \(R = K\) is a field, \(K[X]/(f)\) is a field if and only if \(f\) is irreducible: in a principal ideal domain that is not a field, such as \(K[X]\), the ideal \((f)\) is maximal exactly when \(f\) is irreducible. For irreducible \(f\) the field \(K[X]/(f)\) is the rupture field of \(f\), and \(K\) embeds in it, since a ring homomorphism out of a field is injective.

Examples
  • Over the real numbers, \(X^2 + 1\) is irreducible, and \(\mathbb{R}[X]/(X^2+1)\) is isomorphic to the complex numbers, with \(\alpha\) corresponding to \(i\).
  • Over the field with two elements, \(X^2 + X + 1\) has degree \(2\) and no root, so it is irreducible, and its rupture field is a field with four elements.
  • Over \(\mathbb{Q}\), the polynomial \(X^3 - 2\) is irreducible by Eisenstein's criterion. Its rupture field is isomorphic to \(\mathbb{Q}(\sqrt[3]{2})\), a subfield of \(\mathbb{R}\). The other two complex roots of \(X^3 - 2\) are not real, so \(X^3 - 2\) does not split in this field: a rupture field need not be a splitting field.
  • If \(f = X^2\) over a field \(K\), the quotient \(K[X]/(X^2)\) is the ring of dual numbers. Here \(\alpha \neq 0\) but \(\alpha^2 = 0\), so the quotient is not a field, matching the reducibility of \(X^2\).
  • For an element \(r\) of a commutative ring \(R\), adjoining a root of \(rX - 1\) makes \(r\) invertible, with inverse \(\alpha\).
Properties

Let \(K\) be a field and \(f\) a nonzero polynomial of degree \(d\) over \(K\), and write \(\alpha\) for the class of \(X\) in \(L = K[X]/(f)\).

Over a general commutative ring the quotient behaves less uniformly. If \(f\) is monic of degree \(d\), then \(R[X]/(f)\) is a free \(R\)-module with basis \(1, \alpha, \dots, \alpha^{d-1}\). If \(R\) is an integral domain and \(f\) is not a nonzero constant, the map from \(R\) to \(R[X]/(f)\) is injective, and if \(f\) is a prime element of \(R[X]\), the quotient is an integral domain.

A splitting field of \(f\) is obtained by repeatedly adjoining a root of an irreducible factor of what remains of \(f\); the rupture field is the first step of that process. By the primitive element theorem, every finite separable extension is generated by one element, so it is a rupture field of that element's minimal polynomial. Adjoining a root of \(rX - 1\) is one way to build the localization of a ring at the powers of \(r\).

In Mathlib

Mathlib does not define rupture fields separately. Its construction works for an arbitrary polynomial over an arbitrary commutative ring, as the quotient by the ideal generated by \(f\), with no irreducibility assumed. When the base is a field and irreducibility of \(f\) is supplied as a standing fact, the quotient carries a field structure. Results about bases, degree and minimal polynomials do not use this standing fact and need only that \(f\) is nonzero; the dimension formula holds even for \(f = 0\), because the quotient is then infinite-dimensional, whose dimension Mathlib records as \(0\), and the natural-number degree of the zero polynomial is also \(0\). Separately, Mathlib has a structure recording that a given ring is presented as \(R[X]/(f)\), through a surjective algebra map from \(R[X]\) whose kernel is the ideal generated by \(f\); this lets results about the construction apply to rings that are only isomorphic to it.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibAdjoinRoot
Uses 4 · Used by 2
Statement usesField · Polynomial in one indeterminate · Quotient ring · Irreducible element
Used byExistence of algebraic closure of a field · Splitting field

DefinitionSplitting field#

A splitting field of a polynomial \(f\) over a field \(K\) is a field extension of \(K\) in which \(f\) factors completely into linear factors and which is generated over \(K\) by the roots of \(f\). Every polynomial has one, and any two are isomorphic over \(K\), so one may speak of "the" splitting field. Splitting fields are the extensions in which the roots of a polynomial can all be handled at once, which makes them the basic objects of Galois theory: the finite normal extensions are exactly the splitting fields, and the Galois group of a polynomial is the group of automorphisms of its splitting field over \(K\).

Definition

Let \(L\) be a field extension of \(K\). A polynomial \(f \in K[X]\) splits over \(L\) if, viewed in \(L[X]\), it is a constant times a product of linear factors; equivalently, \(f\) equals its leading coefficient times a product of factors \(X - a_i\), and also equivalently, for nonzero \(f\), the number of roots of \(f\) in \(L\), counted with multiplicity, equals its degree. Separately, the zero polynomial counts as split over every field.

The extension \(L\) is a splitting field of \(f\) if \(f\) splits over \(L\) and \(L\) is generated over \(K\) by the roots of \(f\). If \(f\) has roots \(a_1, \dots, a_n\) in \(L\), the second condition says \(L = K(a_1, \dots, a_n)\); no proper subfield of \(L\) containing \(K\) is a field over which \(f\) splits. Starting from any extension \(M\) over which \(f\) splits, the subfield of \(M\) generated over \(K\) by the roots of \(f\) is a splitting field of \(f\).

Existence

A splitting field of \(f\) can always be constructed, by induction on the degree. If \(f\) has positive degree, choose an irreducible factor \(g\) of \(f\) and pass to the rupture field \(K[X]/(g)\), in which the class of \(X\) is a root of \(g\) and hence of \(f\). Over this larger field, \(f\) has a linear factor; dividing it out leaves a polynomial of smaller degree, to which the induction applies. After at most \(\deg f\) steps one reaches an extension over which \(f\) splits, and the field built this way is a splitting field of \(f\). Since each step has degree at most the current degree of the polynomial, a splitting field of a polynomial of degree \(n \ge 1\) has degree at most \(n!\) over \(K\).

Examples
  • Over \(\mathbb{Q}\), the polynomial \(X^2 - 2\) has splitting field \(\mathbb{Q}(\sqrt 2)\), of degree \(2\). Over \(\mathbb{R}\), the polynomial \(X^2 + 1\) has splitting field \(\mathbb{C}\).
  • The roots of \(X^3 - 2\) over \(\mathbb{Q}\) are \(\sqrt[3]{2}\), \(\omega\sqrt[3]{2}\) and \(\omega^2\sqrt[3]{2}\), where \(\omega\) is a primitive cube root of unity. The splitting field is \(\mathbb{Q}(\sqrt[3]{2}, \omega)\), of degree \(6 = 3!\), so the bound above can be attained. The field \(\mathbb{Q}(\sqrt[3]{2})\), of degree \(3\), contains one root but is not a splitting field, since it lies inside \(\mathbb{R}\) and the other two roots do not.
  • Let \(n \ge 1\). If an extension \(L\) of \(K\) contains a primitive \(n\)-th root of unity \(\zeta\) and \(L = K(\zeta)\) (equivalently, \(L\) is generated over \(K\) by the \(n\)-th roots of unity, which is how Mathlib phrases the hypothesis), then \(L\) is a splitting field of \(X^n - 1\), since the roots of \(X^n - 1\) are the powers of \(\zeta\).
  • If \(K\) is a finite field with \(q\) elements and \(F\) is a subfield of \(K\), then \(K\) is a splitting field of \(X^q - X\) over \(F\), because every element of \(K\) is a root of this polynomial and it has no other roots.
Properties
Finite fields

For a prime \(p\) and a positive integer \(n\), the splitting field of \(X^{p^n} - X\) over \(\mathbb{Z}/p\mathbb{Z}\) is a finite field that has exactly \(p^n\) elements: the polynomial has derivative \(-1\), so its \(p^n\) roots are distinct, and they already form a field. Conversely, a field \(K\) with \(p^n\) elements, regarded as an algebra over \(\mathbb{Z}/p\mathbb{Z}\) (as every field of characteristic \(p\) is), is a splitting field of \(X^{p^n} - X\), so by uniqueness it is isomorphic to the splitting field constructed above. Hence any two fields with \(p^n\) elements are isomorphic.

An algebraic closure of \(K\) is an algebraically closed algebraic extension; it plays the role of a splitting field for all polynomials over \(K\) at once, and contains a copy of the splitting field of each one. The rupture field of an irreducible polynomial adjoins only one root and is in general smaller than the splitting field. The primitive element theorem shows that the splitting field of a separable polynomial is generated by a single element.

In Mathlib

Mathlib separates the property from the construction. Being a splitting field is a predicate on a field extension \(L\) of \(K\): the polynomial splits over \(L\), and \(L\) is generated by the roots as a \(K\)-algebra, which is the same as being generated as a field because the roots are algebraic; an equivalent form uses the subfield generated by the roots. Splitting is defined for polynomials over any semiring, as being a product of constants and monic linear polynomials, so the zero polynomial splits and its splitting field is \(K\) itself. The construction is a specific field, built by repeatedly adjoining a root of an irreducible factor and then rewritten as a quotient of a multivariate polynomial ring over \(K\), so that it carries well-behaved algebraic structure. Results are mostly stated for an arbitrary field satisfying the predicate, and the constructed field supplies existence. The field with \(p^n\) elements is defined in this way, as the constructed splitting field of \(X^{p^n} - X\) over \(\mathbb{Z}/p\mathbb{Z}\).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPolynomial.SplittingField
Uses 5 · Used by 3
Statement usesField · Polynomial in one indeterminate · Roots of a polynomial
Proof usesIrreducible element · Rupture field
Used byAbel-Ruffini theorem (one direction) · Existence of algebraic closure of a field · Primitive element theorem

DefinitionPerfect closure#

The perfect closure of a commutative ring \(K\) of prime characteristic \(p\) is the ring obtained from \(K\) by formally adjoining a \(p\)-th root, a \(p^2\)-th root, and so on, of every element; along the way every nilpotent element of \(K\) is sent to \(0\). It is the most economical way to make the Frobenius morphism \(x \mapsto x^p\) bijective: it is a perfect ring that receives a map from \(K\), and every ring homomorphism from \(K\) into a perfect ring of characteristic \(p\) extends to it in exactly one way. For a field it gives a perfect field containing \(K\), over which every irreducible polynomial is separable.

Definition

Fix a prime \(p\). A commutative ring of characteristic \(p\) is called perfect when its \(p\)-th power map is bijective, so that every element has exactly one \(p\)-th root.

Let \(K\) be a commutative ring of characteristic \(p\). A pair \((n, x)\) with \(n \ge 0\) an integer and \(x \in K\) is meant to stand for the formal root \(x^{1/p^n}\). Since \(x^{1/p^n}\) and \((x^p)^{1/p^{n+1}}\) ought to be the same element, the perfect closure \(K^{\mathrm{perf}}\) is the set of pairs modulo the equivalence relation generated by

\[(n, x) \sim (n+1, x^p).\]

Every element of \(K^{\mathrm{perf}}\) is the class of some pair. The ring operations bring two roots to a common level: the product of the classes of \((m, x)\) and \((n, y)\) is the class of \((m+n,\, x^{p^n} y^{p^m})\), and their sum is the class of \((m+n,\, x^{p^n} + y^{p^m})\); the sum formula is correct because the Frobenius morphism is additive. With these operations \(K^{\mathrm{perf}}\) is a commutative ring of characteristic \(p\), and sending \(x\) to the class of \((0, x)\) is a ring homomorphism \(K \to K^{\mathrm{perf}}\).

Two pairs \((m, x)\) and \((n, y)\) define the same element exactly when \(x^{p^{n+k}} = y^{p^{m+k}}\) for some \(k \ge 0\). If \(K\) has no nonzero nilpotent elements, the Frobenius morphism of \(K\) is injective and one may take \(k = 0\).

Properties
Examples
  • If \(K\) is already perfect, for instance a finite field, the map \(K \to K^{\mathrm{perf}}\) is an isomorphism: the class of \((n, x)\) equals the image of the \(p^n\)-th root of \(x\) in \(K\).
  • For the field of rational functions \(\mathbb{F}_p(t)\), which is not perfect because \(t\) has no \(p\)-th root, the perfect closure is the union, inside an algebraic closure of \(\mathbb{F}_p(t)\), of the increasing chain of fields \(\mathbb{F}_p(t^{1/p^n})\) for \(n \ge 0\).
  • For the polynomial ring \(\mathbb{F}_p[t]\), the perfect closure is the ring of polynomial expressions in \(t\) whose exponents are nonnegative rational numbers with a power of \(p\) as denominator.
  • In \(\mathbb{F}_p[x]/(x^p)\) the class of \(x\) is nilpotent, so it maps to \(0\), and the perfect closure is \(\mathbb{F}_p\).
Perfect closures in general

The universal property determines \(K^{\mathrm{perf}}\) up to unique isomorphism, and there is an intrinsic test for it. Call a ring homomorphism \(i \colon K \to L\) into a perfect ring \(L\) of characteristic \(p\) a perfect closure of \(K\) when every element of \(L\) has some \(p^n\)-th power in the image of \(i\), and every element of the kernel of \(i\) has some \(p^n\)-th power equal to \(0\). The homomorphism \(K \to K^{\mathrm{perf}}\) satisfies both conditions. For any perfect closure, the kernel of \(i\) is exactly the \(p\)-nilradical of \(K\), the ideal of elements with some \(p^n\)-th power equal to \(0\), which for prime \(p\) is the nilradical of \(K\). If \(i \colon K \to L\) and \(j \colon K \to M\) are two perfect closures, then \(L\) and \(M\) are isomorphic as rings, by an isomorphism that carries \(i\) to \(j\).

For fields there is also a relative version. If \(E\) is an extension field of \(F\), the relative perfect closure of \(F\) in \(E\) consists of the elements of \(E\) having some \(p^n\)-th power in \(F\), where \(F\) has characteristic \(p\). It is an intermediate field, and an intermediate field lies inside it exactly when it is purely inseparable over \(F\), so it is the largest purely inseparable subextension. When \(E\) is perfect, for example an algebraic closure of \(F\), the relative perfect closure is a perfect field, and it is then a perfect closure of \(F\) in the sense above.

The perfection of a ring of characteristic \(p\) is the dual construction: instead of adjoining \(p\)-th roots, its elements are the compatible sequences \((x_0, x_1, x_2, \dots)\) of elements of the ring with \(x_{n+1}^p = x_n\) for all \(n\), and it is the universal perfect ring mapping to the given ring rather than from it.

In Mathlib

Mathlib constructs the perfect closure for any commutative ring whose characteristic is a prime \(p\), with \(p\) given explicitly. It is the quotient of the set of pairs by the relation that joins each \((n, x)\) to \((n+1, x^p)\), and equality is then governed by the equivalence relation this generates. The structures of commutative ring, field and perfect ring are supplied separately, the field structure only when the input is a field. The general notion of a perfect closure is phrased with the exponential characteristic, which is \(1\) in characteristic zero; with that convention a perfect closure of a ring of characteristic zero is the same as an isomorphism. A perfect ring is defined by bijectivity of the \(p\)-th power map, and the relative perfect closure is defined for every field extension, using the exponential characteristic of the base field, so that in characteristic zero it is just the base field.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPerfectClosure
Uses 5
Statement usesRing · Characteristic p · Frobenius morphism · Ring morphism · Field

DefinitionGalois correspondence#

The Galois correspondence, also called the fundamental theorem of Galois theory, says that for a finite Galois extension of fields \(E/F\) the intermediate fields of the extension are in one-to-one, inclusion-reversing correspondence with the subgroups of its Galois group. It turns questions about fields, which can be infinite and hard to enumerate, into questions about a finite group, and it is the basis of the classical applications of Galois theory, such as the insolvability of the general quintic by radicals.

Statement

Let \(E/F\) be a field extension. Its Galois group \(\mathrm{Gal}(E/F)\) is the group of field automorphisms of \(E\) that fix every element of \(F\). The extension is Galois if it is normal and separable: every element of \(E\) is algebraic over \(F\), and its minimal polynomial over \(F\) splits into linear factors in \(E\) and has no repeated roots. For an extension of finite degree, being Galois is equivalent to each of: the elements of \(E\) fixed by all of \(\mathrm{Gal}(E/F)\) are exactly those of \(F\); the group has exactly \([E:F]\) elements, where the degree \([E:F]\) is the dimension of \(E\) as a vector space over \(F\); \(E\) is the splitting field of a separable polynomial over \(F\).

To a subgroup \(H\) of \(\mathrm{Gal}(E/F)\) attach its fixed field \(E^H = \{x \in E : \sigma(x) = x \text{ for all } \sigma \in H\}\), and to an intermediate field \(F \subseteq K \subseteq E\) attach the subgroup of automorphisms fixing \(K\) pointwise, which is isomorphic to \(\mathrm{Gal}(E/K)\) and is denoted that way. For any extension, \(K \subseteq E^H\) holds exactly when \(H \subseteq \mathrm{Gal}(E/K)\), so both maps reverse inclusions.

Theorem. If \(E/F\) is a finite Galois extension, then \(K \mapsto \mathrm{Gal}(E/K)\) and \(H \mapsto E^H\) are mutually inverse, inclusion-reversing bijections between the intermediate fields of \(E/F\) and the subgroups of \(\mathrm{Gal}(E/F)\). Moreover, if \(K\) corresponds to \(H\), then

\[|H| = [E:K], \qquad [K:F] = [\mathrm{Gal}(E/F) : H].\]

Both formulas are in Mathlib (the first, the second); the right-hand side of the second is the index of \(H\). Finally, \(K\) is Galois over \(F\) if and only if \(H\) is a normal subgroup of \(\mathrm{Gal}(E/F)\), and in that case restriction to \(K\) induces an isomorphism from the quotient group \(\mathrm{Gal}(E/F)/H\) onto \(\mathrm{Gal}(K/F)\).

Examples
  • A biquadratic field. Let \(E = \mathbb{Q}(\sqrt2, \sqrt3)\), the splitting field of \((x^2-2)(x^2-3)\) over \(\mathbb{Q}\), of degree \(4\). Its Galois group has four elements: the identity, \(\sigma\) sending \(\sqrt2\) to \(-\sqrt2\) and fixing \(\sqrt3\), \(\tau\) sending \(\sqrt3\) to \(-\sqrt3\) and fixing \(\sqrt2\), and \(\sigma\tau\). It has five subgroups, and the correspondence pairs them with five fields: the trivial group with \(E\), \(\{1, \sigma\}\) with \(\mathbb{Q}(\sqrt3)\), \(\{1, \tau\}\) with \(\mathbb{Q}(\sqrt2)\), \(\{1, \sigma\tau\}\) with \(\mathbb{Q}(\sqrt6)\), and the whole group with \(\mathbb{Q}\). The group is abelian, so every intermediate field is Galois over \(\mathbb{Q}\).
  • A cubic. Let \(E = \mathbb{Q}(\sqrt[3]{2}, \omega)\) with \(\omega\) a primitive cube root of unity, the splitting field of \(x^3 - 2\). It has degree \(6\), and its Galois group permutes the three roots \(\sqrt[3]{2}, \omega\sqrt[3]{2}, \omega^2\sqrt[3]{2}\) as the full symmetric group \(S_3\). The three subgroups of order \(2\) correspond to the cubic fields \(\mathbb{Q}(\omega^i\sqrt[3]{2})\), none of them Galois over \(\mathbb{Q}\), matching the fact that these subgroups are not normal. The normal subgroup of order \(3\) corresponds to the quadratic field \(\mathbb{Q}(\omega) = \mathbb{Q}(\sqrt{-3})\), which is Galois.
Properties
Proof

The two halves use different hypotheses. Let \(H\) be a subgroup of \(\mathrm{Gal}(E/F)\) with \(E/F\) finite. Every element of \(H\) fixes \(E^H\), so \(H \subseteq \mathrm{Gal}(E/E^H)\). A finite extension has at most as many automorphisms as its degree; applied to \(E/E^H\), which is finite because \(E/F\) is, this bounds \(|\mathrm{Gal}(E/E^H)|\) by \([E:E^H]\). Artin's theorem gives \([E:E^H] = |H|\), so \(\mathrm{Gal}(E/E^H)\) has at most \(|H|\) elements and equals \(H\). This half needs no Galois hypothesis.

Conversely, let \(K\) be an intermediate field. Clearly \(K \subseteq E^{\mathrm{Gal}(E/K)}\). Since \(E\) is Galois over \(F\), it is also Galois over \(K\), so \(|\mathrm{Gal}(E/K)| = [E:K]\) (the count for Galois extensions). By Artin's theorem \(E\) has the same degree \([E:K]\) over the larger field \(E^{\mathrm{Gal}(E/K)}\), and the tower law forces the two fields to be equal: \(K\) is the fixed field of \(\mathrm{Gal}(E/K)\). The two maps are therefore inverse, and they reverse inclusions.

Generalizations

For a Galois extension of infinite degree, every intermediate field is still the fixed field of its subgroup, but in general not every subgroup arises this way. The Galois group carries a natural profinite topology, the Krull topology, and intermediate fields correspond bijectively to the closed subgroups.

For an arbitrary extension the two maps still form a Galois connection between ordered sets, as the inclusion criterion in the statement shows; for an extension of finite degree, the Galois condition is what makes them inverse bijections. Among the uses of the correspondence is the theorem that a polynomial solvable by radicals has a solvable Galois group.

In Mathlib

Mathlib packages the correspondence as an order isomorphism between the lattice of intermediate fields and the order dual of the lattice of subgroups of the Galois group, which records in one object that the two maps are inverse and reverse inclusions. The subgroup attached to an intermediate field \(K\) is a subgroup of \(\mathrm{Gal}(E/F)\), not the group \(\mathrm{Gal}(E/K)\) itself; a separate isomorphism identifies the two. A Galois extension is defined as a normal and separable one, with no finiteness condition, and separability includes algebraicity, so finite degree is a separate hypothesis wherever the theorem needs it. Several statements hold more generally than the textbook version: the degree formula \([K:F] = [\mathrm{Gal}(E/F):H]\) and the equivalence between normal subgroups and Galois subextensions are proved for Galois extensions of any degree, with the convention that the degree of an infinite extension and the index of an infinite-index subgroup are both \(0\).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibIsGalois.intermediateFieldEquivSubgroup
Uses 6
Statement usesAlgebraic extension · Minimal polynomial · Finite-dimensionality · Index of a subgroup · Normal subgroup · Quotient group

TheoremAbel-Ruffini theorem (one direction)#

The Abel–Ruffini theorem, in the direction treated here, says that if an element of a field extension can be built from the base field by the field operations and the extraction of \(n\)-th roots, then the Galois group of its minimal polynomial is a solvable group. It is the half of Galois's criterion for solvability by radicals that serves as an obstruction: to show that a polynomial has a root that no formula in radicals can express, it suffices to show that its Galois group is not solvable. This is how one proves that there is no general formula in radicals for equations of degree five or more.

Statement

Let \(E\) be a field containing a field \(F\). The elements of \(E\) that are solvable by radicals over \(F\) form the smallest intermediate field of \(E/F\) closed under taking roots: the smallest field \(K\) with \(F \subseteq K \subseteq E\) such that whenever \(x \in E\) and \(x^n \in K\) for some \(n \ge 1\), \(x\) itself lies in \(K\). Equivalently, \(x\) is solvable by radicals when it is reached from elements of \(F\) by finitely many additions, subtractions, multiplications, divisions and extractions of \(n\)-th roots inside \(E\). Every such element is a root of a monic polynomial with coefficients in \(F\), so it has a minimal polynomial over \(F\).

The Galois group \(\mathrm{Gal}(p)\) of a polynomial \(p\) over \(F\) is the group of automorphisms of its splitting field that fix \(F\) (see splitting field). A group \(G\) is solvable if its derived series \(G \supseteq [G,G] \supseteq [[G,G],[G,G]] \supseteq \cdots\) reaches the trivial group after finitely many steps; equivalently, \(G\) has a finite chain of subgroups from \(\{e\}\) to \(G\), each normal in the next with an abelian quotient.

Theorem. If \(x \in E\) is solvable by radicals over \(F\), then the Galois group of the minimal polynomial of \(x\) over \(F\) is solvable.

Since an irreducible polynomial is a constant multiple of the minimal polynomial of each of its roots, an equivalent form reads: if an irreducible polynomial \(q\) over \(F\) has a root in \(E\) that is solvable by radicals, then \(\mathrm{Gal}(q)\) is solvable.

Examples
Proof

The argument uses the closure properties of solvable groups: subgroups and images under surjective homomorphisms of solvable groups are solvable, and an extension of a solvable group by a solvable group is solvable. Abelian groups, those in which all elements commute, are solvable.

Mathlib argues by induction on the way \(x\) is built. If \(x \in F\), its minimal polynomial is \(X - x\) and the group is trivial. For the other steps two facts about Galois groups of polynomials are used. First, the splitting field of \(pq\) is generated by the roots of \(p\) and of \(q\), so \(\mathrm{Gal}(pq)\) embeds in \(\mathrm{Gal}(p) \times \mathrm{Gal}(q)\) and is solvable when both factors are. Second, if \(p\) splits in the splitting field of \(q\), restriction maps \(\mathrm{Gal}(q)\) onto \(\mathrm{Gal}(p)\), so \(\mathrm{Gal}(p)\) is solvable whenever \(\mathrm{Gal}(q)\) is.

If \(x\) and \(y\) have minimal polynomials \(p\) and \(q\) with solvable Galois groups, let \(z\) be any element of \(F(x,y)\), for instance \(x \pm y\), \(xy\) or \(x/y\). An \(F\)-embedding of \(F(x,y)\) into the splitting field of \(pq\) sends \(z\) to an element with the same minimal polynomial; that splitting field is normal over \(F\), so the minimal polynomial of \(z\) splits there and the second fact applies. Negatives and inverses therefore need no separate step, and indeed a property that holds for the elements of \(F\) and is preserved by sums, products and \(n\)-th roots holds for every element solvable by radicals. If \(x^n\) has minimal polynomial \(p\) with solvable Galois group, the minimal polynomial of \(x\) divides \(p(X^n)\), and it remains to see that \(\mathrm{Gal}(p(X^n))\) is solvable. Over the splitting field \(K\) of \(p\), the polynomial \(p(X^n)\) is, up to a constant factor, a product of factors \(X^n - c\), whose Galois groups are solvable. The Galois group of \(X^n - 1\) is abelian, because each automorphism raises every \(n\)-th root of unity to one fixed power; over the splitting field of \(X^n - 1\), for \(c \ne 0\), each automorphism multiplies a root of \(X^n - c\) by an \(n\)-th root of unity lying in the base, which again gives an abelian group. For \(c \ne 0\), \(X^n - 1\) splits in every field in which \(X^n - c\) splits, since dividing the roots of \(X^n - c\) by one of them gives the roots of \(X^n - 1\); so the splitting field of \(X^n - 1\) lies inside that of \(X^n - c\), and the tower property below combines the two abelian groups. Finally, if \(K\) is normal over \(F\) and the automorphism groups of \(K/F\) and \(L/K\) are solvable, so is that of \(L/F\), which assembles the pieces.

Over a field \(F\) of characteristic zero the converse also holds, provided the roots are taken in a large enough field, such as an algebraic closure of \(F\) in the role of \(E\): if the Galois group of an irreducible polynomial over \(F\) is solvable, its roots in an algebraic closure of \(F\) are solvable by radicals there. The choice of \(E\) matters. The polynomial \(X^3 - 3X + 1\) over the rationals has a cyclic Galois group of order \(3\), yet its three real roots cannot be expressed by radicals inside the real numbers, so with \(E = \mathbb{R}\) they are not solvable by radicals. Together the two directions form Galois's criterion. The Galois correspondence underlies the textbook proof, which translates a tower of radical extensions into a chain of subgroups with abelian quotients.

In Mathlib

Mathlib defines the elements solvable by radicals as an intermediate field, the smallest one closed under \(n\)-th roots for every \(n \ge 1\), rather than through explicit towers of radical extensions. The Galois group of a polynomial is the full group of automorphisms of its splitting field over \(F\), defined for every polynomial, separable or not, and always finite. With these conventions the theorem holds over every field, with no assumption on the characteristic, whereas many textbook treatments assume characteristic zero. The theorem is stated for an arbitrary extension field \(E\) of \(F\), and the minimal polynomial is taken over \(F\).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibisSolvable_gal_minpoly
Uses 7 · Used by 1
Statement usesField · Group · Minimal polynomial · Splitting field · Irreducible element · Normal subgroup
Proof usesDirect product of groups
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.