Rolling update

Stream: FLT

[Kevin Buzzard]

Looking ahead I can see a lot of time for Fermat (my realisation a few months ago that I should start saying no to invitations by default rather than yes is now starting to pay off, with very little in my diary for the next few months). So, following an idea which worked very well in the equational reasoning project, and given that I hope to see a lot of movement on FLT in the next few months, I'll use this thread to say what I've been doing this week and flag some low-hanging fruit.

Remember that there is some clear plan with lots of LaTeX all explained here for proving that spaces of quaternionic modular forms are finite-dimensional. I've decided to just leave this (thank you to the people who've made PRs in the last few days, including at least one person who just came out of the blue and filled in a sorry) and start on something else, namely the Hecke algebra T.

The first job is to define the level we're working in, which is a compact open subgroup often called $U_1(N)$ or $U_1(S)$, associated in our case to a finite set of primes $S$. I have now done this in the file FLT.QuaternionAlgebra.NumberField modulo 10 sorrys, many of which should be easy. There is no LaTeX, I'm just writing the Lean (to be honest, I find writing the LaTeX and doing all the wiring up of the blueprint really slows things down).

Rather than writing a bunch of LaTeX, let me explain the sorrys in this thread.

The players are: a number field F, a finite place v, and then the completion v.adicCompletion F (let me call this $K$ for short), which is a field equipped with a subring v.adicCompletionIntegers F (let me call this $R$ for short). The ring $R$ is the "closed unit disc" of $K$ in the sense that there's a valuation Valued.v on $K$ and $R$ is the things with Valued.v <= 1. $R$ is a local ring with maximal ideal $m$ which is the things with Valued.v < 1.

I define GL2.localFullLevel to be the subgroup $GL_2(R)$ of $GL_2(K)$. I define GL2.localTameLevel to be a slightly smaller subgroup, consisting of matrices $(a,b;c,d)\in GL_2(R)$ with $a-d\in m$ and $c\in m$. I skipped the proof that this is a group but it's not hard, it's just a calculation. One nice way of seeing why it's true is that there's an obvious map $GL_2(R)\to GL_2(R/m)$ and the local tame level is just the preimage of the subgroup $(x,y;0,x)$ of $GL_2(R/m)$. Those are the sorries on lines 51 and 53.

Next we need the $F$-algebra homomorphism from $\prod_wF_w$ to $F_v$ which is just the projection; I didn't check it was an $F$-algebra map but this presumably just follows from the definitions. These are the sorries on lines 62 to 66 and this should probably be in mathlib. What we really want is the $F$-algebra map from the finite adeles of $F$ to $F_v$ but this is just the inclusion from the finite adeles into the product, composed with the projection.

Finally, we want GL2.TameLevel to be the pullback to $GL_2(\mathbb{A}_F^\infty)$ of the product of all of these groups defined above. More precisely, this just involves little more than checking that a product of groups is a group as far as I can see, the sorries are lines 90 to 92.

To come: we'll need to check that this subgroup is compact and open, and then we'll have to define Hecke operators at this level, which I hope to start working on next week.

[Ruben Van de Velde]

Did you mean to give GL2.TameLevel an unused (S : Finset (HeightOneSpectrum (𝓞 F))) argument?

[Ruben Van de Velde]

(FLT#358)

[Kevin Buzzard]

Oh that's not supposed to be unused! We need those linters!

def GL2.TameLevel (S : Finset (HeightOneSpectrum (𝓞 F))) :
  Subgroup (GL (Fin 2) (FiniteAdeleRing (𝓞 F) F)) where
    carrier := {x | (∀ v, GL2.toAdicCompletion v x ∈ GL2.localFullLevel v) ∧
      (∀ v ∈ S, GL2.toAdicCompletion v x ∈ GL2.localTameLevel v)}

The point of the local tame levels is that the global thing is full away from S and tame at S

[Kevin Buzzard]

I've pushed the fix to main so probably broken your PR

[Ruben Van de Velde]

The unused arguments linter only triggers when you have no more sorries, which is why you didn't see it

[Ruben Van de Velde]

But it seems like my lazy simp_all proofs still work even with that fixed

[Kevin Buzzard]

Watching CI (so I can try to merge before going to bed) and I see

Run scripts/build_docs.sh
mv: cannot move 'docs/docs' to 'docbuild/.lake/build/doc': No such file or directory
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
...

[Damiano Testa]

mv: cannot move 'docs/docs' to 'docbuild/.lake/build/doc': No such file or directory was mentioned some other time as well.

[Kevin Buzzard]

Let's try this

[Damiano Testa]

Oh, it was probably #FLT > Help -- CI broken

[Kevin Buzzard]

Since that thread we have changed the way the docs work in FLT#319 (and then tinkered in FLT#334 and FLT#343 )

[Kevin Buzzard]

Back to mathematics: after #358 the only sorries left in these new subgroups are

noncomputable def GL2.localTameLevel (v : HeightOneSpectrum (𝓞 F)) :
    Subgroup (GL (Fin 2) (v.adicCompletion F)) where
      carrier := {x ∈ localFullLevel v |
        Valued.v (x.val 0 0 - x.val 1 1) < 1 ∧ Valued.v (x.val 1 0) < 1}
      mul_mem' := sorry
      one_mem' := by simp [one_mem]
      inv_mem' := sorry

My instinct is that it's easiest just to grind these out rather than doing anything fancy like proving its the preimage of a subgroup. For multiplication the proof is this:

1) Prove that if x is in localFullLevel v then det(x) is a unit (i.e. Valued.v(det(x))=1) (because det(x) is certainly an integer as all its entries are integers, as is det(x^{-1}), and their product is 1)

Let me write |t| for Valued.v(t) and call it "norm"

2) Prove that if x is in localFullLevel v and v(x_{10})<1 then v(x_{00}) and v(x_{11}) must both be 1 (because x_{00}x_{11}-x_{10}x_{01} is a unit so has norm 1, and x_{10}x_{01} has norm less than 1)

