miniproject: adeles

Stream: FLT

[Kevin Buzzard]

Finally we have some new tasks for FLT! Check them out on the project dashboard. They are results which we need about Dedekind domains and their completions at maximal ideals. To see an overview of the mathematics, see the blueprint chapter associated to this miniproject. The ultimate goal is to prove that if $L/K$ is a finite extension of number fields then $\mathbb{A}_K\otimes_KL=\mathbb{A}_L$ but we're currently a long way from this; all of the tasks I just released say nothing about adeles.

Perhaps I'll say a word about the dashboard. We have a new workflow for contributing to FLT, because other people maintaining projects have complained about the amount of work it is maintaining the "outstanding tasks" threads. The explanation is here and I heartily thank Pietro for setting everything up. In short, you don't need to look on Zulip to see the current status of things, you can just look directly at the project dashboard. If you want to work on a project, then claim it, to ensure that we don't duplicate effort. You claim it by posting the message claim on the relevant github issue.

This thread is a fine place to talk about issues relating to the five new tasks and more generally about the adeles "miniproject". I'll say more about miniprojects in the "update" thread which I'm about to write.

[Shreyas Srinivas]

I looked at that contribution file. It seems it doesn't contain my addition about how to propose new tasks

[Shreyas Srinivas]

The equational theories contributing.md file has a third bullet point in item 1

[Kevin Buzzard]

I think that I'm the one proposing new tasks rather than the general public, at least at the minute.

[Shreyas Srinivas]

I wanted people to be able to propose their own tasks by creating issues (which GitHub allows on all public repos anyway), and discuss them on zulip. Then maintainers can add them as project tasks

[Shreyas Srinivas]

You will want it soon. There will be all sorts of big and small tooling changes people will suggest and you wouldn't want to spend time writing it up

[Shreyas Srinivas]

At the same time you want maintainers to be Gandalfs who decide which issues they let into the project dashboard. That's my main idea behind it

[Shreyas Srinivas]

Sometimes people find bugs and mistakes

[Shreyas Srinivas]

It's more convenient to have the option to allow people raise issues and discuss them here and you add them to the dashboard if it is worth it

[Andrew Yang]

I'll record my findings(?) today here.
First of all adicCompletionComapRingHom is not general enough. It should be

noncomputable def adicCompletionComapRingHom
    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
    adicCompletion K v →+* adicCompletion L w

This is an easy fix.

Then we need the behaviour of the extended valuation. If I'm not mistaken, it is

lemma v_adicCompletionComapAlgHom
  (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) (x) :
    Valued.v (adicCompletionComapAlgHom A K (L := L) v w hvw x) ^
    (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) = Valued.v x := sorry

A proof strategy is to show that they are both extensions of v so they are equal, but you will need to show continuity etc and I'm not sure how much work this actually is.

After all this I have the "easy direction" of 8.5 depending on the sorry above.

[Andrew Yang]

The draft is in FLT#229.

[Kevin Buzzard]

@Andrew Yang it would be easier if I could refactor the definitions now and push to main -- are you OK with that? (or do you want to make a PR which does this?). I agree your changes are better. I need them because I want to write a bunch more tasks for this miniproject.

To everyone else: I finally found time to work on FLT, and expect to have more time soon; I am finally finding my feet. The reason there's some activity is that I'm currently giving lectures on FLT so people attending the lectures are working on sorries. The course finishes in two weeks' time.

[Andrew Yang]

You can just extract the relevant stuff from that draft and merge them. I’m away from my laptop for another ~2 hours

[Kevin Buzzard]

OK I put part of your work into main -- I was then going to merge it to your PR but it's from a fork so I don't think I can. Hopefully shouldn't be too painful to unravel -- I moved a subst a bit higher in the first proof but that was it.

[Javier Lopez-Contreras]

