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 ;-)

[Kevin Buzzard]

I've been at an education workshop all day so didn't have any time for FLT but on the tube home I worked out a plan for proving that $\mathbb{A}_L$ has the $\mathbb{A}_K$-module topology, which is what is needed to show that the algebraic isomorphism $L\otimes_K\mathbb{A}_K=\mathbb{A}_L$ is also a homeomorphism (the tensor product gets the $\mathbb{A}_K$-module topology by definition). Nothing in Lean yet but I thought I'd write down the maths (quicker to sketch here than do the LaTeX).

Matthew has already reduced the question to proving the analogous result for the finite adeles. Let $B$ be the integers of $L$ and $A$ be the integers of $K$. Then the finite adeles $\mathbb{A}_L^\infty$ are a restricted product over the type $W$ of finite places of $B$ and the finite adeles of $K$ are a restricted product over $V$, the finite places of $A$, and step 1 is to get these restricted products over the same set. This will follow from

Lemma: if $V,W$ are arbitrary, if $r:W\to V$ is a map with finite fibres, if $L_w$ are sets with subsets $B_w$ and if $M_v$ are sets with subsets $C_v$ and if we're given bijections $M_v\to\prod_{w:r(w)=v}L_w$ which induce bijections $C_v\to\prod_{w:r(w)=v}B_w$ then there's an induced bijection on the restriced products $\prod'_w(L_w,B_w)\to\prod'_v(M_v,C_v)$. Here I'm taking the cofinite filter, probably there is some generalization. Furthermore if $L_w$ and $M_v$ are topological spaces and the bijections on the factors are all homeomorphisms then the induced map on the restricted products is also a homeomorphism.

Corollary: $\mathbb{A}_L=\prod'_v(B\otimes_AK_v,B\otimes_AA_v)$ is a homeomorphism.

My original plan was now to prove some result of the form "If $M_v$ are modules over the rings $K_v$ and the $M_v$ have submodules $C_v$ which are modules over the subrings $A_v$ then $\prod_v'(M_v,C_v)$ is a module over $\prod'_v(K_v,A_v)$ and if everything has a topology and we possibly throw in some more conditions like $C_v$ or $A_v$ being closed or open or both and if all the $M_v$ have the $K_v$-module topology and all the $C_v$ have the $A_v$-module topology then the restricted product module has the module topology over the restriced product ring". This would be enough. But I have no real feeling for whether this is likely to be true.

What I realised today when beginning to think about how to deal with all this was that actually it suffices to prove this.