3) $(xy)_{00}-(xy)_{11}=x_{00}y_{00}+x_{01}y_{10}-x_{10}y_{01}-x_{11}y_{11}$, the middle 2 terms have norm less than 1, and x_{00}y_{00}-x_{11}y_{11}=x_{00}(y_{00}-y_{11})+(x_{00}-x_{11})y_{11} so this has norm less than 1

4) (xy)_{10}=x_{11}y_{10}-x_{10}y_{00} so also has norm less than 1 becaue y_{10} and x_{10} do

That does multiplication. For inverse just use the formula for inverse of a 2x2 matrix.

[Ruben Van de Velde]

I have a proof of inv assuming |det x| ≤ 1 I can dig up when I get to my laptop tomorrow, but that shouldn't stop anyone from working on it; it's indeed just applying the lemma in mathlib for the 2x2 inverse

[Kevin Buzzard]

So what's going on is we have a big field $K$ (this v.adicCompletion thing) and a smaller subring $R$ which also happens to be the closed unit ball in this field (the norm on this field has the weird property that $||x+y||\leq max\{||x||,||y||\}$ and so if two things have norm at most 1 then so does their sum).

[Kevin Buzzard]

And then we have a big group $GL_2(K)$ and a smaller subgroup $GL_2(R)$ which is this localFullLevel thing, and the determinant map sends $GL_2(K)$ to $K^\times$ and it also sends $GL_2(R)$ to $R^\times$, because a matrix in $GL_2(R)$ has entires in $R$ so determinant in $R$, but its inverse also has entries in $R$ by definition of $GL_2$ so the inverse also has determinant in $R$, so the determinants must be units because they're inverses of each other.

[Yaël Dillies]

Kevin Buzzard said:

Watching CI (so I can try to merge before going to bed) and I see

Run scripts/build_docs.sh
mv: cannot move 'docs/docs' to 'docbuild/.lake/build/doc': No such file or directory
info: docbuild: no previous manifest, creating one from scratch
info: leanprover/doc-gen4: cloning https://github.com/leanprover/doc-gen4
...

I am fixing this. Sorry, didn't have enough computer time yesterday

[Kevin Buzzard]

OK so I just pushed some new sorries, for example:
1) the subgroup GL_2(R) of GL_2(K) is open and compact (here K is a completion of a number field at a finite place, and R is the ring of integers)
and also global variants (in FLT.QuaternionAlgebra.NumberField)
2) A rank 4 module has finite rank :-/ (in /FLT/Mathlib/Algebra/IsQuaternionAlgebra)

[Ruben Van de Velde]

I've got some unpolished proofs for GL2.localTameLevel up at FLT#361, but no more time tonight

[Kevin Buzzard]

OK so I had to have an enforced break from FLT while I read a PhD thesis, went to Copenhagen to examine it, gave a big school talk and wrote a grant proposal, but now I'm back on track. The big job I'm working on right now is defining the "T" in the R=T theorem, I'm refactoring the definition of an automorphic form on a quaternion algebra in branch quat-alg-weight-2 so that I can use a general "Hecke operator machine" to build the ring we want. I've spent the last couple of days trying to get up to date with open PR's; I've merged Andrew Yang's R=T theorem :tada: and reviewed Salvatore Mercuri's work on infinite adeles. Matthew Jasper is a newcomer but they're making useful PRs -- thanks if you're reading.

[Kevin Buzzard]

OK so quaternionic modular forms are now refactored, in a way which will make Hecke operators much easier to do. I feel like I'm only two serious "sessions" away from the definition of T. Also I have become convinced (something which I didn't know in the 90s) that in fact to prove FLT you only ever need to consider Galois representations with cyclotomic determinant so I have built into the definition of an automorphic form that it has weight 2 and trivial character.

[Kevin Buzzard]

Update: there are a few easy sorries (read: I broke stuff when refactoring) in AutomorphicForm/QuaternionAlgebra/Defs.lean. For example line 41 (proof is "F is in the center of D so if R is some commutative F-algebra (e.g. the finite adeles) then R is in the center of D tensor_F R, so R^* is in the center of (D tensor_F R)^*"), line 57 (proof is in a comment just above, note that we need Algebra.TensorProduct.rightAlgebra as an instance for this to make sense), line 164 (proof is that conjugation is a homeomorphism, this lemma is in the wrong place), and lines 252 to 254 (proof is easy, probably intros; ext; simp or something).

I've started on Hecke operators today, in the branch kbuzzard-hecke-operators (current progress: I wrote the proof that they're well-defined in the module docstring :-) ).

In other news, #20021 is merged and in my opinion we should now refactor the definition of the finite adeles of a number field in mathlib to be this restricted product; the reason is that the definition of the topology is more conceptual and we now get local compactness for free.

[Ruben Van de Velde]

FLT#377 for the easy one

[Ruben Van de Velde]

And FLT#381 for line 57

[Kevin Buzzard]

Thanks! I'm one sorry away from the definition of a Hecke operator!

[Johan Commelin]

Back in the LTE days, you would always remind me "every project starts as a single sorry" :grinning:

[Kevin Buzzard]

We now have Hecke operators! Progress slightly slow at the minute as I'm on holiday :-)

[Ruben Van de Velde]

Only 150 lines, sounds like it must be something trivial :)

[Kevin Buzzard]

They were a little hard-won. Either that or it's hard to find time you work when you're on holiday :-)

[Kevin Buzzard]

OK I've just arrived back in London after a minibreak and I have some sorry-free code which defines Hecke operators and gives a criterion for them to commute, which should be enough in the application to quaternionic modular forms. Sorry for doing very little over the last week. Thanks for the review Ruben! I see there are plenty of PRs which are ready for review; I will hopefully get to these within the next day or two (although Christian Merten is visiting :tada: and I would also like to spend some time talking to him!).

