v.adicCompletionIntegers vs Valued.integer

Stream: FLT

[Yakov Pechersky]

It seems like there are many ways to refer to the valuation ring. I've been proving things about it using Valued.integer (which is really a no extra things over Valuation.integer). There's also Valuation.Integers which is a Prop between a domain O and field F and the expected algebra between them.

[Yakov Pechersky]

Perhaps it will be easier to reuse results if there's a consistent way to refer to said subring?

[Yakov Pechersky]

The completion for sure has a Valued (over Zm0).

[Yakov Pechersky]

Do you ever refer to the v extended to F explicitly? Because you could then say v'.Integers also, for some arbitrary ring, which then sidesteps exactly how you define it.

[Yakov Pechersky]

The reason I bring this up is that it might be easier to work with something that seems to be an arbitrary ring (and thus the infinite products of them) than having to refer to some explicit subtypes, even more so if they come from (possibly overlapping) instances.

[Yakov Pechersky]

Or, this is a refactor with little profit. I'm just not exactly sure how much reuse there currently is between these specific completion valuation rings made directly from a prime ideal (IDD.hOS) and thus Valued foo Zm0 vs arbitrary generalized results.

[Kevin Buzzard]

If this is about https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/QuaternionAlgebra/NumberField.lean then I am totally open to other suggestions about how to define these groups. I just copied what was used in the definition of docs#DedekindDomain.FiniteAdeleRing . Do you think we should be doing something else in (a) the aforementioned file (b) the definition of finite adele ring?

[Yakov Pechersky]

This was in context of the other thread that mentioned adicCompletionIntegers wrt Hecke algebras. Currently on a plane, so having some issues loading a Mathlib cache to see how much work it would be to change FiniteAdeleRing. Because that's what it seems like your QuaternionAlgebra file is using. Although the localFullLevel defn uses the Integers also. Once I get better internet, I can try turning adicCompletionIntegers into an abbrev, or something similar.

[Yakov Pechersky]

So my answer is, it makes sense that you did (a) because of how (b) is. And I'd like to experiment with making (b) better. It probably doesn't make sense to change (a) before changing (b) because of how much (a) relies on (b)

[Kevin Buzzard]

Note also #20021 . @Anatole Dedecker what is the status of that work?

[Patrick Massot]

I think Anatole is in vacations this week and maybe won’t see this message immediately.

[Anatole Dedecker]

The status is that I made a second version which looks satisfying to me, and then I got distracted by other things. I will try to make it a proper PR before Monday, because I'm quite busy next week

[Kevin Buzzard]

Just as it is (presumably) impossible to have $GL_2(R\times S)=GL_2(R)\times GL_2(S)$, it will be impossible to have GL_2 of a restricted product being restricted product of the GL_2's, so there are going to be a bunch of ugly isomorphisms which I'm going to have to carry around :-/ So I suspect that before we go too much further with this it would be good to get these restricted products in because we might want to redefine finite adeles afterwards, and part of FLT is full of GL_2(finite adeles).

[Anatole Dedecker]

#20021 is ready I believe. Tell me if you want me to split the PR and/or the files.

[Ruben Van de Velde]

Please run 'lake exe mk_all' to regenerate the import all files