Just as an FYI for whoever is interested, our adicCompletiontTensorComapAlgIso and adicCompletionComapAlgIso_integral(aka Theorem 5.12 of https://math.berkeley.edu/~ltomczak/notes/Mich2022/LF_Notes.pdf) seem to be a shadow of a more general result in commutative algebra, consequence of Artin-Rees thm. https://math.stackexchange.com/questions/2545914/completion-and-tensor-product

[Javier Lopez-Contreras]

At least the first part of it. You still need to prove that the completion of B with respect to the filtration given by p^i B splits as product of B_w. @Andrew Yang Do you think this is worth having in mathlib?

[Javier Lopez-Contreras]

Andrew Yang said:

I'll record my findings(?) today here.
First of all adicCompletionComapRingHom is not general enough. It should be

noncomputable def adicCompletionComapRingHom
    (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) :
    adicCompletion K v →+* adicCompletion L w

This is an easy fix.

Then we need the behaviour of the extended valuation. If I'm not mistaken, it is

lemma v_adicCompletionComapAlgHom
  (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (hvw : v = comap A w) (x) :
    Valued.v (adicCompletionComapAlgHom A K (L := L) v w hvw x) ^
    (Ideal.ramificationIdx (algebraMap A B) (comap A w).asIdeal w.asIdeal) = Valued.v x := sorry

A proof strategy is to show that they are both extensions of v so they are equal, but you will need to show continuity etc and I'm not sure how much work this actually is.

After all this I have the "easy direction" of 8.5 depending on the sorry above.

For adicCompletionComapRingHom isn't it the exact same? Why do you "unfold" the v = comap A w?

[Kevin Buzzard]

It's easier to apply if the proof isn't forced to be rfl

[Andrew Yang]

Javier Lopez-Contreras said:

At least the first part of it. You still need to prove that the completion of B with respect to the filtration given by p^i B splits as product of B_w. Andrew Yang Do you think this is worth having in mathlib?

This is definitely worth having in mathlib but I'm not convinced it is applicable here.

[Kevin Buzzard]

This just changes the content to proving that $L_v=\oplus_{w|v}L_w$, which still needs an argument.

[Javier Lopez-Contreras]

Yep I agree

[Javier Lopez-Contreras]

But in my opinion it is a slightly cleaner uncoupling. On the other hand, it makes my immediate job a bit harder (but I'll figure it out, maybe asking Andrew)

[Andrew Yang]

The statement quoted above is $M \otimes \lim\limits_{\longleftarrow} R/m^i = \lim\limits_{\longleftarrow} M/m^iM$ (which should follow from Mittag-Leffler if M is finitely presented and no conditions on R), but I'm not immediate seeing how you can get $L \otimes_K K_v = L_v$ from this. I'm not even certain if I know what $L_v$ means.

[Kevin Buzzard]

The proof is rfl ;-) so that's what it means. Alternatively you can do the projective limit of O_L/v^n (v thought of as an ideal of O_L) and then take the total ring of fractions.

[Kevin Buzzard]

OK I am beginning to get the hang of this.

The adele miniproject is now highly fleshed out. You can see on the project dashboard that there are now 16 tasks for people to claim. Some of them are completely elementary (for example one is to prove that an integer y with |y|<1 is zero), others are easy if you are not intimidated by the material (for example one task is "prove that $\mathbb{Q}$ is dense in the intimidating topological $\mathbb{Q}$-algebra $\mathbb{A}_{\mathbb{Q}}$ assuming that there's an open set $U$ whose intersection with $\mathbb{Q}$ is $\{0\}$"; the proof is "for all $q$ we need to find an open whose intersection with $\mathbb{Q}$ is $\{q\}$; use $U+q$". And there's a couple of proofs which are nontrivial but I give LaTeX references (or in one case, a reference to another Lean repo).

I've been giving a course on FLT all term and it's supposed to be on Teams and inaccessible to Joe Public but I've got so exasperated with Teams that I've switched to Zoom. The next lecture is in about 14 hours at 2024-12-02T13:00:00Z and it's two hours long. The Zoom link is here if anyone is interested. Usually I say some waffle and then people break into groups, claim things on the dashboard and work on them.
On Monday I'm going to go through why we need all these results about adeles with an application to quaternionic modular forms. The big theorem we want is that the space of quaternionic modular forms of a given weight and level is finite-dimensional. If you don't know what an adele is then you probably won't get much out of the lecture, but feel free to claim issues anyway.

The last lecture will be on Monday 9th Dec, live from the Hoskinson center at Pittsburgh, if that's Ok with Jeremy Avigad!

[David Michael Roberts]

(OT: I share your exasperation with Teams, sadly my company is moving over to it, away from Slack...) But thanks for making the last lecture public, that's very cool.

[Kim Morrison]

How do I claim a task? I couldn't work it out. In any case, FLT#255 is closed by FLT#260.

[Michael Rothgang]

See CONTRIBUTING.md. TL;DR: write a comment containing just the word claim. You can only claim one task at a time.

[Kevin Buzzard]

The problem with Teams is that (a) Teams seems to be really confused about whether my login is k.buzzard@imperial.ac.uk or [the actual userid I use to log in]@ic.ac.uk and (b) I now have accounts at four universities and I need to switch from Imperial to Oxford to log in. Anyway, this is all moot, we're not using it any more, we're going public :-)

[Ahmad Alkhalawi]

Will the lectures be recorded?

[Kevin Buzzard]

The first six weren't and I had no intention of recording this one either. There's not really anything to see, I'll do a bit of maths (not much) and then we'll have a chat about who's doing what and then for most of the time we go and work in small groups.

[Ruben Van de Velde]

Kim Morrison said:

How do I claim a task? I couldn't work it out. In any case, FLT#255 is closed by FLT#260.

Was https://github.com/leanprover-community/mathlib4/issues/11573 the issue you hit?

[Kim Morrison]

Yes, that was the one! I've since taught omega how to work around this, but we should fix it.

[Ruben Van de Velde]

(This is now, in case you enjoy seeing Kevin fight with Zoom)

[Andrew Yang]

I'm still trying to get in.

[Kevin Buzzard]

Ok I feel like we are now well on the way with the adele miniproject. Here's a summary of where we are and where we're going.

In December I made an effort to "blueprintize" this miniproject, one of whose goals is $L\otimes_K\mathbb{A}_K=\mathbb{A}_K$. I created lots of tasks from issues on the project dashboard. I've recently realised that actually this system has worked, all tasks have been claimed.

The tasks were of several types. Firstly there were tasks which were easy, which were often done very quickly. Then there were tasks which turned out to be reasonable, and these were picked off over a period of time. Then there were tasks which were unreasonable, perhaps because the proofs were very long or because the theory had not settled down enough. For example FLT#231 is $L\otimes_KK_v=\prod_wL_w$, whose original proof in the blueprint was something like "this is standard", and a later proof was "here's a sketch proof I copied out of some notes" but really the proof should be "here is a detailed argument which involves splitting things up into many smaller parts each of which could be an issue in themselves". Another spanner in the works was the refactoring of adeles, which has meant that arguments about topologies on adeles need to be rerouted. I think that this "noise" can really be traced back to my inexperience of running a project like this.

But the bottom line is that there are no unclaimed tasks right now, and those tasks which turned out to be unreasonable are now far better understood. So what I want to work on right now is:

1) More Latex, explaining more details of what needs to be done to get all the goals in the adele miniproject https://imperialcollegelondon.github.io/FLT/blueprint/Adele_miniproject.html over the line.

2) Then more stubbed-out Lean code containing concrete sorries and linked to the miniproject.

