You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
- Drop hK : FunctionField Fq K from exists_companion and the family corollary:
it follows from the finite-type hypothesis plus the RatFunc Fq embedding, so
it was a redundant hypothesis. Fq is passed by name where the family
corollary invokes exists_companion, since no explicit argument determines it
any longer.
- AUDIT: restore both inductive conditions on the Kummer construction (the
condensed version pinned only the later pi_j and did not fix v_i(b_m));
retract the companion-matrix witness as overstated (degree-one places only,
lambda-unit roots only at lambda_0) while keeping the degeneracy finding;
E-rationality is definitionally necessary for the compatibility notion here;
n = 0 and one-prime items reclassified as reformulations; Ramakrishna scoped
to a density-one set of primes; finite-level Frobenius API recorded;
primary-source verification status updated.
- Frobenius convention noted where VII.6 was said to apply directly: Mathlib's
Frobenius is arithmetic, Lafforgue's polynomials use geometric.
- Unit-ness scoped away from p with slope bounds at p; the (sigma_lambda)^r
descent restated as the n-th power in this file's notation; lisse scope added
to the integrality remark; 'constant field' corrected to the chosen finite
base field; 'need not be either' fix in the Setup comment.
- Design debt recorded: IsUnramifiedAt generalisation over the target ring,
FrobeniusChoice restriction to the complement of S.
`E`-rationality of the Frobenius characteristic polynomials were all added. The
71
76
first two are Lafforgue's own hypotheses; the third is an artefact of fixing `E`
72
77
in advance here, where Lafforgue obtains the number field as part of the theorem.
73
-
None of the three is necessary for a compatible system to exist, since reducible
74
-
ones do.
78
+
Neither of the first two is necessary for a compatible family to exist, since
79
+
reducible compatible systems do; the third cannot be dropped even in principle,
80
+
because the notion of compatibility here builds `E`-rationality of the
81
+
polynomials into the definition.
75
82
Once those hypotheses were added the statement was still stronger than the
76
83
theorem it named, in two independent ways. The conclusion placed companions over
77
84
`E_λ` itself, where Theorem VII.6(v) gives the companion over a finite extension
@@ -87,31 +94,41 @@ was never actually assumed, since declaring a structure with an existence field
87
94
does not assume it, so the compatibility condition could hold vacuously; it is
88
95
now passed as data. Separately, the base ring was an arbitrary Dedekind domain
89
96
with the right fraction field, and fields and discrete valuation rings qualify,
90
-
so the place set could be empty or a single point. The conclusion was then
91
-
satisfiable cheaply, since the roots of the prescribed polynomial are `λ`-adic
92
-
units, `GL_n(O_λ)` is profinite and `Ẑ` is procyclic, so a companion-matrix
93
-
representation of the constant-field quotient satisfies everything. What made
94
-
that sufficient is that the conclusion of the version in question imposed no
95
-
irreducibility on the members of the family. It would not satisfy the present
96
-
conclusion: a representation factoring through a procyclic group has image
97
-
generated by a single matrix `C`, so its span lies in `M[C]` and has dimension at
98
-
most `n`, short of the `n²` that `SpanFull` demands once `n > 1`. Requiring the
99
-
base ring to be a finite-type algebra over the constant field makes its spectrum
97
+
so the place set could be empty or a single point. In the empty case every condition in the
98
+
definition quantifies over places that do not exist, and the conclusion was
99
+
trivially satisfiable; a single place leaves the compatibility conditions
100
+
constraining one Frobenius conjugacy class instead of infinitely many. An
101
+
earlier version of this file claimed an explicit cheap witness in the one-place
102
+
case, a companion-matrix representation of the constant-field quotient. That was
103
+
overstated: the construction matches the prescribed polynomial only at a place
104
+
of degree one, since a place of degree `d` sends the generator to the `d`-th
105
+
power of the chosen matrix, and it needs the roots of the polynomial to be units
106
+
at the target `λ`, which continuity supplies only at `λ₀`. Nor would any witness
107
+
of that shape survive the present conclusion: a representation factoring through
108
+
a procyclic group has image generated by a single matrix `C`, so its span lies
109
+
in `M[C]` and has dimension at most `n`, short of the `n²` that `SpanFull`
110
+
demands once `n > 1`. Requiring the
111
+
base ring to be a finite-type algebra over the chosen finite base field makes its spectrum
100
112
a smooth affine curve carrying cofinitely many of the places, and closes this.
101
113
102
114
Three claims were described as doing more than they do.
103
115
`charpoly_eq_of_isConj` was said to establish well-definedness of the
104
116
compatibility condition, which needs inertia rather than conjugacy, and a
105
117
docstring continued to assert that claim, and to cite the deleted axiom, after
106
-
the code had been corrected. Unit-ness of the Frobenius roots was attributed to
107
-
purity, when it is part (iii) of Deligne's Conjecture 1.2.10, labelled (c) in
118
+
the code had been corrected. Unit-ness of the Frobenius roots away from `p` was attributed to purity, when it is part (iii) of Deligne's Conjecture 1.2.10, labelled (c) in
108
119
Drinfeld's abbreviated restatement, proved for curves by Lafforgue, and a conclusion separate from the weight condition; `(3 + 4i)/5` has
109
120
absolute value `1` at every archimedean place and is not a `5`-adic unit. The
110
121
equivalence between the span condition and absolute irreducibility was stated
111
122
without its scope, which is a field and `n ≥ 1`.
112
123
113
-
Two smaller defects: `n : ℕ` admitted `n = 0`, and unramifiedness quantified over
114
-
one prime above a place where every prime is wanted.
124
+
Two smaller items were reformulations rather than corrections of wrong
125
+
mathematics. Positivity of `n` became a hypothesis of the main theorem; the
126
+
definitions still compile at `n = 0`, where `GL (Fin 0)` is trivial and the
127
+
predicates hold vacuously, harmless where they are used. And unramifiedness,
128
+
which had quantified over one prime above a place, now quantifies over every
129
+
prime; the two readings are equivalent once a prime above `v` exists, since the
130
+
primes are conjugate and `ker ρ` is normal, but the every-prime form does not
131
+
lean on the transitivity that is unavailable here.
115
132
116
133
One error was not about the mathematics at all. An action of `G_K` on the
117
134
integral closure of `A` in `K̄`, and the `SMulCommClass` accompanying it, were
@@ -133,13 +150,17 @@ It is tempting to drop it. Continuity forces the image into a compact subgroup o
133
150
of the maximal ideal factors through a finite extension ramified at finitely many
134
151
places. That gives a finite ramification set at every finite level, but the
135
152
level-wise sets need not stabilise, and for `n ≥ 2` they need not. For
136
-
`ℓ ≠ char K`, a Kummer class built from `b_m = ∏_{i ≤ m} π_i^{ℓ^i}`, with places
137
-
`v_i` and elements `π_i` chosen so that `v_i(π_i) = 1` and each later `π_j` is a
138
-
unit at the earlier `v_i`, gives a continuous upper-triangular
139
-
`ρ = (χ_ℓ, c; 0, 1) : G_K → GL₂(ℤ_ℓ)` ramified at every `v_i`. Ramakrishna,
153
+
`ℓ ≠ char K`, a Kummer class built from `b_m = ∏_{i ≤ m} π_i^{ℓ^i}`, with the places `v_i` and elements `π_i` chosen
154
+
inductively so that `v_i(π_i) = 1` and `v_i(π_j) = 0` for every `j ≠ i`, gives a
every `v_i`; a block sum with the trivial representation extends this to every
157
+
`n ≥ 2`. Controlling the earlier `π_j` at `v_i` as well as the later ones is
158
+
what makes `v_i(b_m) = ℓ^i` exactly, which is nonzero mod `ℓ^m` for every
159
+
`m > i`. Ramakrishna,
140
160
*Infinitely ramified Galois representations*, Ann. of Math. 151 (2000), 793–815,
141
-
constructs over `ℚ` surjective `GL₂(ℤ_ℓ)`-valued representations ramified at
142
-
infinitely many primes, so even full image is compatible with infinite
161
+
constructs over `ℚ`, for every prime `ℓ ≥ 5` in a set of density one,
162
+
surjective `GL₂(ℤ_ℓ)`-valued representations ramified at infinitely many primes,
163
+
so even full image is compatible with infinite
143
164
ramification;
144
165
Khare–Rajan, Int. Math. Res. Not. 2001, no. 12, 601–607, show that for continuous
145
166
semisimple representations of the absolute Galois group of a number field the
@@ -173,13 +194,19 @@ Three notions defined here have close Mathlib counterparts that are not used.
173
194
`LambdaAdicRep` is a `ContinuousMonoidHom`; the recurring conjunction
174
195
`Q.IsPrime ∧ Q.under A = v.asIdeal` restates `Ideal.LiesOver`, the idiom
175
196
`RingTheory/Frobenius.lean` itself uses; and `Field.absoluteGaloisGroup` is the
176
-
fixed-closure form of `AbsGal`. Each is equivalent to what is written, and each
177
-
would be the better choice in a version aimed at upstreaming.
178
-
179
-
Lafforgue's Theorem VII.6 and Deligne's Conjecture 1.2.10 were verified through
180
-
Drinfeld's verbatim quotations and bibliography rather than the originals. The
181
-
internal part-numbering of the conjecture in Weil II was not checked against
182
-
Deligne's own text.
197
+
fixed-closure form of `AbsGal`. Each is equivalent to what is written, and each would be the better choice in a version aimed at upstreaming. Two further
198
+
items: `IsUnramifiedAt` is hard-wired to representations over `E_λ`, so the same
199
+
inertia condition is written a second time, inline, in the conclusion of
200
+
`exists_companion`, where a version stated for an arbitrary `G →* GL n R` would
201
+
let hypothesis, conclusion and the family corollary share one predicate; and
202
+
`FrobeniusChoice` supplies a lift at every place where only the places outside
203
+
`S` are used.
204
+
205
+
The literature attributions, including Deligne's part-numbering in Weil II and
206
+
the hypotheses and conclusions of Lafforgue's Theorem VII.6, have been checked
207
+
against the primary sources. Two asides rest on standard usage rather than the
208
+
original papers: the attribution of the matrix-span criterion to Burnside, and
209
+
the remark about the Fontaine–Mazur conjecture.
183
210
184
211
Every mathematical claim in this repository that is not a compiled Lean theorem
185
212
is a claim, not a fact. The compiled theorems are listed in the README.
0 commit comments