Skip to content

Commit 66eeb47

Browse files
kbuzzardkbuzzard
committed
Merge branch 'main' of github.com:ImperialCollegeLondon/FLT into main
2 parents 0c1e08c + 0fae0ef commit 66eeb47

File tree

6 files changed

+254
-10
lines changed

6 files changed

+254
-10
lines changed

‎.github/workflows/01-claim-issue.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ jobs:
8484
COMMENT_RESPONSE=$(curl -s -o /dev/null -w "%{http_code}" -X POST \
8585
-H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
8686
-H "Content-Type: application/json" \
87-
-d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been added to the project board by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md)."}' \
87+
-d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been added to the project board by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md)."}' \
8888
https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/comments)
8989
9090
if [ "$COMMENT_RESPONSE" -eq 201 ]; then
@@ -113,7 +113,7 @@ jobs:
113113
if [ "$CURRENT_STATUS_ID" != "$UNCLAIMED_TASKS_ID" ]; then
114114
echo "Issue is not classified as 'Unclaimed'. Posting comment."
115115
curl -X POST -H "Authorization: token ${{ secrets.GITHUB_TOKEN }}" \
116-
-d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been classified as an \"Unclaimed Outstanding Task\" by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/teorth/equational_theories/blob/main/CONTRIBUTING.md)."}' \
116+
-d '{"body": "This issue cannot be assigned to @${{ github.event.comment.user.login }} because it has not been classified as an \"Unclaimed Outstanding Task\" by the project maintainers.\n\nPlease consider discussing the issue on our [Zulip channel](https://leanprover.zulipchat.com/#narrow/stream/416277-FLT). To understand the contribution process, please read the [CONTRIBUTING guide](https://github.com/ImperialCollegeLondon/FLT/blob/main/CONTRIBUTING.md)."}' \
117117
https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.issue.number }}/comments
118118
exit 1
119119
fi

‎FLT/FLT_files.lean

+1
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,5 @@ import FLT.MathlibExperiments.Frobenius2
1919
import FLT.MathlibExperiments.FrobeniusRiou
2020
import FLT.MathlibExperiments.HopfAlgebra.Basic
2121
import FLT.MathlibExperiments.IsFrobenius
22+
import FLT.NumberField.AdeleRing
2223
import FLT.TateCurve.TateCurve

‎FLT/NumberField/AdeleRing.lean