Where we're going here is that Andrew's "abstract" R=T work is now merged, I am working on defining the relevant T and Javier is working on the relevant R, and once these are done we should be able to put it all together and get a theorem of the form "a modularity lifting theorem is true if we can check all of the hypotheses"; these hypotheses will be hard to check, however many of them were known in the 1980s, so basically we are slowly making our way towards the first milestone of the FLT project.

[Kevin Buzzard]

I've been at an education workshop this week and I've also been thinking about local and global fields for the Clay workshop so FLT has been a bit disrupted. On the other hand other people have been making PRs and I've been merging them; we are making progress with adeles. However I have also thrown a huge spanner into the works with #23542 which will break a bunch of code, but which I think is for the best; this will give us a new topology on the adeles whose definition is conceptual rather than ad-hoc, and the underlying type is still basically the same. I am still quietly confident that we have a clear route towards finite-dimensionality of spaces of quaternionic modular forms, and the proof is written in the blueprint and sorried in the repo.

Branch kbuzzard-concrete-hecke-operators is a highly preliminary branch where I will start working on the definition of the Hecke algebra we care about. The work depends on a bunch of sorries, many of which are local (I would advise people against working too much on adelic stuff because the definition will change soon). I was tempted to think about a couple of these myself. Let me explain the mathematics here. Let $K$ be what the experts would call a nonarchimedean local field, but the actual definitions don't matter. What matters is that $K$ is a field with a norm, and it has a ring of integers $R$ which is the closed unit disc and which is also open due to the weirdness of nonarchimedean norms ($|a+b|\leq\max\{|a|,|b|\}$ rather than $\leq |a|+|b|$). The first thing we need is that $GL_2(R)$ is open in $GL_2(K)$ and I started thinking about this in the branch kbuzzard-topology-experiments which I was doing for fun when I was putting off doing a tedious non-FLT-related admin task. My instinct is that because the inclusion $R\to K$ is an open map, perhaps the inclusion $GL_2(R)\to GL_2(K)$ is completely formally an open map, although I didn't get anywhere. I did show that continuity of $R\to K$ gave continuity of $GL_2(R)\to GL_2(K)$ though. This is all just point-set topology I think: is it true that if $M\to N$ is a morphism of topological monoids which is an open map then $M^\times\to N^\times$ is also an open map? Note that $M^\times$ doesn't get the subspace topology from $M$, it gets the subspace topology from $M\times M$ embedded via $m\mapsto (m,m^{-1})$.

You can see my preliminary thoughts on this stuff here.

[Yakov Pechersky]

I was only able to prove the IsOpenMap Units.map under pretty strict conditions, IsLocalHom and Injective:

