|
| 1 | +# Audit record |
| 2 | + |
| 3 | +`lake build` verifies that proofs are valid. It says nothing about whether the |
| 4 | +definitions mean what they claim. For a statement-level formalisation that gap is |
| 5 | +the entire risk, so this file records what Mathlib v4.28.0 could and could not |
| 6 | +supply, which errors were found in the course of the work, and which claims here |
| 7 | +are not machine-checked. |
| 8 | + |
| 9 | +## Mathlib v4.28.0 |
| 10 | + |
| 11 | +Everything below was verified by reading source at the pinned tag rather than |
| 12 | +from recall. Guessing a lemma's behaviour produced a wrong survey verdict early |
| 13 | +on, so nothing here is asserted from memory. |
| 14 | + |
| 15 | +Available: `krullTopology` on `Gal(L/K)`; `IsDedekindDomain.HeightOneSpectrum` |
| 16 | +and `.adicCompletion`; `GL`; `Matrix.charpoly` and `Matrix.charpoly_units_conj`; |
| 17 | +`RingTheory/Frobenius.lean`, whose `IsArithFrobAt` is stated for monoid actions |
| 18 | +with `SMulCommClass` and needs no finiteness; `Ideal.inertia`; |
| 19 | +`IsArithFrobAt.mul_inv_mem_inertia`; `IsArithFrobAt.conj`; |
| 20 | +`Topology/Algebra/Module/ModuleTopology.lean`, which is what makes a coefficient |
| 21 | +field finite over `E_λ` expressible with a pinned rather than an arbitrary |
| 22 | +topology; `Algebra.FiniteType`; and `CategoryTheory/Galois/` as an abstract |
| 23 | +development. |
| 24 | + |
| 25 | +Partial: `NumberTheory/FunctionField.lean` gives the predicate and the valuations |
| 26 | +but no tie-in to a curve. Unramifiedness predicates exist, but nothing for a |
| 27 | +representation. |
| 28 | + |
| 29 | +Missing: `π₁^ét(X)` for schemes, since the Galois-category development is |
| 30 | +abstract and the finite étale site is not instantiated as one. This decided the |
| 31 | +`G_K`-based formulation. Chebotarev density is absent entirely, as is |
| 32 | +characteristic-polynomial coefficient descent to `E`. The `MulSemiringAction` of |
| 33 | +`G_K` on the integral closure is supplied here. |
| 34 | + |
| 35 | +Three facts constrain the design. First, `IsArithFrobAt R g Q` unfolds to |
| 36 | +`∀ x, g • x - x ^ Nat.card (R ⧸ Q.under R) ∈ Q`. If the base residue ring were |
| 37 | +infinite that cardinal is `0`, the congruence at `x = 0` gives `1 ∈ Q`, and |
| 38 | +primality fails; so there is no degenerate `q = 0` reading, but a Frobenius |
| 39 | +choice is uninhabited whenever a residue field is infinite, and every result |
| 40 | +taking one is then vacuously true. Second, |
| 41 | +`IsArithFrobAt.exists_of_isInvariant` fails at the infinite level on three |
| 42 | +counts, not one: a finite residue field at the chosen prime, `[Finite G]`, and |
| 43 | +`[Algebra.IsInvariant R S G]`; existence of Frobenius elements in the absolute |
| 44 | +Galois group therefore has to be assumed as data. Third, |
| 45 | +`isPretransitive_of_isGaloisGroup` requires `[Finite G]` and |
| 46 | +`[IsGaloisGroup G A B]`, so transitivity of the action on primes above a place is |
| 47 | +unavailable, which is why Frobenius independence is proved only at a fixed prime. |
| 48 | + |
| 49 | +## Errors found and corrected |
| 50 | + |
| 51 | +All of the following compiled cleanly and passed `#print axioms`; they were found |
| 52 | +on further review of the definitions themselves, ordered here by severity. |
| 53 | + |
| 54 | +False statements. An axiom asserted that any two Frobenius elements at a place |
| 55 | +are conjugate; in fact two lifts at the same prime differ by an element of |
| 56 | +inertia. It was deleted and replaced by the correct inertia argument. The |
| 57 | +companion statement was false as first written, since a rank-one unramified |
| 58 | +character of the constant-field quotient has Frobenius eigenvalues outside `E`; |
| 59 | +irreducibility, finite-order determinant and `E`-rationality of the Frobenius |
| 60 | +characteristic polynomials are all required. Once those hypotheses were added the |
| 61 | +statement was still stronger than the theorem it named, in two independent ways: |
| 62 | +the conclusion placed companions over `E_λ` itself, where Lafforgue's theorem |
| 63 | +produces them over an algebraic closure and descent to `E_λ` for a fixed `E` is |
| 64 | +obstructed by the Schur index in `Br(E_λ)`; and the irreducibility hypothesis was |
| 65 | +irreducibility over `E_λ`, which is weaker than absolute irreducibility, so using |
| 66 | +it strengthened the theorem. Both had been filed as limitations, which reads as |
| 67 | +having proved less when the truth was that it asserted more. |
| 68 | + |
| 69 | +Vacuity. Frobenius existence was never actually assumed, since declaring a |
| 70 | +structure with an existence field does not assume it, so the compatibility |
| 71 | +condition could hold with no content; it is now passed as data. The base ring was |
| 72 | +an arbitrary Dedekind domain with the right fraction field, and fields and |
| 73 | +discrete valuation rings qualify, so the place set could be empty or a single |
| 74 | +point and the conclusion was satisfiable cheaply: the roots of the prescribed |
| 75 | +polynomial are `λ`-adic units, `GL_n(O_λ)` is profinite and `Ẑ` is procyclic, so |
| 76 | +a companion-matrix representation of the constant-field quotient satisfies |
| 77 | +everything. Requiring the base ring to be a finite-type algebra over the constant |
| 78 | +field makes its spectrum a smooth affine curve carrying cofinitely many of the |
| 79 | +places, and closes this. |
| 80 | + |
| 81 | +Misdescription. `charpoly_eq_of_isConj` was described as establishing |
| 82 | +well-definedness of the compatibility condition, which needs inertia rather than |
| 83 | +conjugacy; a docstring continued to assert that claim, and to cite the deleted |
| 84 | +axiom, after the code had been corrected. Unit-ness of the Frobenius roots was |
| 85 | +attributed to purity, when it is part (c) of Deligne's Conjecture 1.2.10, proved |
| 86 | +for curves by Lafforgue, and a conclusion separate from the weight condition — |
| 87 | +`(3 + 4i)/5` has absolute value `1` at every archimedean place and is not a |
| 88 | +`5`-adic unit. The equivalence between the span condition and absolute |
| 89 | +irreducibility was stated without its scope; it needs a field and `n ≥ 1`. |
| 90 | + |
| 91 | +Minor. `n : ℕ` admitted `n = 0`, and unramifiedness quantified over one prime |
| 92 | +above a place where every prime is wanted. |
| 93 | + |
| 94 | +## Why the unramifiedness hypothesis is not redundant |
| 95 | + |
| 96 | +It is tempting to drop it: continuity forces the image into a compact subgroup of |
| 97 | +`GL_n(E_λ)`, which stabilises a lattice, so the representation modulo each power |
| 98 | +of the maximal ideal factors through a finite extension ramified at finitely many |
| 99 | +places. That gives a finite ramification set at every finite level, but the |
| 100 | +level-wise sets need not stabilise, and for `n ≥ 2` they need not. A Kummer class |
| 101 | +built from `b_m = ∏_{i ≤ m} π_i^{ℓ^i}` gives a continuous upper-triangular |
| 102 | +`ρ = (χ_ℓ, c; 0, 1) : G_K → GL₂(ℤ_ℓ)` ramified at every `v_i`. Ramakrishna, |
| 103 | +Infinitely ramified Galois representations, Ann. of Math. 151 (2000), shows even |
| 104 | +full image is compatible with infinite ramification; Khare and Rajan, IMRN 2001 |
| 105 | +no. 12, show the ramified set has density zero but can still be infinite. For |
| 106 | +`n = 1` the claim is true, since the torsion of `1 + 𝔪` is finite and class field |
| 107 | +theory closes the argument. This is why finite ramification is an explicit |
| 108 | +condition in the Fontaine-Mazur conjecture rather than a consequence of |
| 109 | +continuity, and it is why the hypothesis is stated here. |
| 110 | + |
| 111 | +## What is not machine-checked |
| 112 | + |
| 113 | +Compile status and the axiom profile are checked in CI; see `Axioms.lean` and |
| 114 | +`.github/workflows/build.yml`. An instance diamond on the supplied |
| 115 | +`MulSemiringAction` is excluded only insofar as the build succeeds; no competing |
| 116 | +instance exists in Mathlib v4.28.0, where the ramification files take such |
| 117 | +actions as hypotheses. |
| 118 | + |
| 119 | +Lafforgue's Théorème VII.6 and Deligne's Conjecture 1.2.10 were verified through |
| 120 | +Drinfeld's verbatim quotations and bibliography rather than the originals. The |
| 121 | +internal part-numbering of the conjecture in Weil II was not checked against |
| 122 | +Deligne's own text. |
| 123 | + |
| 124 | +Every mathematical claim in this repository that is not a compiled Lean theorem |
| 125 | +is a claim, not a fact. The compiled theorems are listed in the README. |
0 commit comments