+159
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
2+
import Mathlib.NumberTheory.NumberField.Basic
3+
import Mathlib
4+
5+
universe u
6+
7+
section PRed
8+
-- Don't try anything in this section because we are missing a definition.
9+
10+
-- see mathlib PR #16485
11+
def NumberField.AdeleRing (K : Type u) [Field K] [NumberField K] : Type u := sorry
12+
13+
open NumberField
14+
15+
variable (K : Type*) [Field K] [NumberField K]
16+
17+
-- All these are already done in mathlib PRs, so can be assumed for now.
18+
-- When they're in mathlib master we can update mathlib and then get these theorems/definitions
19+
-- for free.
20+
instance : CommRing (AdeleRing K) := sorry
21+
22+
instance : TopologicalSpace (AdeleRing K) := sorry
23+
24+
instance : TopologicalRing (AdeleRing K) := sorry
25+
26+
instance : Algebra K (AdeleRing K) := sorry
27+
28+
end PRed
29+
30+
section AdeleRingLocallyCompact
31+
-- This theorem is proved in another project, so we may as well assume it.
32+
33+
-- see https://github.com/smmercuri/adele-ring_locally-compact
34+
35+
variable (K : Type*) [Field K] [NumberField K]
36+
37+
theorem NumberField.AdeleRing.locallyCompactSpace : LocallyCompactSpace (AdeleRing K) := sorry
38+
39+
end AdeleRingLocallyCompact
40+
41+
section TODO
42+
-- these theorems can't be worked on yet because we don't have an actual definition
43+
-- of the adele ring. We can work out a strategy when we do.
44+
45+
variable (K : Type*) [Field K] [NumberField K]
46+
47+
-- Maybe this isn't even stated in the best way?
48+
theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing K),
49+
IsOpen U ∧ (algebraMap K (AdeleRing K)) ⁻¹' U = {k} := sorry
50+
51+
open NumberField
52+
53+
-- ditto for this one
54+
theorem NumberField.AdeleRing.cocompact :
55+
CompactSpace (AdeleRing K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing K)).toAddMonoidHom) :=
56+
sorry
57+
58+
end TODO
59+
60+
-- *************** Sorries which are not impossible start here *****************
61+
62+
variable (A K L B : Type*) [CommRing A] [CommRing B] [Algebra A B] [Field K] [Field L]
63+
[Algebra A K] [IsFractionRing A K] [Algebra B L] [IsDedekindDomain A]
64+
[Algebra K L] [Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L]
65+
[IsIntegralClosure B A L] [FiniteDimensional K L]
66+
67+
variable [IsDomain B] -- is this necessary?
68+
variable [Algebra.IsSeparable K L]
69+
70+
-- example : IsDedekindDomain B := IsIntegralClosure.isDedekindDomain A K L B
71+
72+
variable [IsDedekindDomain B]
73+
74+
-- example : IsFractionRing B L := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
75+
76+
variable [IsFractionRing B L]
77+
78+
-- example : Algebra.IsIntegral A B := IsIntegralClosure.isIntegral_algebra A L
79+
80+
variable [Algebra.IsIntegral A B]
81+
82+
-- Conjecture: in this generality there's a natural isomorphism `L ⊗[K] 𝔸_K^∞ → 𝔸_L^∞`
83+
-- Note however that we don't have a definition of adeles in this generality.
84+
85+
-- One key input is the purely local statement that if L/K
86+
-- is a finite extension of number fields, and v is a place of K,
87+
-- then `L ⊗[K] Kᵥ ≅ ⊕_w|v L_w`, where the sum is over the places w
88+
-- of L above v.
89+
namespace DedekindDomain
90+
91+
open scoped TensorProduct -- ⊗ notation for tensor product
92+
93+
noncomputable instance : Algebra K (ProdAdicCompletions B L) := RingHom.toAlgebra <|
94+
(algebraMap L (ProdAdicCompletions B L)).comp (algebraMap K L)
95+
96+
-- Need to pull back elements of HeightOneSpectrum B to HeightOneSpectrum A
97+
open IsDedekindDomain
98+
99+
namespace HeightOneSpectrum
100+
-- first need a map from finite places of 𝓞L to finite places of 𝓞K
101+
variable {B L} in
102+
def comap (w : HeightOneSpectrum B) : HeightOneSpectrum A where
103+
asIdeal := w.asIdeal.comap (algebraMap A B)
104+
isPrime := Ideal.comap_isPrime (algebraMap A B) w.asIdeal
105+
ne_bot := mt Ideal.eq_bot_of_comap_eq_bot w.ne_bot
106+
107+
open scoped algebraMap
108+
109+
-- homework
110+
def valuation_comap (w : HeightOneSpectrum B) (x : K) :
111+
(comap A w).valuation x = w.valuation (algebraMap K L x) ^ (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) := sorry
112+
113+
-- Say w is a finite place of L lying above v a finite places
114+
-- of K. Then there's a ring hom K_v -> L_w.
115+
variable {B L} in
116+
noncomputable def of_comap (w : HeightOneSpectrum B) :
117+
(HeightOneSpectrum.adicCompletion K (comap A w)) →+* (HeightOneSpectrum.adicCompletion L w) :=
118+
letI : UniformSpace K := (comap A w).adicValued.toUniformSpace;
119+
letI : UniformSpace L := w.adicValued.toUniformSpace;
120+
UniformSpace.Completion.mapRingHom (algebraMap K L) <| by
121+
-- question is the following:
122+
-- if L/K is a finite extension of sensible fields (e.g. number fields)
123+
-- and if w is a finite place of L lying above v a finite place of K,
124+
-- and if we give L the w-adic topology and K the v-adic topology,
125+
-- then the map K → L is continuous
126+
refine continuous_of_continuousAt_zero (algebraMap K L) ?hf
127+
delta ContinuousAt
128+
simp only [map_zero]
129+
rw [(@Valued.hasBasis_nhds_zero K _ _ _ (comap A w).adicValued).tendsto_iff
130+
(@Valued.hasBasis_nhds_zero L _ _ _ w.adicValued)]
131+
simp only [HeightOneSpectrum.adicValued_apply, Set.mem_setOf_eq, true_and, true_implies]
132+
refine fun i ↦ ⟨i ^ (1 / Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal), fun _ h ↦ ?_⟩
133+
-- last line is nonsense but use `valuation_comap` to finish
134+
push_cast at h
135+
sorry
136+
137+
end HeightOneSpectrum
138+
139+
open HeightOneSpectrum
140+
141+
noncomputable def ProdAdicCompletions.baseChange :
142+
L ⊗[K] ProdAdicCompletions A K →ₗ[K] ProdAdicCompletions B L := TensorProduct.lift <| {
143+
toFun := fun l ↦ {
144+
toFun := fun kv w ↦ l • (of_comap A K w (kv (comap A w)))
145+
map_add' := sorry
146+
map_smul' := sorry
147+
}
148+
map_add' := sorry
149+
map_smul' := sorry
150+
}
151+
152+
-- hard but hopefully enough (this proof will be a lot of work)
153+
theorem ProdAdicCompletions.baseChange_iso (x : ProdAdicCompletions A K) :
154+
ProdAdicCompletions.IsFiniteAdele x ↔
155+
ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChange A K L B (1 ⊗ₜ x)) := sorry
156+
157+
end DedekindDomain
158+
159+
-- Can we now write down the isomorphism L ⊗ 𝔸_K^∞ = 𝔸_L^∞ ?

