Some adelic background for quaternion algebras (#176)

* more

* fix

* epsilon more

* basics on adeles

* remove sorried data

* state hard theorem

FLT/FLT_files.lean

@@ -24,4 +24,5 @@ import FLT.MathlibExperiments.Frobenius2
 import FLT.MathlibExperiments.FrobeniusRiou
 import FLT.MathlibExperiments.HopfAlgebra.Basic
 import FLT.MathlibExperiments.IsFrobenius
+import FLT.NumberField.AdeleRing
 import FLT.TateCurve.TateCurve

FLT/NumberField/AdeleRing.lean

@@ -0,0 +1,113 @@
+import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
+import Mathlib.NumberTheory.NumberField.Basic
+
+universe u
+
+variable (K : Type*) [Field K] [NumberField K]
+
+section PRed
+-- Don't try anything in this section because we are missing a definition.
+
+-- see mathlib PR #16485
+def NumberField.AdeleRing (K : Type u) [Field K] [NumberField K] : Type u := sorry
+
+open NumberField
+
+-- All these are already done in mathlib PRs, so can be assumed for now.
+-- When they're in mathlib master we can update mathlib and then get these theorems/definitions
+-- for free.
+instance : CommRing (AdeleRing K) := sorry
+
+instance : TopologicalSpace (AdeleRing K) := sorry
+
+instance : TopologicalRing (AdeleRing K) := sorry
+
+instance : Algebra K (AdeleRing K) := sorry
+
+end PRed
+
+section AdeleRingLocallyCompact
+-- This theorem is proved in another project, so we may as well assume it.
+
+-- see https://github.com/smmercuri/adele-ring_locally-compact
+
+variable (K : Type*) [Field K] [NumberField K]
+
+theorem NumberField.AdeleRing.locallyCompactSpace : LocallyCompactSpace (AdeleRing K) := sorry
+
+end AdeleRingLocallyCompact
+
+section TODO
+-- these theorems can't be worked on yet because we don't have an actual definition
+-- of the adele ring. We can work out a strategy when we do.
+
+-- Maybe this isn't even stated in the best way?
+theorem NumberField.AdeleRing.discrete : ∀ k : K, ∃ U : Set (AdeleRing K),
+    IsOpen U ∧ (algebraMap K (AdeleRing K)) ⁻¹' U = {k} := sorry
+
+open NumberField
+
+-- ditto for this one
+theorem NumberField.AdeleRing.cocompact :
+    CompactSpace (AdeleRing K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing K)).toAddMonoidHom) :=
+  sorry
+
+end TODO
+
+-- *************** Sorries which are not impossible start here *****************
+
+-- recall we already had `variable (K : Type*) [Field K] [NumberField K]`
+
+variable (L : Type*) [Field L] [Algebra K L] [FiniteDimensional K L]
+
+instance : NumberField L := sorry -- inferInstance fails
+
+-- We want the map `L ⊗[K] 𝔸_K → 𝔸_L`, but we don't have a definition of adeles.
+-- However we do have a definition of finite adeles, so let's work there.
+
+namespace DedekindDomain
+
+open scoped TensorProduct NumberField -- ⊗ notation for tensor product and 𝓞 K notation for ring of ints
+
+noncomputable instance : Algebra K (ProdAdicCompletions (𝓞 L) L) := RingHom.toAlgebra <|
+  (algebraMap L (ProdAdicCompletions (𝓞 L) L)).comp (algebraMap K L)
+
+-- Need to pull back elements of HeightOneSpectrum (𝓞 L) to HeightOneSpectrum (𝓞 K)
+open IsDedekindDomain
+
+variable {L} in
+def HeightOneSpectrum.comap (w : HeightOneSpectrum (𝓞 L)) : HeightOneSpectrum (𝓞 K) where
+  asIdeal := w.asIdeal.comap (algebraMap (𝓞 K) (𝓞 L))
+  isPrime := Ideal.comap_isPrime (algebraMap (𝓞 K) (𝓞 L)) w.asIdeal
+  ne_bot := sorry -- pullback of nonzero prime is nonzero? Certainly true for number fields.
+  -- Idea of proof: show that if B/A is integral and B is an integral domain, then
+  -- any nonzero element of B divides a nonzero element of A.
+  -- In fact this definition should be made in that generality.
+  -- Use `Algebra.exists_dvd_nonzero_if_isIntegral` in the FLT file MathlibExperiments/FrobeniusRiou.lean
+
+variable {L} in
+noncomputable def HeightOneSpectrum.of_comap (w : HeightOneSpectrum (𝓞 L)) :
+    (HeightOneSpectrum.adicCompletion K (comap K w)) →+* (HeightOneSpectrum.adicCompletion L w) :=
+  letI : UniformSpace K := (comap K w).adicValued.toUniformSpace;
+  letI : UniformSpace L := w.adicValued.toUniformSpace;
+  UniformSpace.Completion.mapRingHom (algebraMap K L) <| by
+  sorry
+
+open HeightOneSpectrum in
+noncomputable def ProdAdicCompletions.baseChange :
+    L ⊗[K] ProdAdicCompletions (𝓞 K) K →ₗ[K] ProdAdicCompletions (𝓞 L) L := TensorProduct.lift <| {
+  toFun := fun l ↦ {
+    toFun := fun kv w ↦ l • (of_comap K w (kv (comap K w)))
+    map_add' := sorry
+    map_smul' := sorry
+  }
+  map_add' := sorry
+  map_smul' := sorry
+}
+
+-- hard but hopefully enough (this proof will be a lot of work)
+theorem ProdAdicCompletions.baseChange_iso (x : ProdAdicCompletions (𝓞 K) K) :
+  ProdAdicCompletions.IsFiniteAdele x ↔
+  ProdAdicCompletions.IsFiniteAdele (ProdAdicCompletions.baseChange K L (1 ⊗ₜ x)) := sorry
+
+-- Can we now write down the isomorphism L ⊗ 𝔸_K^∞ = 𝔸_L^∞ ?

