Regular extensions of $\mathbb{Q}(t)$

Definition

MathieuM23_Regular

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

field-theoryinverse-galois-problemnumber-theory

Let $L$ be a field extension of the rational function field $\mathbb{Q}(t)$ . Then $L$ is regular (over $\mathbb{Q}$ ) if it contains no nontrivial algebraic extension of $\mathbb{Q}$ . That is, every $x\in L$ that is algebraic over $\mathbb{Q}$ already lies in $\mathbb{Q}$ .

Regularity is what lets Hilbert's irreducibility theorem specialize a regular $G$ -extension of $\mathbb{Q}(t)$ to infinitely many $G$ -extensions of $\mathbb{Q}$ .

Formalization Note "Algebraic over $\mathbb{Q}$ " is expressed as being a root of a nonzero polynomial $p\in\mathbb{Q}[X]$ , with $\mathbb{Q}$ acting on $L$ through $\mathbb{Q}\subset\mathbb{Q}(t)\to L$ . This avoids choosing a separate $\mathbb{Q}$ -algebra structure on $L$ .

Definition code

import Mathlib

/-! # Regular extensions of `ℚ(t)` (§1.2) -/

namespace MathieuM23

/-- An extension `L` of `ℚ(t)` is *regular* if it contains no nontrivial algebraic extension of
`ℚ`: every element of `L` that is a root of a nonzero polynomial with rational coefficients
already lies in (the image of) `ℚ`. -/
def IsRegularOverRatFunc (L : Type*) [Field L] [Algebra (RatFunc ℚ) L] : Prop :=
  ∀ x : L, (∃ p : Polynomial ℚ, p ≠ 0 ∧
      Polynomial.aeval x (p.map (algebraMap ℚ (RatFunc ℚ))) = 0) →
    ∃ q : ℚ, algebraMap (RatFunc ℚ) L (algebraMap ℚ (RatFunc ℚ) q) = x

end MathieuM23

Source

X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, *The Mathieu group M23 is a Galois group over Q*, arXiv:2608.08538v1 (2026), https://arxiv.org/abs/2608.08538, p. 2, §1.2 (definition of a regular extension)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), with full knowledge of the source paper and of the intended meaning. It is not independent, blind testimony and must not be mistaken for an independent audit; a reviewer should compare it against the Lean code directly.

Let $L$ be a field equipped with a ring homomorphism (algebra structure) $\iota:\mathbb{Q}(t)\to L$ , where $\mathbb{Q}(t)$ is the field of rational functions in one variable over $\mathbb{Q}$ . Write $j:\mathbb{Q}\to\mathbb{Q}(t)$ for the inclusion of constants. The property regular holds for $L$ when the following is true. For every $x\in L$ , if there exists a nonzero polynomial $p\in\mathbb{Q}[X]$ such that $x$ is a root of the polynomial obtained by applying $j$ to the coefficients of $p$ (evaluated in $L$ via $\iota$ ), then there is a rational number $q$ with $\iota(j(q))=x$ .

No finiteness, Galois or separability condition on $L/\mathbb{Q}(t)$ is part of this property.

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Regular extensions of Q(t)\mathbb{Q}(t)Q(t)

Regular extensions of $\mathbb{Q}(t)$