‎README.md

+6-2
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11
# Fermat's Last Theorem
22

3-
[![Website](https://img.shields.io/badge/Website-ready-green)](https://ImperialCollegeLondon.github.io/FLT/) [![Documentation](https://img.shields.io/badge/Documentation-passing-green)](https://ImperialCollegeLondon.github.io/FLT/docs/) [![Blueprint](https://img.shields.io/badge/Blueprint-WIP-blue)](https://ImperialCollegeLondon.github.io/FLT/blueprint/) [![Paper](https://img.shields.io/badge/Paper-WIP-blue)](https://ImperialCollegeLondon.github.io/FLT/blueprint.pdf) [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/ImperialCollegeLondon/FLT)
3+
[![Website](https://img.shields.io/badge/Website-ready-green)](https://ImperialCollegeLondon.github.io/FLT/)
4+
[![Documentation](https://img.shields.io/badge/Documentation-passing-green)](https://ImperialCollegeLondon.github.io/FLT/docs/)
5+
[![Blueprint](https://img.shields.io/badge/Blueprint-WIP-blue)](https://ImperialCollegeLondon.github.io/FLT/blueprint/)
6+
[![Paper](https://img.shields.io/badge/Paper-WIP-blue)](https://ImperialCollegeLondon.github.io/FLT/blueprint.pdf)
7+
[![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/ImperialCollegeLondon/FLT)
48

5-
An ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover.
9+
An ongoing multi-author open source project to formalise a proof of Fermat's Last Theorem in the Lean theorem prover.
610

711
# Information about the project
812

‎blueprint/lean_decls

+4-1
Original file line numberDiff line numberDiff line change
@@ -80,4 +80,7 @@ TotallyDefiniteQuaternionAlgebra.AutomorphicForm
8080
TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup
8181
TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module
8282
TotallyDefiniteQuaternionAlgebra.AutomorphicForm.finiteDimensional
83-
DivisionAlgebra.finiteDoubleCoset
83+
DivisionAlgebra.finiteDoubleCoset
84+
NumberField.AdeleRing.discrete
85+
NumberField.AdeleRing.cocompact
86+
NumberField.AdeleRing.locallyCompactSpace

‎blueprint/src/chapter/QuaternionAlgebraProject.tex

+82-5
Original file line numberDiff line numberDiff line change
@@ -202,9 +202,86 @@ \section{Statement of the main result of the miniproject}
202202

203203
It thus remains to prove Fujisaki's lemma.
204204

205-
% \section{Proof of Fujisaki's lemma}
205+
\section{Preliminaries on adeles of a number field}
206206

207-
% We need to talk about the full adele ring of the number field~$K$. This is
208-
% the product of the finite adele ring $\A_K^\infty$ and the ring of ``infinite adeles''
209-
% $K\otimes_{\Q}\R$, which is often described as $\prod_{v\infty}K_v$, where
210-
% $v$ runs through the infinite places of $K$.
207+
Let $K$ be a number field. Right now mathlib has the finite adeles $\A_K^\infty$ of $K$,
208+
with its topological ring structure. It does not however have the infinite adeles $K_\infty$,
209+
which can be defined either as $K\otimes_{\Q}\R$ or as $\prod_{v\infty}K_v$, where
210+
$v$ runs through the infinite places of $K$. There are PRs by Salvatore Mercuri currently
211+
in progress for defining this topological ring. Once we have it, the full ring of
212+
adeles $\A_K$ is defined as $\A_K:=\A_K^\infty\times K_\infty$; it is a topological ring
213+
and also a $K$-algebra. Once Mercuri's mathlib PR `16485` is merged, we will have
214+
all this available to us; until then, we sorry the definitions and these facts.
215+
216+
Mercuri's work isn't however enough for us; we also need several theorems about this topological
217+
$K$-algebra. These lemmas are essentially impossible to work on until we have the definition in
218+
mathlib. We state them here without proof.
219+
220+
\begin{theorem}
221+
\lean{NumberField.AdeleRing.discrete}
222+
\label{NumberField.AdeleRing.discrete}
223+
The additive subgroup $K$ of $\A_K$ is discrete.
224+
\end{theorem}
225+
226+
\begin{theorem}
227+
\lean{NumberField.AdeleRing.cocompact}
228+
\label{NumberField.AdeleRing.cocompact}
229+
The quotient $\A_K/K$ is compact.
230+
\end{theorem}
231+
232+
\begin{theorem}
233+
\lean{NumberField.AdeleRing.locallyCompactSpace}
234+
\label{NumberField.AdeleRing.locallyCompact}
235+
The topological ring $\A_K$ is locally compact.
236+
\end{theorem}
237+
238+
Mercuri has already proved local compactness in
239+
\href{https://github.com/smmercuri/adele-ring_locally-compact}{his own repo} but rather than
240+
depending on this repo, we should aim to have this in mathlib. As far as I know, the other
241+
two theorems remain unformalised (but as I've mentioned, we cannot start on them until
242+
we have a definition of the adele ring).
243+
244+
However, there is something that we can do here: one proof I know that of discreteness
245+
and cocompactness of $K$ in $\A_K$ reduces to the case $K=\Q$, using the ``canonical''
246+
isomorphism $\A_K\cong\A_{\Q}\otimes_{\Q}K$. This is proved by checking it for finite
247+
and infinite adeles separately, so one thing which we can work on now is the finite case.
248+
The general results we need are:
249+
250+
\begin{theorem}
251+
If $K$ is any field equipped with a real-valued absolute value $|.|$, and $L/K$ is a finite
252+
separable extension of degree $N$, then there are at most $N$ extensions of $|.|$ to $L$.
253+
\end{theorem}
254+
255+
The Lean formalisation of this would use {\tt AbsoluteValue}. However, I suspect that the
256+
archimedean case can be dealt with by hand, which means that we can probably restrict to
257+
{\tt Valuation}s.
258+
259+
Now say $K$ is any field equipped with a real-valued absolute value $|.|$, $L/K$ is a finite
260+
separable extension, and let $||.||_i$ denote the finitely many extensions of $|.|$ to $L$.
261+
Let $\hat{K}$ denote the completion of $K$ with respect to $|.|$, and let $\hat{L}_i$ denote
262+
the completion of $L$ with respect to $||.||_i$. For each $i$ we have natural maps
263+
$\hat{K}\to\hat{L}_i$ and $L\to\hat{L}_i$, giving us a map $\theta:
264+
L\otimes_K\hat{K}\cong\prod_i\hat{L}_i$.
265+
266+
\begin{theorem}
267+
The map $\theta$ is an isomorphism of $L$-algebras.
268+
\end{theorem}
269+
270+
Because $\hat{K}$ has a topology, we can give $L\otimes_K\hat{K}$ the $\hat{K}$-module topology.
271+
272+
\begin{theorem}
273+
The map $\theta$ is a topological isomorphism.
274+
\end{theorem}
275+
276+
The map $\theta$ thus induces an isomorphism $L\otimes\prod_vK_v\to \prod_wL_w$, where $v$
277+
(resp. $w$) runs through the finite places of $K$ (resp. $L$).
278+
279+
\begin{theorem}
280+
The map $\theta$ induces an isomorphism (both topological and algebraic)
281+
$L\otimes\A_K^\infty\to\A_L^\infty$.
282+
\end{theorem}
283+
\begin{proof}
284+
It suffices to show that show that for all but finitely many finite places $v$ of $K$, the map
285+
$\theta$ induces an isomorphism $\calO_L\otimes_{\calO_K}\calO_{K_v}\to\prod_i\calO_{\hat{L}_i}$
286+
at the integral level.
287+
\end{proof}

0 commit comments

Comments
 (0)