Lemma: If $X_v$ and $Y_v$ are top spaces with subspaces $A_v$ and $B_v$ then the obvious identification of $\prod'_v(X_v\times Y_v,A_v\times B_v)$ with $\left(\prod'_v(X_v,A_v)\right)\times\left(\prod'_v(Y_v,B_v)\right)$ is a homeomorphism, where the all the restricted products have Anatole's topology and the binary product on the RHS has the product topology.

I think this should be easy, I convinced myself it was a fairly straightforward exercise. Then by induction you get some analogous statement with a product of $n$ things, and then you just pick a basis of everything and get $B\otimes_AK_v=K_v^n$ identifying $B\otimes_AA_v$ with $A_v^n$ homeomorphically, and all you now need to prove is that the restricted product of homeomorphisms is a homeomorphism which should be straightforward. Here we need that a f.g. torsion-free module over the PID $A_v$ is free but we have this. We also need things like $B\otimes_AM=L\otimes_KM$ for $M$ a $K$-module but I already wrote this stuff up in the blueprint.

So this seems to me to be a coherent (hopefully) plan for the last of the mathematical details which are not currently in LaTeX form. I thus propose to spend my time getting all the LaTeX above into the blueprint and then creating all the remaining sorries for the adele and Haar character miniprojects and we can then see how many of these projects we can get over the line by June 9th.

[Kevin Buzzard]

I've been taking stock of where we are with the adele project. I'm on holiday right now but during the flight I found a pretty cool error which I'd made so I thought I'd hop online to explain it because it's quite fun.

We still don't have a sorry-free proof of the algebraic isomorphism $L\otimes_K\mathbb{A}_K=\mathbb{A}_L$ but we're close. Tensoring with $L$ over $K$ is slightly inconvenient with restricted products, because the subrings $\mathcal{O}_v$ of $K_v$ are not $K$-modules, so it is probably easier to tensor with $B$ over $A$, because everything in sight is an $A$-module. So the set-up is this. Let $L/K$ be a finite extension of number fields, with integer rings $B/A$. By work of Matthew we have $B\otimes_A A_v=\prod_{w|v}B_w$ and $B\otimes_A K_v=\prod_{w|v}L_w$, so to get $B\otimes_A\mathbb{A}_K=\mathbb{A}_L$ we just need to prove some statement about how tensor product commutes with restricted product.

@Madison Crim has taken the first step in this direction. She has shown in FLT/DedekindDomain/FiniteAdeleRing/TensorPi.lean that tensoring with finitely-presented modules commutes with arbitrary products of modules. More precisely if $R$ is a fixed commutative base ring and we have a family of $R$-modules $N_i$ and a finitely-presented module $M$, then we have an isomorphism $M\otimes_R(\prod_i N_i)=\prod_i (M\otimes_R N_i)$.

What remains then is just to move from a product to a restricted product. But as I confidently explained to Maddy recently, this is easy; a restricted product is a filtered colimit of products, and left adjoints preserve colimits, so this is a proof that tensoring with a finitely-presented $R$-module commutes with taking restricted product of $R$-modules with respect to $R$-submodules.

So on the plane I found a counterexample :-) If the index set is infinite and the filter is cofinite, if $K_i$ is $\Z/4\Z$ and $A_i$ is the subgroup $2\Z/4\Z$, if $R=\Z$ and $M=\Z/2\Z$ then the restricted product $X$ has a subgroup $\prod_iA_i$ and the quotient is $\oplus_i(\Z/2\Z)$, and tensoring over $\Z$ with the finitely-presented module $M:=\Z/2\Z$ gives us $X/2X$ which still admits a map from $\prod_i A_i$; this map isn't injective any more (tensor product isn't left exact), but it's not the zero map either because if $g$ is a generator of $2\Z/4\Z$ then $(g,g,g,g,\ldots)$ is not a multiple of 2 in the restricted product so lives on in $X/2$ giving us nonzero elements which become zero in $\prod_i[K_i/2;0]=\oplus_i\Z/2\Z$.

[Kevin Buzzard]

So in fact I knew that something might be up when I attempted to formalise the statement of what I'd suggested that Maddy prove; the discussion is here #Is there code for X? > tensoring up a submodule @ 💬 . If $K_i$ are modules with submodules $A_i$ and if we write $\prod'[K_i;A_i]$ for the restricted product, then I want to write $M\otimes\prod'[K_i;A_i]=\prod'[M\otimes K_i;M\otimes A_i]$ but even though $A_i\subseteq K_i$ the map from $M\otimes A_i$ to $M\otimes K_i$ might not be injective any more, so in order to state what we mean by the restricted product we have to interpret $M\otimes A_i$ as meaning "the image of this in $M\otimes K_i$". Initially I wasn't at all bothered by this because when I figured that when you take the filtered colimit everything would sort itself out, but actually the filtered colimit isn't quick enough; it can only deal with finitely many injectivity failures, so in a situation where injectivity fails infinitely often this can cause problems (as in the example).