open MulOpposite in
lemma IsOpenMap.units_map {M N : Type*} [Monoid M] [Monoid N] [TopologicalSpace M]
    [TopologicalSpace N] (f : M →* N) (hf : IsOpenMap f)
    (hf' : IsLocalHom f) (hf'' : Function.Injective f):
    IsOpenMap (Units.map f : Mˣ →* Nˣ) := by
  intro U hU
  rw [isOpen_induced_iff] at hU ⊢
  obtain ⟨U, hU, rfl⟩ := hU
  have : (Units.map f) '' (Units.embedProduct _ ⁻¹' U) =
    Units.embedProduct _ ⁻¹' (Prod.map f f.op '' U) := by
    ext x
    simp only [Set.mem_image, Set.mem_preimage, Units.embedProduct_apply, Prod.exists,
      Prod.map_apply, MonoidHom.op_apply_apply, Function.comp_apply, Prod.mk.injEq, op_inj,
      «exists», unop_op]
    constructor
    · rintro ⟨y, hy, rfl⟩
      refine ⟨_, _, hy, ?_⟩
      simp
    · rintro ⟨a, b, hab, ha, hb⟩
      have ha' : IsUnit a := by
        apply isUnit_of_map_unit f
        rw [ha]
        exact Units.isUnit _
      replace ha : Units.map f ha'.unit = x := by
        ext
        simp [ha]
      have hb' : IsUnit b := by
        apply isUnit_of_map_unit f
        rw [hb]
        exact Units.isUnit _
      refine ⟨ha'.unit, ?_, ha⟩
      suffices ha'.unit⁻¹ = hb'.unit by
        simp [this, hab]
      have : Function.Injective (Units.map f) := by exact Units.map_injective hf''
      replace hb : Units.map f hb'.unit = x⁻¹ := by
        ext
        simp [hb]
      rw [← this.eq_iff, map_inv, ha, hb]
  rw [this]
  refine ⟨Prod.map _ _ '' U, ?_, rfl⟩
  exact hf.prodMap hf.op U hU

[Yakov Pechersky]

Other useful API that I couldn't find otherwise

lemma Function.RightInverse.image_subset {X Y : Type*} {f : X → Y} {g : Y → X}
    (hf : Function.RightInverse f g) (s : Set X) :
    f '' s ⊆ g ⁻¹' s :=
  Set.image_subset_preimage_of_inverse hf _

lemma Function.RightInverse.preimage_subset {X Y : Type*} {f : X → Y} {g : Y → X}
    (hf : Function.RightInverse f g) (s : Set Y) :
    f ⁻¹' s ⊆ g '' s :=
  Set.preimage_subset_image_of_inverse hf _

lemma isOpenMap_induced {X Y : Type*} [TopologicalSpace Y]
    {f : X → Y} (hf : Function.Surjective f) :
    @IsOpenMap _ _ (.induced f ‹_›) _ f  := by
  intro U
  simp only [isOpen_induced_iff, forall_exists_index, and_imp]
  rintro V hV rfl
  rwa [Set.image_preimage_eq _ hf]

@[to_additive]
lemma MulOpposite.isOpenMap_unop {M : Type*} [Monoid M] [TopologicalSpace M] :
    IsOpenMap (MulOpposite.unop (α := M)) :=
  isOpenMap_induced MulOpposite.unop_surjective

@[to_additive]
lemma MulOpposite.isOpenMap_op {M : Type*} [Monoid M] [TopologicalSpace M] :
    IsOpenMap (MulOpposite.op (α := M)) := by
  have h : Function.RightInverse (β := M) MulOpposite.op MulOpposite.unop := congrFun rfl
  have h' : Function.RightInverse (α := M) MulOpposite.unop MulOpposite.op := congrFun rfl
  intro
  simp only [isOpen_induced_iff, subset_antisymm_iff]
  intro hU
  refine ⟨_, hU, h'.preimage_subset _, h.image_subset _⟩

open MulOpposite in
lemma IsOpenMap.op {M N : Type*} [Monoid M] [Monoid N] [TopologicalSpace M]
    [TopologicalSpace N] {f : M →* N} (hf : IsOpenMap f) :
    IsOpenMap f.op := by
  simp only [MonoidHom.op, Equiv.coe_fn_mk, MonoidHom.coe_mk, OneHom.coe_mk]
  exact isOpenMap_op.comp (hf.comp isOpenMap_unop)

instance {M : Type*} [Monoid M] [TopologicalSpace M] : ContinuousInv Mˣ where
  continuous_inv := by
    constructor
    simp only [isOpen_induced_iff, Set.inv_preimage, forall_exists_index, and_imp,
      forall_apply_eq_imp_iff₂]
    intro U hU
    let V := (Prod.map MulOpposite.op MulOpposite.unop) ⁻¹' (Prod.swap ⁻¹' U)
    refine ⟨V, ?_, ?_⟩
    · simp only [isOpen_prod_iff, exists_and_left, MulOpposite.forall, Set.mem_preimage,
      Prod.map_apply, Prod.swap_prod_mk, MulOpposite.unop_op, V] at hU ⊢
      intro x y hyx
      obtain ⟨v, hv, w, hw, hyv, hxw, h⟩ := hU y x hyx
      refine ⟨MulOpposite.op ⁻¹' w, ?_, MulOpposite.unop ⁻¹' v, ?_, ?_, ?_, ?_⟩
      · exact MulOpposite.continuous_op.isOpen_preimage _ hw
      · exact MulOpposite.continuous_unop.isOpen_preimage _ hv
      · simp [hxw]
      · simp [hyv]
      · rw [← Set.preimage_prod_map_prod]
        refine Set.preimage_mono ?_
        rw [← Set.preimage_swap_prod]
        exact Set.preimage_mono h
    · ext
      simp [V]

[Yakov Pechersky]

The challenge with the IsOpenMap without the hypotheses is that for an open set s \in Set (M, M^x), I couldn't well control that the (a, b) \in s, a and b were related multiplicatively

[Yakov Pechersky]

I've generalized the proof to remove the strict assumptions, and pushed to your branch. And used it for your GL use case, where the missing piece is now

lemma _root_.isOpenMap_ringHom_mapMatrix_of_isOpenEmbedding {m α β : Type*} [Fintype m]
    [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β]
    [TopologicalSpace α] [TopologicalSpace β]
    {f : α →+* β} (hf : Topology.IsOpenEmbedding f) :
    IsOpenMap (RingHom.mapMatrix f : Matrix m m α →+* Matrix m m β) := by
  sorry

I have the Topology.IsOpenEmbedding f stronger hypothesis because I think it will be necessary for the proof

[Yakov Pechersky]

So for the bottom of your post:

is it true that if $M\to N$ is a morphism of topological monoids which is an open map then $M^\times\to N^\times$ is also an open map?

My answer so far is yes under the condition that the kernel is trivial. (I _think_ this is weaker than injectivity because we have monoids, not groups, as the domain).

[Yakov Pechersky]

Which is fine in the use case because we're mapping with subtype, which is injective.

[Yakov Pechersky]

I think I have the isopenmap for matrix map proven, I was complicating it for myself getting lost in the pi Topology. But we're in finitely indexed matrices so things are more straightforward

[Yakov Pechersky]

Because the image is the finite set sum of the images of each of the standard basis sets at i, j, which is open by hypothesis

[Kevin Buzzard]

Yakov Pechersky said:

I was only able to prove the IsOpenMap Units.map under pretty strict conditions, IsLocalHom and Injective:

Hmm that's kind of bad because $\Z_p\to\mathbb{Q}_p$ isn't a local hom and this is where we want to apply it. It's certainly true that $\Z_p^\times\to\mathbb{Q}_p^\times$ is an open map. But are you saying you don't need LocalHom any more?

[Kevin Buzzard]

One stupid reason that it's an open map in this case is that the units topology on $\mathbb{Q}_p^\times$ is the subspace topology and the same is true for $\mathbb{Z}_p^\times$. I don't really understand when this is true (it fails for the adeles so I know the answer isn't "always").

[Andrew Yang]

It is true for adic-rings (i.e. rings with the $I$-adic topology for some $I \le J(R)$). See docs#IsOpenUnits.of_isAdic.

[Kevin Buzzard]

That covers $\Z_p$ but not $\mathbb{Q}_p$ (or $\R$). But maybe we only need it for $\Z_p$?

[Andrew Yang]

It is also true (more or less by definition) for topological fields and we also have that: docs#instIsOpenUnitsOfHasContinuousInv₀OfT1Space

[Yakov Pechersky]

No need for IsLocalHom anymore

[Yakov Pechersky]

example : IsOpenMap (Units.map (RingHom.mapMatrix
    (v.adicCompletionIntegers F).subtype).toMonoidHom :
    GL (Fin 2) (v.adicCompletionIntegers F) →* GL (Fin 2) (v.adicCompletion F)) := by
  apply IsOpenMap.units_map
  · exact (Valued.valuationSubring_isOpen _).isOpenEmbedding_subtypeVal.isOpenMap.matrix_map_finite
  · intro x
    apply (map_eq_one_iff ..).mp
    exact (v.adicCompletionIntegers F).subtype_injective.matrix_map ..

is now sorry free, on your branch

[Kevin Buzzard]

So for the last few days I've been working on bumping FLT over the adele refactor, which now landed in mathlib. It's FLT#399 and I'm sorry I've been ignoring everything else! Hopefully this is now ready, I'm going to bed but hopefully it'll have a green tick tomorrow and I'll be able to merge it.

[Kevin Buzzard]

I then want to spend some time trying to understand what Michael Rothgang has been telling me about how to stop all you people from making PRs with lines in which are too long etc (in mathlib such PRs would fail CI).

[Yaël Dillies]

Kevin Buzzard said:

I then want to spend some time trying to understand what Michael Rothgang has been telling me about how to stop all you people from making PRs with lines in which are too long etc (in mathlib such PRs would fail CI).

This can very easily be done. I have the setup in Toric. Should I open a PR?

[Kevin Buzzard]

I'm currently working through what Michael has told me.

[Kevin Buzzard]

(actually no I'm not, I'm still dealing with fallout from the adele refactor)

[Kevin Buzzard]

so sure -- thanks

[Yaël Dillies]

Wait, is CI not passing?

[Kevin Buzzard]

Note FLT#427 -- does this do what you are suggesting doing?

[Yaël Dillies]

No, that's different. I think both approaches are useful

[Kevin Buzzard]

My plan is to (a) merge FLT#434 (b) merge master into FLT#427 (c) merge #427

[Kevin Buzzard]

What are you proposing doing which isn't #427 ?

[Yaël Dillies]

Adding the linters to the lakefile so that people get feedback from the environment linters when writing their code, instead of merely when they push it to CI

[Kevin Buzzard]

But didn't I do that already?

[Yaël Dillies]

I see very few linters in the lakefile. Certainly less than in mathlib!

[Kevin Buzzard]

The ones in mathlib which I don't have are just the ones I didn't yet realise I need.

[Kevin Buzzard]

Don't worry about adding them, I know how to do this, I'll get to it myself. It's CI I don't understand properly.

[Kevin Buzzard]

I'll tell you what you could do -- there is a tracking issue for linters at FLT#418 . Feel free to suggest linters which I didn't realise I need yet.

[Yaël Dillies]

Currently I'm trying to bump FLT past #23603, but there are a bunch of unrelated errors due to, I imagine, the adele refactor

[Kevin Buzzard]

I just bumped -- are you up to date?

[Kevin Buzzard]

FLT#433

[Yaël Dillies]

Ah, I know what happened. I'm working on Javier's fork and it mustn't have been updated

[Kevin Buzzard]

Before I merge anything else I'm merging FLT#434 and FLT#427 and then merging master on lots of PRs, then I think we're going to be (a) past the adele refactor :tada: and (b) with a much better CI/linter set-up (thanks @Michael Rothgang !). Then I need to add some new mathematical issues which have come out of the adele refactor and then I hope to go back to Hecke algebras for a bit.

[Yaël Dillies]

I don't understand how you are on latest mathlib and still importing Mathlib.Topology.Algebra.ClosedSubgroup, given that it's now called Mathlib.Topology.Algebra.Group.ClosedSubgroup

[Kevin Buzzard]

That's because we now have deprecated imports probably :-)

[Yaël Dillies]

but... you have to act on the deprecations :sweat_smile:

[Kevin Buzzard]

not if we're not linting for them!

[Kevin Buzzard]

Where do you see a bad import? Are you looking at current main on my repo?

[Kevin Buzzard]

Oh, are you talking about the stuff I fixed in FLT#434 which I'm about to merge when it passes CI?

[Yaël Dillies]

FLT.Patching.Utils.AdicTopology, I'm fixing it in my bump

[Kevin Buzzard]

You are wasting your time

[Yaël Dillies]

Ah well, I just read the build output

[Kevin Buzzard]

As I already told you, I bumped ten minutes ago, I am about to merge FLT#434 and then I will merge FLT#427 so anything that you do which redoes any of this will not happen

[Yaël Dillies]

All I wanted to do was bumping past #23603, which you did, but without deleting the relevant material from FLT

[Kevin Buzzard]

aah!

[Kevin Buzzard]

Here's something which I find annoying: when I merge FLT#434 I will squash merge it. So in theory you could branch off FLT#434, do the thing which you want to do and then make a new PR, and then when I squash merge it things will get confused, right?

[Kevin Buzzard]

Given that I am actively working on the project right now, maybe you can just wait a bit?

[Yaël Dillies]

I can just rebase, don't worry

[Yaël Dillies]

There you go: FLT#435. I believe it shouldn't conflict with anything you're doing

[Kevin Buzzard]

Looks good -- thanks a lot!

[Kevin Buzzard]

An update of where we are and where we're going.

Big Proof

Over the last week or so I've been thinking about good things to work on before the Big Proof talk on June 9th (4 weeks away). Since the project began I have been focussing on the mathematics behind an "$R=T$ theorem" because this was the insight in Wiles' paper which was historically the last piece in the puzzle for FLT. So what is an $R=T$ theorem?

$R=T$

One explanation of $R=T$ is very simple: it's just an abstract theorem in commutative algebra which says that if you have a bunch of data including commutative rings R and T and a map between them, then under a bunch of hypotheses, this map is an isomorphism. For applications to FLT we don't need it to be an isomorphism, we just need some kind of control over the kernel (e.g. being nilpotent is enough), and we have this abstract theorem in FLT thanks to work of Andrew Yang; it's ker_RtoT_le_nilradical in FLT.Patching.RequalsT. So far so good! But of course we need to apply the theorem to a certain ring $R$ (a deformation ring) and a certain ring $T$ (a Hecke algebra), neither of which have been defined yet (but we're working on it).

Once the deformation ring $R$ and Hecke algebra $T$ are defined, this "bisects" the proof of FLT. There are now, broadly speaking, two tasks (both gigantic) left: (1) check the hypotheses of the abstract commutative algebra $R=T$ theorem are satisfied for these rings (this was where the mistake was in the original 1993 argument) and (2) deduce FLT from the conclusion of the $R=T$ theorem. In actual fact things are slightly more convoluted; one has to apply the $R=T$ result twice to prove FLT for example, in two slightly different situations, and the $R=T$ we're proving is not exactly the same as the one Wiles proved, but it's not unreasonable to ignore these complications if one just wants a feeling for where we are.

So what is the status of the definition of the $R$ and the $T$ in the application?

The deformation ring $R$.

The deformation ring work is in a pretty poor state. I had a student working on it but they have left academia with the work unfinished so now we have to either rescue it or start again. The literature reference we decided to follow was de Smit--Lenstra "Explicit construction of universal deformation rings". Our first goal is Theorem 2.3, the first theorem of that paper (the existence of a universal deformation ring, i.e. the assertion that a certain functor is representable). The functor in that theorem will not be exactly the functor which we want though; we also need to impose local conditions on our deformations, so we also need Proposition 6.1 (deformations which have some property which is well-behaved are also representable). Right now there is no blueprint, nobody working on the project, and a WIP PR containing a huge dump of all the work we have on the project so far, which needs a lot of work. @Andrew Yang was involved with writing a small amount of this code and I've asked him to see how much of it is rescuable; I'm also trying to get @Junyan Xu interested in the project. Anyone who likes the idea of formalizing work of Lenstra (which is always extremely clearly-written) is welcome to join us, although right now there is nothing concrete to do and currently my priorities are elsewhere.

$T$

The situation regarding $T$ is much healthier. Not only are we well along the way towards a definition, but we are also well along the way towards proving one of the hypotheses in the $R=T$ theorem, namely that $T$ is Noetherian. Noetherian-ness will follow from finite-dimensionality of a certain space of automorphic forms, and @William Coram is working on this finite-dimensionality proof as part of his PhD thesis (so please don't anyone else work on it without discussing things with William first). I am part way through the definition of $T$; I've defined "abstract Hecke operators" in FLT/AutomorphicForm/QuaternionAlgebra/HeckeOperators/Abstract.lean and now we just want to get concrete Hecke operators acting on spaces of automorphic forms (which we also have); this shouldn't be too hard, the WIP PR is FLT#446 and getting this over the line is currently third on my job list. I hope to be back on this within a week or so. The reason it's not top priority is that right now I want to work a little more on the prerequisites for the proof of $T$ being Noetherian, which is what I'll finish by talking about.

$T$ is Noetherian

All the work is in proving that a certain space of automorphic forms is finite-dimensional (and I'll say again the thing which I always say, which is that AFAIK there is no Lean proof that classical modular forms are finite-dimensional yet, and it is appealing to me to try and get some fancy automorphic version of this theorem over the line first, just like there was a definition of the p-adic zeta function in Lean before there was a definition of the classical zeta function :-) ). So how do we prove this finite-dimensionality statement?

One possibility is "we just skip it becasue it was known in the 60s" (remember, the rules of the game are that we can assume anything which was known in the 80s, at least until 2029, because that was what I promised EPSRC). But about 6 months ago I made the executive decision that we should do it properly, not least because I knew that it would force us to develop a lot of material about adeles, which I felt was very suitable for mathlib and would be a necessary prerequisite for a lot of other stuff (class field theory, Tate's thesis, the Langlands program in general).

To be honest, I now feel a bit conflicted by this decision. For me, one motiviation for trying something as daft as proving FLT in Lean was that I knew that a consequence would be that mathlib grew in the direction which I wanted it to grow, i.e. towards number theory. But this has made me really try and figure out the correct generality for everything, i.e. doing stuff "the mathlib way" even though that's not completely necessary, and as a result we now have a really robust theory of adeles including some quite subtle theorems about them. For this work I should thank @Matthew Jasper , @Salvatore Mercuri and @Madison Crim who between them have supplied a lot of the harder and more technical results, together with @Aaron Hill, @Yakov Pechersky and @Ruben Van de Velde who did some of the simpler ones. This kind of collaboration shows that the set-up really does work; people are able to contribute genuinely helpful stuff even if they're not number theorists. Modulo some technical statements about topology on restricted products, which are second on my job list unless Matthew gets to them first, we are almost over the line here, and assuming this stuff ultimately makes it into mathlib then this will in some sense be the second serious contribution to mathlib which FLT has produced (the first was Frobenius elements in some absurd generality following Bourbaki, which was mostly done in FLT by me and then completed and merged into mathlib by @Thomas Browning ). If I need any more results on adeles then I'll open tasks, but I think that after Matthew's heroic work on $L\otimes_KK_v=\prod_{w|v}L_w$ it might be all downhill from here (although of course upstreaming will present its own challenges; ideally we'll find another person who wants a bunch of the theory of adeles for their own project and is motivated to just upstream the material themselves; see the blueprint for an explicit description of what our goals are; all of these theorems are now very close).

But a robust theory of adeles isn't enough for finite-dimensionality, we also need a bunch of results about additive Haar measure on topological rings. Here @Yaël Dillies and @Andrew Yang have been key players, and mathlib already has docs#MeasureTheory.distribHaarChar . But we still need a bunch of results about this and related functions, and this is where my efforts are currently going. I am about to open a bunch of new tasks related to Haar characters; I will report on them in the Haar character miniproject thread. Again probably the hardest one will be about Haar characters of restricted products; I thank @Anatole Dedecker for his beautiful work getting those into mathlib; it meant that we had to completely refactor the finite adeles and hence the adeles, which broke everything, but it was definitely worth it.

In my talk on June 9th I'll give an update on where we are with all of this; my dream scenario would be that we have a definition of the Hecke algebra T, a proof that it's Noetherian, and a plan for getting the definition of the deformation ring R over the line.

[Matthew Jasper]

I haven't come up with anything general for the topology for restricted products. I'm probably going to start on some of the algebra results we still need before dealing with continuity.

[Anatole Dedecker]

I can’t guarantee availability, but I can probably help with some continuity results (I believe Kevin wrote down what is needed, I just need to find some time to think about it)

[Kevin Buzzard]

My memory is that I have not written down (even informally) exactly the results for topology and restricted products which we need to get base change for adeles over the line as a topological statement. For the haar characters there is an informal statement here but over the next day or two I will be working on writing down formal statements of everything which remains in the Haar character miniproject, so then it will just be some concrete sorries to fill in.

[David Michael Roberts]

Kevin Buzzard said:

For applications to FLT we don't need [R -> T] to be an isomorphism, we just need some kind of control over the kernel (e.g. being nilpotent is enough)

Noob question: you still need surjectivity of R -> T, I guess?

[Andrew Yang]

Yes but that is (relatively) much easier.

[Kevin Buzzard]

Surjectivity can be thought of as "every Galois representation that comes from a modular form, is a Galois representation". Injectivity can be thought of as "Every Galois representation, comes from a modular form".

[Kevin Buzzard]

It's not quite as simplistic as that because you can have finite errors but that's the naive idea.

[Kevin Buzzard]

OK so 13 new Hecke algebra tasks just dropped (see the Outstanding tasks V8 thread). Having got a definition of Hecke algebras which contains no sorried data I'm now going back to Haar characters for a bit and then adeles; I hope to review both of those miniprojects before my big proof talk in 8 days. Basically everything that we have done in 2025 has been working towards a sorry-free proof of the statement that a certain ring is Noetherian and hence that the deformation theory which Andrew Yang has been setting up in FLT#504 (now merged :tada: ) will apply to the Hecke algebra.

Andrew has made the quite pertinent point that the fact that this Hecke algebra is Noetherian was known in the 1980s (indeed probably in the 1960s) and hence in theory I didn't need to spend so much time on the work. When I said "reduce FLT to theorems from the 1980s" what I had in my head was "reduce FLT to a small finite list of hard theorems" rather than "reduce FLT to hundreds of statements ranging from the simple to the profound, all of which were known in the 1980s", and I think we do now have a viable path towards a sorry-free proof that the Hecke algebra is Noetherian.

However I'm going to try something else next, and perhaps try romping through statements of some or maybe even all of the main theorems which we will need to prove, or at least make progress on, over the next few years, and here I might start skipping "medium-length sorries" for a while, i.e. "stuff which could be proven in a couple of lectures in a fast-paced graduate course", with the logic being "if it was known in the 1980s then sorry it, open an issue and point to a proof in the literature". So the nature of the project will change. However there will still be plenty to do; according to the project dashboard there are 25 uncompleted tasks of which 14 are unclaimed, and whilst most of these tasks are reasonable (i.e. can be done in one or two sittings) there are some which I think will inevitably break up into more tasks. I certainly intend to still "manage" work on those tasks (i.e. reviewing PRs, offering advice etc) whilst we launch off into the unknown in the post Big Proof era.

Looking forward, I think that some of the biggest issues I face are that various definitions (such as continuous cohomology, the local Artin map, and local fields) are not in mathlib, preventing me from properly stating theorems. There has been progress in all of these areas but I am still a bit edgy about sorrying definitions.

[David Michael Roberts]

I just watched a lecture series by Colin McLarty from last year, and he referenced your project, in the context of the conjecture FLT is provable in formal arithmetic. It would be interesting for logicians to get access to the formal proof that's being written and see if each component is really doable in say PA.

[David Michael Roberts]

McLarty wrote a paper showing that SGA4 could be done with much less than ZFC as a foundation (the only real part of this is proving derived functor cohomology didn't need universes, but in fact much much less). But of course, if you only need étale cohomology in very restricted examples, stronger statements will be possible.

[David Michael Roberts]

I could foresee someone analysing the R=T theorem from this project and showing it has weak logical strength, and then one is reduced to examining your "assumptions" theorems etc individually.

[Kevin Buzzard]

The R=T theorem is just an abstract theorem in commutative algebra, it only needs rings and modules, it doesn't need anything

[David Michael Roberts]

Hmm, maybe I mean together with the stuff about adeles, quaternionic modular forms etc. That's not pure algebra. So not just the abstract R=T theorem, but the actual application of it.

[Matthew Jasper]

https://github.com/matthewjasper/FLT/tree/finite-adele-basechange-outline has my progress on showing that the finite adele base change is bijective, it needs current restricted product work to settle down a bit (as well as clean up) before it can be a PR, but I'm posting it here to hopefully save Kevin from duplicating all of the work.

[Kevin Buzzard]

Thanks! Having been distracted by Hecke algebras last week, I spent the weekend distracted by haar characters but am desperate to get back to adeles

[Michael Rothgang]

ImperialCollegeLondon/FLT#605 and ImperialCollegeLondon/FLT#612 bump mathlib (the latter to current mathlib). On top of this, ImperialCollegeLondon/FLT#613 adopts mathlib's hot-from-the-press linter sets: you can enable all of mathlib's syntax linters in one line, this updates as mathlib adds (or disables) new linters, and it appears a tad faster also.

[Michael Rothgang]

ImperialCollegeLondon/FLT#614 adds shake to PR CI

[Rémy Degenne]

I was not sure how to use the new linter set in my projects, to thanks @Michael Rothgang for the example in ImperialCollegeLondon/FLT#613!
Perhaps it would be worth making a post in general to advertise that mechanism more broadly?

[Kevin Buzzard]

Thanks! Yesterday was the first day in a long time that I didn't do any FLT and I see things are piling up!

[Kevin Buzzard]

OK so I know the PRs are still piling up but I wanted to get the Haar character miniproject graph broadly representing the project before Monday; this is now over the line.

I think it's becoming pretty clear that a goal we're working towards is a paper on current progress towards a modularity lifting theorem. One key missing part right now is the statement that the Hecke algebra is a Noetherian commutative ring and I feel like this should be sorry-free before we can really say that we have reached an R=T milestone. The wy I've set it up, It involves essentially all of the results in the adele and Haar character projects. In these projects we've proved things in more generality than what we've needed -- but I would say that we've proved them in the correct generality. I wanted to use the R=T application as an excuse to build up the theory in the correct generality so that mathlib benefits too (a lot of the work we've done here will be useful for a future project on Tate's thesis, for example).

After Big Proof I'll be back focussing on the adele miniproject and trying to work out exactly what is needed and where we are. I will also create the remaining tasks for the Haar character project. This task-collection busywork ("find a sorry, create an issue, describe the problem, mark it WIP, put the issue number in the LaTeX and the Lean, repeat for lots of sorries, make a PR, merge the PR, go through all the WIP issues and mark them not WIP, put them on the dashboard") is kind of tedious but also extremely rewarding because the community is reacting so positively to my task-posting. For example twice in the last month or so I just dumped over 10 new tasks on the project dashboard and within a week or so most of them had been claimed.

[David Michael Roberts]

Big Proof talk: https://www.youtube.com/live/r-Vu_4sJuuI?si=Gp_gJYuSwZZN2wmD with Kevin taking the stage at 16:50

[Kevin Buzzard]

Sorry things have been slow for the last two weeks. I was away in Cambridge last week, away last weekend, away for two days this week in Southampton and away this weekend so I'm barely keeping my head above water. I've reviewed some of the many outstanding PRs today and on Monday things will be back to normal with me spending most of my time thinking about FLT-related things. Apologies to those who have been waiting two weeks or more for reviews.

[Kevin Buzzard]

So I reviewed a bunch of PRs. One new functionality is that if people need movement at my end then they should write awaiting-review on the PRs and then they'll get the awaiting-review tag which I will see (and which will remove an awaiting-author tag). If I think it's your move I'll tag awaiting-author (which will remove an awaiting-review tag).

FLT#73 the ball is in your court @Ruben Van de Velde right? FLT#562 it's your move @Anatole Dedecker right? FLT#607 is this ready for me @Matthew Jasper ? I keep not noticing it because it's awaiting-author and my github notifications are completely out of control since Big Proof (I have hundreds of unread notifications unfortunately). FLT#614 is this waiting for you @Michael Rothgang ? FLT#615 is this waiting for you @Andrew Yang ? FLT#617 this is failing CI @William Coram . If it's ready for review can you get rid of the awaiting-author tag and fix CI? @Matthew Jasper FLT#633 has merge conflicts and is failing CI so I keep not reviewing it. @Kenny Lau FLT#635 is awaiting-author.

I have not looked at things from #649 onwards and will try to find time to do this on Monday (I'm away this weekend).

[Kevin Buzzard]

Advanced warning: from 12th to 19th July I'm away on a family holiday and from 21st to 25th I'm running a class field theory workshop, so actually a lot of my Lean time is going into reviewing mathlib PRs which I want over the line before that workshop starts. Obviously these things (group cohomology, group homology, Tate cohomology, local fields etc) are going to be relevant for FLT but right now there are no (public) concrete things for people to work on; indeed there is a list of things but Richard and I are suppressing it right now, so that people have things to do during the workshop :-) After the workshop everything will be public and there will be some cool local field goals. Mathlib still doesn't have the definition of local fields though :-)

[Matthew Jasper]

FLT#607 is waiting for you, FLT#633 is definitely waiting for me, I'll get it after 607 is merged

[Ruben Van de Velde]

Thanks for the reminder, I actually managed to finish FLT#73 yesterday

[Kevin Buzzard]

I'm getting on top of recent PRs -- thanks to everyone for making them (especially to the new folks) and thanks for your patience. Usually I am quick to move on these things but right now I am finding that all my Lean time is going into preparing for the Oxford class field theory workship which is happening 21st to 25th of this month July; I am spending most of my time reviewing relevant mathlib PRs and contributing to the secret CFT repo which will be made public during the workshop. I am very conscious of the fact that there are essentially no unclaimed tasks on the FLT dashboard but right now I don't want to dump a bunch of class field theory-related tasks there because I want to save them for the workshop attendees. By the end of this, we are going to have nonarch local fields in mathlib plus a bunch of API, which is a great step in the right direction. In fact we already have nonarch local fields: currently they're spelt like this

variable (K : Type*)
  [Field K] [ValuativeRel K]
  [UniformSpace K] [IsTopologicalDivisionRing K]
  [LocallyCompactSpace K]
  [CompleteSpace K] [ValuativeTopology K]
  [ValuativeRel.IsNontrivial K]
  [ValuativeRel.IsRankLeOne K]
  [ValuativeRel.IsDiscrete K]

and whilst it looks complicated, the breakthrough is that we have not had to fix a target monoid-with-zero as the target of the valuation.

If anyone wants a challenge, they could prove that the completion of a number field at a finite place of its ring of integers satisfies the above :-)

[Kevin Buzzard]

Woohoo, I finally reviewed all the PRs which had accrued! I am busy for the next two weeks so no doubt more things will accrue. If there are people who are looking for things to do then we have an ever-growing Mathlib folder... :-/

[AbdulShabazz]

:grinning:

[Kevin Buzzard]

So I'm back in London this week and my main goal is again to get on top of all the open PRs, given that next week I am away again :-/ . If you have an open PR with no conflicts and which is passing CI, expect it to be looked at today or tomorrow. Sorry for the delays, summer has been full of non-Lean-related events :-/