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!