blueprint/lean_decls

@@ -80,4 +80,7 @@ TotallyDefiniteQuaternionAlgebra.AutomorphicForm
 TotallyDefiniteQuaternionAlgebra.AutomorphicForm.addCommGroup
 TotallyDefiniteQuaternionAlgebra.AutomorphicForm.module
 TotallyDefiniteQuaternionAlgebra.AutomorphicForm.finiteDimensional
-DivisionAlgebra.finiteDoubleCoset
+DivisionAlgebra.finiteDoubleCoset
+NumberField.AdeleRing.discrete
+NumberField.AdeleRing.cocompact
+NumberField.AdeleRing.locallyCompactSpace

blueprint/src/chapter/QuaternionAlgebraProject.tex

@@ -202,9 +202,86 @@ \section{Statement of the main result of the miniproject}
 
 It thus remains to prove Fujisaki's lemma.
 
-% \section{Proof of Fujisaki's lemma}
+\section{Preliminaries on adeles of a number field}
 
-% We need to talk about the full adele ring of the number field~$K$. This is
-% the product of the finite adele ring $\A_K^\infty$ and the ring of ``infinite adeles''
-% $K\otimes_{\Q}\R$, which is often described as $\prod_{v\infty}K_v$, where
-% $v$ runs through the infinite places of $K$.
+Let $K$ be a number field. Right now mathlib has the finite adeles $\A_K^\infty$ of $K$,
+with its topological ring structure. It does not however have the infinite adeles $K_\infty$,
+which can be defined either as $K\otimes_{\Q}\R$ or as $\prod_{v\infty}K_v$, where
+$v$ runs through the infinite places of $K$. There are PRs by Salvatore Mercuri currently
+in progress for defining this topological ring. Once we have it, the full ring of
+adeles $\A_K$ is defined as $\A_K:=\A_K^\infty\times K_\infty$; it is a topological ring
+and also a $K$-algebra. Once Mercuri's mathlib PR `16485` is merged, we will have
+all this available to us; until then, we sorry the definitions and these facts.
+
+Mercuri's work isn't however enough for us; we also need several theorems about this topological
+$K$-algebra. These lemmas are essentially impossible to work on until we have the definition in
+mathlib. We state them here without proof.
+
+\begin{theorem}
+  \lean{NumberField.AdeleRing.discrete}
+  \label{NumberField.AdeleRing.discrete}
+  The additive subgroup $K$ of $\A_K$ is discrete.
+\end{theorem}
+
+\begin{theorem}
+  \lean{NumberField.AdeleRing.cocompact}
+  \label{NumberField.AdeleRing.cocompact}
+  The quotient $\A_K/K$ is compact.
+\end{theorem}
+
+\begin{theorem}
+  \lean{NumberField.AdeleRing.locallyCompactSpace}
+  \label{NumberField.AdeleRing.locallyCompact}
+  The topological ring $\A_K$ is locally compact.
+\end{theorem}
+
+Mercuri has already proved local compactness in
+\href{https://github.com/smmercuri/adele-ring_locally-compact}{his own repo} but rather than
+depending on this repo, we should aim to have this in mathlib. As far as I know, the other
+two theorems remain unformalised (but as I've mentioned, we cannot start on them until
+we have a definition of the adele ring).
+
+However, there is something that we can do here: one proof I know that of discreteness
+and cocompactness of $K$ in $\A_K$ reduces to the case $K=\Q$, using the ``canonical''
+isomorphism $\A_K\cong\A_{\Q}\otimes_{\Q}K$. This is proved by checking it for finite
+and infinite adeles separately, so one thing which we can work on now is the finite case.
+The general results we need are:
+
+\begin{theorem}
+  If $K$ is any field equipped with a real-valued absolute value $|.|$, and $L/K$ is a finite
+  separable extension of degree $N$, then there are at most $N$ extensions of $|.|$ to $L$.
+\end{theorem}
+
+The Lean formalisation of this would use {\tt AbsoluteValue}. However, I suspect that the
+archimedean case can be dealt with by hand, which means that we can probably restrict to
+{\tt Valuation}s.
+
+Now say $K$ is any field equipped with a real-valued absolute value $|.|$, $L/K$ is a finite
+separable extension, and let $||.||_i$ denote the finitely many extensions of $|.|$ to $L$.
+Let $\hat{K}$ denote the completion of $K$ with respect to $|.|$, and let $\hat{L}_i$ denote
+the completion of $L$ with respect to $||.||_i$. For each $i$ we have natural maps
+$\hat{K}\to\hat{L}_i$ and $L\to\hat{L}_i$, giving us a map $\theta:
+L\otimes_K\hat{K}\cong\prod_i\hat{L}_i$.
+
+\begin{theorem}
+  The map $\theta$ is an isomorphism of $L$-algebras.
+\end{theorem}
+
+Because $\hat{K}$ has a topology, we can give $L\otimes_K\hat{K}$ the $\hat{K}$-module topology.
+
+\begin{theorem}
+  The map $\theta$ is a topological isomorphism.
+\end{theorem}
+
+The map $\theta$ thus induces an isomorphism $L\otimes\prod_vK_v\to \prod_wL_w$, where $v$
+(resp. $w$) runs through the finite places of $K$ (resp. $L$).
+
+\begin{theorem}
+  The map $\theta$ induces an isomorphism (both topological and algebraic)
+  $L\otimes\A_K^\infty\to\A_L^\infty$.
+\end{theorem}
+\begin{proof}
+  It suffices to show that show that for all but finitely many finite places $v$ of $K$, the map
+  $\theta$ induces an isomorphism $\calO_L\otimes_{\calO_K}\calO_{K_v}\to\prod_i\calO_{\hat{L}_i}$
+  at the integral level.
+\end{proof}