A statement-level formalisation in Lean 4 of compatible families of λ-adic Galois
representations and of the companion-existence statement of Lafforgue's theorem
for curves. Five supporting lemmas are proved; the companion theorem is stated
and deliberately left sorry (Lean's marker for a statement admitted without
proof); the family over all coefficient places follows from it by the axiom of
choice.
A secondary purpose is to establish precisely which ingredients Mathlib v4.28.0 supports and which it does not.
Drafted with LLM assistance; I audited the statements against Mathlib v4.28.0 source and the citations against the primary literature. AUDIT.md records the Mathlib survey, the errors corrected, and the claims that remain unverified.
Fix a finite field 𝔽_q of characteristic p; a function field K over 𝔽_q
with algebraic closure K̄ and absolute Galois group G_K = Gal(K̄/K), carrying
the Krull topology; a Dedekind domain A which is a finite-type 𝔽_q-algebra
with fraction field K, so that Spec A is a smooth affine curve over 𝔽_q and
the height-one primes of A are its closed points, all but finitely many of the
places of K; a number field E of coefficients, with λ ranging over its
finite places, completion E_λ and residue characteristic ℓ(λ); a finite set
S of places of A; an integer n; and a choice of Frobenius element
Frob_v ∈ G_K at each place v.
A family (ρ_λ) of continuous homomorphisms ρ_λ : G_K → GL_n(E_λ) is a
compatible family unramified outside S if for every v ∉ S there is a
polynomial P_v ∈ E[T] such that for every λ with v ∤ ℓ(λ), the
representation ρ_λ is unramified at v and the characteristic polynomial of
ρ_λ(Frob_v) is the image of P_v. The polynomial is chosen before λ, not
after; that quantifier order is the content of the definition.
The companion theorem, as formalised here, reads as follows. Let n ≥ 1 and
ℓ(λ₀) ≠ p, and let ρ₀ : G_K → GL_n(E_{λ₀}) be continuous, absolutely irreducible, of
finite-order determinant, unramified at every v ∉ S, and such that the
characteristic polynomial of ρ₀(Frob_v) is the image of P_v for a fixed
family P_v ∈ E[T]. Then for every finite place λ of E with ℓ(λ) ≠ p there
exist a finite extension M/E_λ and a continuous ρ : G_K → GL_n(M), unramified
at every v ∉ S, whose characteristic polynomial at Frob_v is the image of the
same P_v under E → E_λ → M, and which is itself absolutely irreducible with
determinant of finite order.
The statement is made one place λ at a time. A family indexed by all λ
follows by choice, and exists_companion_family is that derivation.
This is the companion-existence part of Lafforgue's Theorem VII.6, not the
whole of it: clause (v) gives the companion and its coefficient field, and the
companion's finite-order determinant is carried from the construction in the
proof, though it is in any case implied by the other conclusions together with
the finite-order hypothesis on ρ₀, by the same Chebotarev density and
continuity of the determinant used in the degree-bound remark. VII.6 starts from an irreducible lisse sheaf with finite-order
determinant and constructs E and the P_v, which are hypotheses here; it also proves
purity, unit-ness of the Frobenius roots away from p with slope bounds at the
places over p, and a further statement descending the n-fold direct sum of the companion to E_λ itself. In
the other direction, the curve here is the affine Spec A with S removed,
where VII.6 treats a smooth curve as an open subscheme of a projective one.
M carries the E_λ-module topology, via Mathlib's IsModuleTopology, rather than an arbitrary one; that pins which continuity is being asserted. For a finite
extension of the complete field E_λ it is the canonical valuation topology, so
the degenerate reading in which every map is continuous is excluded.
Three things hold but are not stated in the Lean. The extension M can be taken
of a specific degree: Drinfeld's Lemma 2.7 (arXiv:1007.4004) is an elementary
Brauer-group argument showing that a semisimple representation of dimension n
over an algebraic closure of E_λ whose character is defined over E_λ descends
to any extension whose degree is divisible by each of n, n-1, …, 2. Its
hypothesis is met, since the companion is irreducible and its character is
defined over E_λ: the Frobenius traces lie in E ⊆ E_λ, the union of the
Frobenius conjugacy classes is dense by Chebotarev in the quotient through which
the companion factors, the trace is continuous and conjugacy-invariant, and E_λ
is closed in M. So [M : E_λ] = n! suffices, and is not claimed minimal.
Drinfeld's Theorem 1.1 carries a hypothesis that the roots of the characteristic
polynomials are λ-adic units. For curves that is a consequence rather than an
extra assumption: unramifiedness on the curve makes the representation a lisse
sheaf there, and Lafforgue proves unit-ness for an irreducible lisse sheaf with
finite-order determinant. The mechanism is not purity. Being a unit away from
p is part (iii) of Deligne's Conjecture 1.2.10, where the label (c) is
Drinfeld's numbering in his abbreviated restatement rather than Deligne's. It is
a conclusion separate from the weight condition, which is part (i) there, and for
curves it is part (iii) of Lafforgue's Theorem VII.6. Purity is the archimedean statement and does not imply integrality:
(3 + 4i)/5 has absolute value 1 at every archimedean place and is not a
5-adic unit.
At λ₀ one may take M = E_{λ₀} and ρ = ρ₀, so ρ₀ is itself one of the
companions. No clause asserting this is needed or stated, since once the
coefficient field varies an equality ρ_{λ₀} = ρ₀ is type-inappropriate.
charpoly_eq_of_isConj_gl and charpoly_eq_of_isConj: the characteristic
polynomial of ρ(g) depends only on the conjugacy class of g. This is not the
well-definedness fact behind the compatibility condition; see below.
isFrobAt_conj: conjugates of a Frobenius element at v are again Frobenius
elements at v, from IsArithFrobAt.conj.
toHom_eq_of_isArithFrobAt: if ρ is unramified at v and g, g' are
Frobenius elements at the same prime Q above v, then ρ g = ρ g'. The
argument runs through inertia, since IsArithFrobAt.mul_inv_mem_inertia gives
g * g'⁻¹ ∈ inertia Q, which ρ kills.
charpoly_eq_of_isArithFrobAt: the corresponding statement for characteristic
polynomials.
exists_companion_family: the family indexed by all λ away from the
characteristic, obtained from exists_companion by choice. Proved, but it
inherits that theorem's sorry.
IsFrobAt is a definition, not an axiom. It is built on Mathlib's
IsArithFrobAt via the action of G_K on the integral closure of A in K̄,
which Mathlib supplies, as it does the SMulCommClass that action needs. Nothing
obstructs defining arithmetic Frobenius at the infinite level, since
IsArithFrobAt is stated for monoid actions and needs no finiteness. Existence
of Frobenius elements is a separate matter, treated under Limitations.
Both the hypothesis on ρ₀ and the conclusion about the companion need absolute
irreducibility. Formalising that naively means constructing an algebraic closure
of E_λ, giving it a topology, and base-changing the representation, none of
which Mathlib v4.28.0 makes cheap.
The slice avoids all of it. SpanFull ρ says that the R-linear span of the
image of ρ is the whole matrix algebra M_n(R). For R a field and n ≥ 1
this is equivalent to absolute irreducibility, by an argument short enough to
state here. The image contains 1 and is closed under multiplication, so its
span is already an R-subalgebra; if that span is M_n(R) it remains full after
any scalar extension, so there is no proper nonzero invariant subspace over any
extension field. Conversely, if ρ is absolutely irreducible then Burnside's
theorem over an algebraic closure R̄ gives a span of dimension n², and the
span over R̄ is R̄ ⊗_R the span over R, so the span over R already has
dimension n².
The equivalence is not formalised; it is what justifies the choice of predicate,
which applies unchanged to the companion over M.
These are out of scope.
Frobenius existence is assumed, not proved. FrobeniusChoice takes it as data.
IsArithFrobAt.exists_of_isInvariant fails here on three counts: it requires a
finite residue field at the chosen prime, which at K̄ is the algebraic closure
of A/v; a finite acting group; and Algebra.IsInvariant. Proving existence needs surjectivity of the decomposition group onto the
residue Galois group together with an inverse-limit argument; Mathlib v4.28.0
has both at the profinite level, under an invariance hypothesis that fails for
the integral closure in K̄, and the derivation is not carried out here. Every result mentioning FrobeniusChoice is conditional on it.
IsFrobAt silently entails a finite residue field. Mathlib defines
IsArithFrobAt by g · x ≡ x ^ #(A/v) (mod Q) with # read as Nat.card. If
A/v were infinite that cardinal is 0, the congruence at x = 0 forces
1 ∈ Q, and primality fails. So there is no degenerate reading, but
FrobeniusChoice is uninhabited for any A with an infinite residue field, and
every result taking one is then vacuously true.
Frobenius independence is proved only at a fixed prime. Comparing Frobenius
elements at different primes above v needs transitivity of the G_K-action on
those primes, which is not available here.
There is no descent to E_λ for the given E: the companion lands in a finite
extension M/E_λ. The obstruction is the class
of a central simple algebra in Br(E_λ), the algebra Lafforgue's proof of
VII.6(v) works with; no explicit counterexample is cited here. Removing it by
enlarging E is Chin, Independence of ℓ in Lafforgue's theorem, Adv. Math. 180
(2003), 64–86, which Drinfeld cites for exactly this step, and is not formalised
here.
HeightOneSpectrum A indexes an affine model: U = Spec A with S removed is a smooth affine curve
and Lafforgue's theorem applies to it, up to one change of convention: the
Frobenius used here is arithmetic, where Lafforgue writes the characteristic
polynomials for geometric Frobenius, its inverse, and the two determine each
other. What follows from it is that the
places of a proper model outside Spec A are not points of U, so "unramified
outside S" says nothing about them, and the group here is not π₁^ét(X ∖ S)
for projective X.
IsCompatibleFamily is the E_λ-valued notion. It is a legitimate definition
and is kept, but it is not what the companion theorem produces. IsIrred is
likewise kept as the E_λ-irreducibility notion, and is deliberately not the
hypothesis of exists_companion.
The main theorem is sorry. Formalising the proof is not in scope.
The slice is stated via G_K with an unramified-outside-S condition rather
than via π₁^ét(X ∖ S), because no π₁^ét(X) is available in Mathlib v4.28.0.
AUDIT.md records what the library has here and what is missing.
It is tempting to drop it. Continuity forces the image into a compact subgroup of
GL_n(E_λ), which stabilises a lattice, so the representation modulo each power
of the maximal ideal factors through a finite extension ramified at finitely many
places. That gives a finite ramification set at every finite level, but the
level-wise sets need not stabilise, and for n ≥ 2 they need not. For
ℓ ≠ char K, a Kummer class built from b_m = ∏_{i ≤ m} π_i^{ℓ^i}, with the places v_i and elements π_i chosen
inductively so that v_i(π_i) = 1 and v_i(π_j) = 0 for every j ≠ i, gives a
continuous upper-triangular ρ = (χ_ℓ, c; 0, 1) : G_K → GL₂(ℤ_ℓ) ramified at
every v_i; a block sum with the trivial representation extends this to every
n ≥ 2. Controlling the earlier π_j at v_i as well as the later ones is
what makes v_i(b_m) = ℓ^i exactly, which is nonzero mod ℓ^m for every
m > i. Ramakrishna,
Infinitely ramified Galois representations, Ann. of Math. 151 (2000), 793–815,
constructs over ℚ, for every prime ℓ ≥ 5 in a set of density one,
surjective GL₂(ℤ_ℓ)-valued representations ramified at infinitely many primes,
so even full image is compatible with infinite
ramification;
Khare–Rajan, Int. Math. Res. Not. 2001, no. 12, 601–607, show that for continuous
semisimple representations of the absolute Galois group of a number field the
ramified set has density zero while remaining possibly infinite, and remark that
the same holds over function fields when the coefficient residue characteristic
differs from the field characteristic. Semisimplicity is essential there; the
Kummer representations above are not semisimple. For n = 1 the claim is true,
since the torsion of 1 + 𝔪 is finite and class field theory closes the
argument.
The example settles continuity alone. It does not show the hypothesis independent
of the others: the representation displayed is reducible, so it fails SpanFull,
and its determinant χ_ℓ has infinite order. Whether continuity together with
absolute irreducibility and finite-order determinant forces finite ramification is
not settled here. The hypothesis is stated because nothing available establishes
that it can be dropped, which is also why finite ramification is an explicit
condition in the Fontaine–Mazur conjecture rather than a consequence of
continuity.
lake build kernel-checks the proofs that are given, accepting sorry as an
axiom; it does not verify that the definitions say what they are intended to
say. Every mathematical error listed in AUDIT.md was found in that gap. A sorry conceals the
difference: a statement that is unprovable because it is false looks exactly
like a statement that is unproved because the infrastructure is missing.
CI runs the build, checks the axiom profile of the declarations named in
Axioms.lean (the five lemmas admit none beyond the classical three, the two
theorems additionally sorryAx), and counts the source lines
consisting of sorry, requiring exactly one. AUDIT.md records what each check establishes and what it
misses.
The most self-contained is existence of Frobenius elements in the absolute Galois
group, which is missing from Mathlib. Beyond
that: coefficient-field descent, which would replace M by E_λ for a suitably
enlarged E; independence of ℓ for arithmetic monodromy groups, where Chin,
Independence of ℓ of monodromy groups, J. Amer. Math. Soc. 17 (2004), 723–747,
treats the neutral connected component, identifying it after enlarging E with
base changes of one connected split reductive E-group for a semisimple
compatible system pure of integer weight, and Drinfeld, On the pro-semisimple
completion of the fundamental group of a smooth variety over a finite field,
Adv. Math. 327 (2018), 708–788, treats the whole pro-semisimple object; and
Deligne's companion conjecture for smooth varieties in arbitrary dimension,
proved by Drinfeld.
Lean v4.28.0 and Mathlib v4.28.0, pinned exactly.
lake exe cache get && lake build
lake env lean Axioms.lean