So actually the statement should be that if $M$ is a finitely-presented flat $R$-module (and in the application $R=A$ and $M=B$ which is indeed flat as it's finitely-generated and projective).

Under this extra hypothesis my sketch proof can be turned into a proof.

[Kevin Buzzard]

Although I might not have too much time to think about this this week (or next week, when I'm running a workshop in Oxford), I must say that I am currently not really clear about how one is going to formalise this. Recall the set-up again; we have a commutative ring $R$ and a finitely-presented flat $R$-module $M$. We have $R$-modules $K_i$ each equipped with with $R$-submodules $A_i$. The claim is that there's a canonical isomorphism $M\otimes_R\prod'[K_i;A_i]=\prod'[M\otimes_R K_i;M\otimes_R A_i]$.

And the proof is: $M\otimes_R\prod'[K_i;A_i]=M\otimes\mathrm{colim}_S\left(\prod_{i\notin S}A_i\times\prod_{i\in S}K_i\right)=\mathrm{colim}_S\left(M\otimes(\prod_{i\notin S}A_i\times\prod_{i\in S}K_i)\right)=\mathrm{colim}_S\left(\prod_{i\notin S}(M\otimes A_i)\times\prod_{i\in S}(M\otimes K_i)\right)=\prod'[M\otimes K_i;M\otimes A_i].$

But we don't seem to have a predicate "I am a direct limit" in mathlib. Do people have suggestions of good ways to formalise this?

[Madison Crim]

I was looking at Mathlib.Algebra.Colimit.Module file and a way to take direct limits there. In lean I was able to construct the direct limit Module.DirectLimit. My original set-up was when M was finitely presented, but I can fix this to include the condition that M is also flat.

[Kevin Buzzard]

The thing about that file is that it uses DirectLimit, i.e. "given a directed system I will produce a new type for you called the direct limit of that directed system". I feel like in this situation we would rather say "given a directed system and a bunch of maps from that system to some type that we have already (i.e. the restricted product), the type that we have already is a direct limit". Direct limits are unique up to unique isomorphism but in Lean "unique isomorphism" isn't the same thing as "equals". It's a bit like the difference between docs#Localization and docs#IsLocalization , docs#AlgebraicClosure and docs#IsAlgClosure and so on. I wonder if having IsDirectLimit would make our lives easier here?

[Kevin Buzzard]

@Anatole Dedecker do you have any thoughts on how to formalize that chain of R-module isomorphisms above in Lean? The tl;dr is: tensoring by a finitely-presented flat module preserves arbitrary products, and restricted products are filtered colimits of products, and tensoring commutes with filtered colimits because it's a left adjoint, so tensoring with a f.p. flat module commutes with restricted products.

[Dagur Asgeirsson]

Kevin Buzzard said:

I feel like in this situation we would rather say "given a directed system and a bunch of maps from that system to some type that we have already (i.e. the restricted product), the type that we have already is a direct limit"

Do you want to avoid category theory? If not, you're just saying that a cocone is a colimit (docs#CategoryTheory.Limits.Cocone, docs#CategoryTheory.Limits.IsColimit). I know IsColimit isn't a prop but that's not really important here

[Shaopeng]

(deleted)

[Joël Riou]

Dagur Asgeirsson said:

Kevin Buzzard said:

I feel like in this situation we would rather say "given a directed system and a bunch of maps from that system to some type that we have already (i.e. the restricted product), the type that we have already is a direct limit"

Do you want to avoid category theory? If not, you're just saying that a cocone is a colimit (docs#CategoryTheory.Limits.Cocone, docs#CategoryTheory.Limits.IsColimit). I know IsColimit isn't a prop but that's not really important here

I made a Prop version of IsColimit for types docs#CategoryTheory.Functor.CoconeTypes.IsColimit

[Bryan Wang]

Perhaps a useful first step is to formalise the fact that an arbitrary restricted product is a (filtered) colimit? Or maybe this has been done somewhere..

[Kevin Buzzard]

Yeah, the question is how to state that in lean

[Bryan Wang]

It does seem natural to define IsDirectLimit using universal property of direct limit, analogous to IsColimit. But then I guess one of the first questions is to show that RestrictedProduct satisfies this? I could maybe also see some value in providing the explicit bijection between the RestrictedProduct and DirectLimit

[Bryan Wang]

In any case it seems that some basic results relating Filter (which is used to define RestrictedProduct) and DirectedSystem might be needed (both live in Mathlib.Order)

[Joël Riou]

In #27504, I add lemmas which allow to check that a type-theoretic cocone for a functor F : J ⥤ Type w₀ is colimit when J is a filtered category.

[Bryan Wang]

Bryan Wang said:

In any case it seems that some basic results relating Filter (which is used to define RestrictedProduct) and DirectedSystem might be needed (both live in Mathlib.Order)

A rough mwe:

import Mathlib.Topology.Algebra.RestrictedProduct.Basic
import Mathlib.Order.DirectedInverseSystem

open Set Filter

variable {ι : Type*} {𝓕 : Filter ι}

variable (𝓕) in
/-- The complements of sets in a `Filter`.
E.g. for the cofinite filter, these are just the finite subsets. -/
def Filter.complement : Set (Set ι) := (fun S => Sᶜ) '' 𝓕.sets

theorem principal_filter_order {S₁ S₂ : 𝓕.complement} (h : S₁ ≤ S₂) :
    (𝓟 S₂ᶜ : Filter ι) ≤ 𝓟 S₁ᶜ := by
  simp only [le_principal_iff, mem_principal, compl_subset_compl]; exact h

theorem filter_bot :
    ∀ S : 𝓕.complement, 𝓕 ≤ (𝓟 Sᶜ : Filter ι) := by
  intro S
  simp only [le_principal_iff]
  refine Filter.mem_sets.mp ?_
  have h : 𝓕.sets = (fun S => Sᶜ) '' (𝓕.complement) := by
    rw[complement]
    exact Eq.symm (compl_compl_image 𝓕.sets)
  rw[h]
  simp

open scoped RestrictedProduct

variable {R : ι → Type*} {A : (i : ι) → Set (R i)}

variable (A) in
/-- This is (isomorphic to) `(Π i ∈ S, R i) × (Π i ∉ S, A i)` -/
def mem_A_away_from_S (S : 𝓕.complement) : Type _ :=
  Πʳ i, [R i, A i]_[𝓟 Sᶜ]

/-- The inclusions between `mem_A_away_from_S` which will form the directed system. -/
def inclusion (S₁ S₂ : 𝓕.complement) (h : S₁ ≤ S₂) :
    mem_A_away_from_S A S₁ → mem_A_away_from_S A S₂ :=
  RestrictedProduct.inclusion _ _ (principal_filter_order h)

instance directed_system :
    @DirectedSystem (𝓕.complement) _ (mem_A_away_from_S A) (inclusion) where
  map_self _ _ := rfl
  map_map _ _ _ _ _ _ := rfl

/-- The maps from the directed system to the actual restricted product. -/
def inclusion_to_restrictedProduct (S : 𝓕.complement) :
    mem_A_away_from_S A S → Πʳ i, [R i, A i]_[𝓕] :=
  RestrictedProduct.inclusion _ _ (filter_bot S)

-- ....

[Joël Riou]

The idea would be to build a docs#CategoryTheory.Functor.CoconeTypes structure and prove it is colimit using the results in the PR above.

[Bryan Wang]

Joël Riou said:

The idea would be to build a docs#CategoryTheory.Functor.CoconeTypes structure and prove it is colimit using the results in the PR above.

ok, let me see if I can try that out. My concern was how to interface RestrictedProduct with these other structures (Colimit, DirectLimit, ...)

[Kevin Buzzard]

What is the conceptual way to understand what we are doing in this project? I realise I have some fundamental questions.

For adeles, what we seem to be doing is constructing a functor A from the category of number fields (with morphisms just abstract ring homomorphisms) to the category of commutative topological rings, sending a number field to a locally compact and second countable topological ring. This functor has the property that it sends a ring morphism between number fields K->L to a continuous morphism between topological rings A(K) -> A(L) making A(L) into a finite free A(K)-module and such that A(L)'s topology is the A(K)-module topology. But there is also some extra structure -- the adeles of K are a K-algebra. Is there a category-theoretic way of stating this? It's some kind of "dependent functor"? And then how to state in categorical terms that there's a canonical isomorphism $L\otimes_K\mathbb{A}_K=\mathbb{A}_L$ for every ring morphism $K\to L$ between number fields?

For finite adeles we have done a similar thing but in a more general set-up. The source category of the finite adele functor seems to be the category of pairs (A,K) with A a Dedekind domain and K a choice of field of fractions, with morphisms defined to be AKLB diagrams (so L/K a finite separable extension of fields, implying I believe that B is a finite projective A-algebra). The finite adele functor goes from these pairs (A,K) to abelian profinite topological groups, plus again the extra structure that the finite adeles of (A,K) is a K-algebra and an A-algebra and there's a scalar tower. The functor has the property that an AKLB morphism makes the B-finite-adeles into a finite free module over the A-finite-adeles, and the topology on the B-finite-adeles is the A-finite-adele-module topology. I feel like the construction should also be functorial for localisations (i.e. not AKLB but A' is a localisation of A with the same field of fractions) but I didn't think too hard about this.

I am unclear about what generality the statements should be for infinite adeles, is this a number-field-only thing?

I think it's worth mentioning that for the global adele functor, a completely different approach to that in the literature is simply to define the a new basic type: the adelic completion $\mathbb{A}_0$ of the integers, which is the product topological ring $\widehat{\mathbb{Z}}\times\mathbb{R}$ (the product of the arithmetic and real-analytic completions of some basic arithmetic types), and then we can define the adeles of a number field $K$ to just be $K\otimes\mathbb{A}_0$, the tensor being over $\Z$, and we give it the $\mathbb{A}_0$-module topology. Another advantage of making this basic type $\mathbb{A}_0$ is that we then get a predicate for "I am the adeles of K", namely IsTensorProduct Z K A_0. Any abelian group is automatically a Z-module. Is it the case that any locally profinite or locally compact second-countable topological abelian group (or maybe just every complete topological additive abelian group?) is uniquely a topological module for A_0? This would make "IsAdeleRing K" be a predicate on complete topological rings equipped with a K-algebra structure.

[Kevin Buzzard]

(deleted)

[Johan Commelin]

Is it the case that any locally profinite or locally compact second-countable topological abelian group (or maybe just every complete topological additive abelian group?) is uniquely a topological module for A_0?

Isn't $\Z$ a counterexample? That satisfies your assumptions, right?

[Kevin Buzzard]

What's the theorem then? What kind of topological abelian objects inherit an action of A_0, like abelian groups inherit an action of $\Z$?

[Johan Commelin]

Do we already have a subsingleton statement? If a top.ab.grp has a topological module structure over A_0, then it has exactly one such structure?

[Johan Commelin]

That sounds true to me.

[Johan Commelin]

And then maybe you just have to look at the classification of LCA's, and kick out the discrete bits.

[Kevin Buzzard]

Hmm, I see that GL1(Qp) has the same problem as Z, near to 1 you get an action but it doesn't act on a uniformizer. Maybe compactness is needed?

[Johan Commelin]

Although... I guess $\mathbb{F}_p$ is a perfectly fine top.ab.grp with module structure over A_0?

[Johan Commelin]

$\R$ is fine. So you don't need compactness.

[Kevin Buzzard]

Yeah but $\R/\Z$ isn't.

I was trying to figure out whether the adeles were defined by some kind of natural universal property

[Alex Kontorovich]

Do we have the abstract/axiomatic notion of a Global Field?... (See: https://sites.math.rutgers.edu/~alexk/2023S572/Artin1943.pdf)

[Kevin Buzzard]

We do not. My opinions on formalising global fields is that we should just do the number field and function fields separately, and that we should also do finite and infinite adeles separately in the number field case, because even though it's definitely useful to know that Archimedean and nonarchimedean norms are analogous, in practice their API is totally different; it's ROrCLike in the arch case and rings of integers in the nonarch case.

[Kevin Buzzard]

Every profinite abelian group has an action of Zhat, because it's the pontrjagin dual of a discrete torsion group.

[Matthew Jasper]

FLT#697 is everything left except the direct limit result.

[Kevin Buzzard]

I'm away until Tuesday but FLT reviewing will be number 1 priority when I get back (I need to concentrate hard on FLT for the next month after my holiday ends)

[Madison Crim]

I'm currently working on the direct limit result. I have a

variable {R : Type*} [Semiring R] {ι : Type*} [Preorder ι] (M : ι → Type*) (P : Type*)
variable [AddCommMonoid P] [Module R P]
variable [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)] (f : ∀ i j, i ≤ j → M i →ₗ[R] M j)
variable (g : ∀ i, M i →ₗ[R] P)
variable [DecidableEq ι] [IsDirected ι (· ≤ ·)] [Nonempty ι] [DirectedSystem M (f · · ·)]

@[mk_iff] class IsDirectLimit' : Prop where
  surj : ∀ m : P, ∃ i, ∃ mi : M i, g i mi = m
  inj :  ∀ i j, ∀ mi : M i, ∀ mj : M j, g i mi = g j mj → ∃ (k : ι) (hik : i ≤ k) (hjk : j ≤ k),
      f i k hik mi = f j k hjk mj
  compatibility : ∀ i j hij x, g j (f i j hij x) = g i x

From this is I was able to show Module.DirectLimit satisfies this, construct a lift map, show uniquness, and show

noncomputable def iso_of_isDirectLimit'
    [h₁ : IsDirectLimit' M P₁ f g₁] [h₂ : IsDirectLimit' M P₂ f g₂] :
    P₁ ≃ₗ[R] P₂  := sorry

I'm now trying to prove that (P ⊗[R] N) satisfies IsDirectLimit. I'm having some difficulties showing injectivity. I was talking to Bryan Wang who thinks we should maybe instead consider using #docsModuleCat.

[Andrew Yang]

Are you stuck mathematically or lean-wise?

[Madison Crim]

A bit of both. I'm wondering if I'd have an easier time proving that having the universal property implies IsDirectLimit, and then proving (P ⊗[R] N) satisfies IsDirectLimit that way.

[Andrew Yang]

I am guessing what you want is to transport IsDirectLimit' across isos, and transport it along $P \otimes \varinjlim N_i \cong \varinjlim (P \otimes N_i)$.

[Andrew Yang]

But I thought the hard part is tensoring with finite presented modules commutes with inverse limit. Do we have this already?

[Madison Crim]

This is the end goal. I didn't think we need a finitely presented flat module until we want to show the direct limit commutes with the restricted product. I am not stuck anymore and am making progress again.

[Bryan Wang]

Andrew Yang said:

But I thought the hard part is tensoring with finite presented modules commutes with inverse limit. Do we have this already?

There is docs#TensorProduct.directLimitLeft

[Bryan Wang]

But when it comes to bringing in RestrictedProduct, there were (I think) two main routes, either give the explicit isos between RestrictedProduct and a DirectLimit, or more generally define IsDirectLimit (and get the iso from there, say)

[Bryan Wang]

However for IsDirectLimit, there are some issues around the universal property which I guess would be better handled using some category-theoretic API

[Madison Crim]

Can you clarify what you mean by issues around the universal property? I
was able to prove we have the universal property for IsDirectLimit.
Although I haven’t proved having the universal property implies
IsDirectLimit.

[Bryan Wang]

Oh I thought you mentioned there were type issues when formulating the universal property?

[Madison Crim]

Oh yes, I was having type issues for both versions of IsDirectLimit. Now with the previous version, including compatibility now, I had success constructing a lift map, showing uniqueness, and the isomorphism we wanted.

[Madison Crim]

I couldn’t figure out how to get around the type issues for having one of the properties of IsDirectLimit be the universal property. I instead deduced it from the previous version of IsDirectLimit.

[Bryan Wang]

I guess perhaps eventually one would want to prove things about IsDirectLimit without showing it is iso to a DirectLimit (or sth similar). Otherwise we could have also just given the explicit iso to DirectLimit, similar to say docs#Submodule.FG.rTensor.directLimit ? (I might be missing sth here)

[Bryan Wang]

This feels like it is of more categorical nature, so then the question becomes how to interface the more algebraic API (like Module, etc) with the category-theoretic API? and it seems like docs#ModuleCat does some of that

[Andrew Yang]

Bryan Wang said:

Andrew Yang said:

But I thought the hard part is tensoring with finite presented modules commutes with inverse limit. Do we have this already?

There is docs#TensorProduct.directLimitLeft

I am confused. This seems to be exactly what Maddy is proving? And I said this is the easy part and inverse limit is the hard part. We need both because the restricted product is a direct limit of inverse limits.

[Madison Crim]

This is what I was working on yes, just with the IsDirectLimit class. I missed this in the docs.

[Bryan Wang]

Andrew Yang said:

Bryan Wang said:

Andrew Yang said:

But I thought the hard part is tensoring with finite presented modules commutes with inverse limit. Do we have this already?

There is docs#TensorProduct.directLimitLeft

I am confused. This seems to be exactly what Maddy is proving? And I said this is the easy part and inverse limit is the hard part. We need both because the restricted product is a direct limit of inverse limits.

I could be wrong, but I think all we need is that the restricted product is a direct limit of products