3) And then more tasks.

This work is going on in WIP PR FLT#445 . Once this is completed we should have a host of new issues. I should warn people that I have to give two talks in the next week which will slow down my progress a bit, and what I'm proposing does involve a fair bit of work (I need to think about mathematics, and LaTeX, and Lean, and github) but hopefully by the end of next week this PR will be merged and then we'll have a much clearer path towards goals 1--4 of the miniproject.

Goal 5 is to get everything into mathlib; right now I haven't started thinking about a strategy for this, because clearly 1--4 come first.

[Ruben Van de Velde]

Re: goal 5 - is there code that's ready to (be cleaned up and) be moved to mathlib now?

[Kevin Buzzard]

A lot of stuff relies on $L\otimes_KK_v=\oplus_wL_w$ which is not sorry-free, and it might be a while before it is sorry-free because e.g. we will need stuff like $[L:K]=ef$ for complete discretely-valued fields which I have not even stated in Lean yet (and right now in the mathlib4 thread about finite extensions of Q_p I'm still trying to establish the mathlib-idiomatic way to talk about things like the class of fields for which this is true).

I think something which is definitely ready to be upstreamed is semi-algebra maps. I don't really even know why we don't have them in mathlib. We have semilinear maps and then linear maps, and we have algebra maps but for some reason never did semialgebra maps. This is FLT/Mathlib/Algbra/Algebra/Hom and I don't know if PRing it will then result in a push for algebra maps to be refactored to use them.

In general stuff in FLT/Mathlib/* is supposed to be "pretty much ready for mathlib but someone needs to PR it", and the name of the file in that directory is supposed to be a guide as to where it goes in mathlib. In an ideal world FLT/Mathlib/X.lean just has one import, import Mathlib.X, and that's where it's supposed to be.

[Yakov Pechersky]

I really like KConrad's sketch here regarding classification of nonarchimedean local fields of char 0: https://math.stackexchange.com/a/3121202/1452351. That will hopefully help with n = ef. I have some directions into this at #22231, #22232, #22233

[Kevin Buzzard]

I'm going through the entire adele miniproject and trying to write down more bite-sized Lean statements of what we're missing, and opening issues/unclaimed tasks for them. I've just merged four more sorries to main and opened four more issues, FLT#448 to FLT#451 . The set-up for the first 2 is A is a Dedekind domain, v a nonzero prime and a valuation, K the field of fractions, completion K_v, integer ring O_v. The first claim is that there's a map from A/v to the residue field of O_v and the second is that it's a bijection. Now specialize to the case of K a number field and A its integer ring. The third issue is the claim that the residue field of O_v is finite (and the proof is easy, we know A/v is finite and we know it's isomorphic to the residue field) and the fourth is the deeper claim that O_v is compact, which I guess @Salvatore Mercuri must have thought about already because he's already proved the consequence that the adeles are locally compact.

There's no LaTeX proof for this stuff, but I gave proofs in the issues pages on github.

The plan is to open a bunch more issues pertaining to the adele miniproject and also get the LaTeX up to date and make the blueprint graph for the adele miniproject more interesting (right now it's https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_8.html and is missing lots of edges (and several vertices); I hope to fix this with FLT#445, a WIP PR editing the LaTeX).

If someone tries to claim an issue by typing claim in the github issue, and nothing happens, then can you let me know? I am always worried that the system doesn't actually work (I still haven't really got the hang of tokens)

[Aaron Hill]

claim didn't seem to work: https://github.com/ImperialCollegeLondon/FLT/issues/450

[Matthew Jasper]

For FLT#451 there's already Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField that gets most of the way there (IsDiscreteValuationRing is harder and it's probably worth working out how we want to prove it).

[Matthew Jasper]

I might end up doing FLT#448 and FLT#449 when showing global e = local e

[Matthew Jasper]

But I guess they're open if anyone really wants to work on them

[Pietro Monticone]

Aaron Hill said:

claim didn't seem to work: https://github.com/ImperialCollegeLondon/FLT/issues/450

This is likely due to a PAT_TOKEN expiration issue: 30 days have passed since it was last generated. Please @Aaron Hill wait for @Kevin Buzzard to generate a new one. Sorry for the inconvenience.

[Yakov Pechersky]

(IsDiscreteValuationRing is harder and it's probably worth working out how we want to prove it).

docs#Valued.integer.isPrincipalIdealRing_of_compactSpace. Ah, but you don't have complete.

[Matthew Jasper]

But we don't know it's compact

[Matthew Jasper]

We do know complete

[Yakov Pechersky]

docs#Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrdered

[Matthew Jasper]

Yes, there's that, but I'm wondering whether IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization would actually be easier

[Yakov Pechersky]

#455 for #448

[Matthew Jasper]

Once my current pr is done I'll create a pr to outline the rest of the FLT#231 proof so that anything that's shared only exists once in FLT.

[Salvatore Mercuri]

Kevin Buzzard said:

The plan is to open a bunch more issues pertaining to the adele miniproject and also get the LaTeX up to date and make the blueprint graph for the adele miniproject more interesting (right now it's https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_8.html and is missing lots of edges (and several vertices); I hope to fix this with FLT#445, a WIP PR editing the LaTeX).

Heads up that I'm currently writing up the infinite adele base change in the blueprint, so feel free to leave that part unedited in your WIP PR! It's nearly there so should have a PR in the next couple of days

[Kevin Buzzard]

Oh many thanks! I've been mostly working on the finite adele part but I was going to move onto the infinite part afterwards; I'll skip and go straight onto the compact discrete stuff. Did you see my WIP PR FLT#455 ? I've unfortunately been a bit derailed by having to give two talks in the next week (one in Cambridge and a big one in Oxford) but we'll get there. My plan today is to get https://imperialcollegelondon.github.io/FLT/blueprint/dep_graph_chapter_8.html looking less ridiculous so I will probably merge 455 today after I've drawn in some more lines.

[Kevin Buzzard]

Ha ha you can tell I'm giving a talk in 30 minutes -- I've just merged FLT#455 and hopefully by the time the talk starts the blueprint graph for chapter 8 will be essentially connected (if my local calculations are correct it will have one very large connected component and then just a small thing proving it's locally compact).

[Kevin Buzzard]

I specifically didn't merge the three PRs which came in over the last day or two so I should show that it wasn't just me making PRs ;-)