Local fields in Lean 4

Stream: maths

[Florent Schaffhauser]

Is it ok to also post the link to the arXiv version of the article?

[Filippo A. E. Nuccio]

Here the HAL (but I think that this should be free)

[Florent Schaffhauser]

Filippo A. E. Nuccio said:

but I think that this should be free

Only the abstract and reference list (for me right now, not on a university network).

[Filippo A. E. Nuccio]

Long Live Free Repositories :smile: :free:

[Patrick Massot]

This is great! We all know it’s no fun at all to return to some job that seemed finish and fight the system to port it.

[Notification Bot]

5 messages were moved here from #announce > Local fields in Lean 4 by Johan Commelin.

[Johan Commelin]

@María Inés de Frutos Fernández @Filippo A. E. Nuccio Awesome! Great job! Looking forward to the PRs.

[Filippo A. E. Nuccio]

Johan Commelin said:

María Inés de Frutos Fernández Filippo A. E. Nuccio Awesome! Great job! Looking forward to the PRs.

Sure? We'll ping you for each of them... :wink:

[Andrew Yang]

We are preparing a PR containing this (with all the sorries filled) into mathlib at the class field theory workshop at Oxford (with the help of Yakov and Kenny and others). I believe this stemmed from a secret negotiation between people who care about this the most so I assume people are already somewhat happy about it, but I shall post it here first to gather feedback.

import Mathlib

class IsNonarchLocalField (K : Type u)
    [Field K] [ValuativeRel K] [UniformSpace K] : Prop extends
  IsUniformAddGroup K,
  ValuativeTopology K,
  LocallyCompactSpace K,
  ValuativeRel.IsNontrivial K

open ValuativeRel

namespace IsNonarchLocalField

variable (K : Type u) [Field K] [ValuativeRel K] [UniformSpace K]
  [IsNonarchLocalField K]

example : IsTopologicalDivisionRing K := inferInstance

instance : CompactSpace 𝒪[K] := sorry

instance : IsDiscreteValuationRing 𝒪[K] := by sorry

instance : ValuativeRel.IsDiscrete K := sorry

instance : ValuativeRel.IsRankLeOne K := sorry

instance : CompleteSpace 𝒪[K] := sorry

instance : Finite 𝓀[K] := sorry

instance : CompleteSpace K := sorry

end IsNonarchLocalField

[Kenny Lau]

Should we ping the relevant people?

[David Ang]

(in particular we believe we can fill all the sorries here just with those 4 assumptions)

[Andrew Yang]

David Ang said:

(in particular we believe we can fill all the sorries here just with those 4 assumptions)

No they are actually sorry free.

[David Ang]

Ah, you managed to fill rank le one!

[Yakov Pechersky]

Thank you for compiling all of this! Will there be a helper constructor for the instance that rather than take a LocallyCompactSpace argument, takes simpler ones like the various ValuativeRel instances + CompleteSpace? Because it seems challenging proving that, e. g. F((T)), is locally compact without first proving all of the conclusions listed.

[Yakov Pechersky]

Or, more relevant to (L)CFT, K_v for K a number field and v a place.

[Kenny Lau]

@Yakov Pechersky sorry, could you be more specific on what the helper constructor should look like?

[Yakov Pechersky]

lemma IsNonarchLocalField.mk' (K : Type u) [Field K] [ValuativeRel K] [UniformSpace K] [IsUniformAddGroup K] [ValuativeTopology K] [ValuativeRel.IsNontrivial K] [ValuativeRel.IsDiscrete K] [ValuativeRel.IsRankLeOne K] [CompleteSpace K] : IsNonarchLocalField  K := sorry

-- this one installs the topology and UniformSpace etc structure from `Valuation.subgroups_range_basis`, from #27314
-- https://github.com/leanprover-community/mathlib4/pull/27314/files#diff-e5cabd8cf65825ec8f06f06e9f50c80c48c36996bad6b09e6691642fc1506542R96
lemma IsNonarchLocalField.mk_with_uniformSpace (K : Type u) [Field K] [ValuativeRel K] [ValuativeRel.IsNontrivial K] [ValuativeRel.IsDiscrete K] [ValuativeRel.IsRankLeOne K] := sorry

[María Inés de Frutos Fernández]

Have you also proven Valuation.IsRankOneDiscrete for the ValuativeRel.valuation (or more generally, for a compatible valuation)?

[Andrew Yang]

Not yet tried. But I assume one should prove that for all ValuativeRel.IsDiscrete K + ValuativeRel.IsRankLeOne K (and perhaps + nontrivial).

[Andrew Yang]

BTW it would be helpful if someone can first review/merge #27430 :wink:

[Kenny Lau]

to recap, the above definition says:

import Mathlib

class IsNonarchLocalField (K : Type u)
    [Field K] [ValuativeRel K] [UniformSpace K] : Prop extends
  IsUniformAddGroup K,
  ValuativeTopology K,
  LocallyCompactSpace K,
  ValuativeRel.IsNontrivial K

[Kenny Lau]

i have a question to ask the communtiy, because now we've removed a lot of axioms, and we've discovered that "uniform space" wasn't really used in the axioms

[Andrew Yang]

I think we are doing

import Mathlib

class IsNonarchLocalField (K : Type u)
    [Field K] [ValuativeRel K] [TopologicalSpace K] : Prop extends
  IsTopologicalAddGroup K,
  ValuativeTopology K,
  LocallyCompactSpace K,
  ValuativeRel.IsNontrivial K

instead

[Kenny Lau]

yes, that's the alternative definition we want to propose, and then the plan is that whenever we need the uniform structure, we'll add that to the assumptions.

[Andrew Yang]

#27465 (and in particular this file) contains the aforementioned definition and the instances.
(This depends on #27412 which depends on #27430)

[Adam Topaz]

I think being a topological group should follow from being a valuative topology, in case you want to minimize further!

[Adam Topaz]

congrats on this work btw!

[Andrew Yang]

Adam Topaz said:

I think being a topological group should follow from being a valuative topology, in case you want to minimize further!

Valuative topology only describes the neighborhoods of 0 I think.

[Adam Topaz]

oh youre right. maybe we should change it to describe the nbhds of any element?

[Adam Topaz]

somehow in my mind being a topological group should follow from having the topology induced by the valuation, and, yes, for that we would need to say something about the nbhds of any point

[Patrick Massot]

Equivalently you can add that translation are homeomorphisms.

[Patrick Massot]

stated in terms of pushing nhd to nhd.

[Andrew Yang]

translation are homeomorphisms.

I think that is exactly ContinuousAdd (on groups)?

[Patrick Massot]

No, ContinuousAdd asks that addition is continuous of both variables.

[Patrick Massot]

If you simply take a random filter as neighborhoods of zero and carry it around by translation then you don’t always get a topological group, but translations will be “homeomorphisms” by construction.

[Patrick Massot]

docs#AddGroupFilterBasis tells you what to ask about (a basis of) your filter to get a topology that is a group topology.

[Aaron Liu]

docs#ContinuousConstVAdd gives you translations are homeomorphisms (is there a better way to state it?)

[Kenny Lau]

so, for the sake of consensus, let me once again recap the definition in Andrew's PR #27465:

class IsNonarchLocalField (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K] : Prop extends
  IsTopologicalAddGroup K,
  ValuativeTopology K,
  LocallyCompactSpace K,
  ValuativeRel.IsNontrivial K

Does anyone have any (significant) objection to this definition?

[Aaron Liu]

You're bundling IsTopologicalAddGroup but when your space is also a UniformSpace you have to additionally state IsUniformAddGroup and then the IsTopologicalAddGroup forks is kind of useless

[Andrew Yang]

I claim we seldom care / need that it is a uniform space in statements

[Kenny Lau]

when we do analysis we want completeness right

[Kenny Lau]

like exp

[Kenny Lau]

but yeah i don't think this is a good enough reason (at least for me) to add IsUniformAddGroup to the assumptions

[David Ang]

There was some notation whose history I’m a bit confused about:

• We have \MCO K for rings of integers of number fields and function fields and \McO[K] for valuation rings of valued fields. Why square brackets for one and space for the other? Is the different font necessary because \MCO K_p cannot be distinguished from (\MCO K)_p? We should add module docstrings for these notations in any case.
• We have \McO[K] in two different files Topology.Algebra.Valued.ValuedField and Topology.Algebra.Valued.ValuativeRel, so we can’t open both scopes but they’re both often used in the same file to get some instances. I think we should remove this duplication.

[Kenny Lau]

Links:

• 𝓞 K for number field
• 𝒪[K] for valuative rel

[Yakov Pechersky]

Removing the duplication of notation relies on getting rid of Valued. That is slowly in progress. The duplication of notation was added to help assist in the refactor.

[María Inés de Frutos Fernández]

Is the plan still to replace Valued by ValuativeRel? That was my impression, but I have been given conflicting answers about this.
@Kevin Buzzard @Adam Topaz

[Kevin Buzzard]

I just want a definition of nonarch local field that everyone is happy with. We certainly need an API for ValuativeRel mimicking the Valued API but I don't see why we should delete Valued because perhaps sometimes you really do only care about one specific NNReal-valued valuation on a field and you can make a local instance or whatever if it's on a concrete object like Q or the splitting field of X^2+1 over Q_3 etc

[María Inés de Frutos Fernández]

This contradicts the documentation on the Mathlib.Topology.Algebra.Valued.ValuationTopology file:

The Valued class defined in this file will eventually get replaced with ValuativeRel from Mathlib.RingTheory.Valuation.ValuativeRel. New developments on valued rings/fields should take this into considation.

[Andrew Yang]

I think we should get rid of Valued and just carry around a valuation that is Compatible in the case Kevin mentioned. I don’t think this is any more cumbersome. We might need a typeclass saying that a Norm instance is compatible with a valuation (or a RankOne) on it.

[Adam Topaz]

I think that keeping Valued around is perfectly reasonable to do for now. Eventually we should probably phase it out and do things as Andrew suggests, but I understand that there was quite a lot of work done on top of Valued (some of which is not in mathlib), so I don't think we necessarily need to rush to delete Valued from the library.

[Adam Topaz]

Kenny Lau said:

so, for the sake of consensus, let me once again recap the definition in Andrew's PR #27465:

class IsNonarchLocalField (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K] : Prop extends
  IsTopologicalAddGroup K,
  ValuativeTopology K,
  LocallyCompactSpace K,
  ValuativeRel.IsNontrivial K

Does anyone have any (significant) objection to this definition?

In terms of this, I think this is a perfectly reasonable definition. We should keep in mind that ValuativeTopology is only "correct" if we also assume IsTopologicalAddGroup (or something slightly weaker). The only change I would suggest is to redefine ValuativeTopology to say something about the nbhds of any point, as we discussed in the thread above.

With such a change to ValuativeTopology, by assuming [ValuativeTopology K] [UniformSpace K] it would be possible to provide instances of [IsTopologicalDivisionRing K]

[Yakov Pechersky]

My proposal is to deprecate the construction of explicit Valued instances, and instead rely on the one we currently have implied by ValuativeTopology. That way, we can keep the Valued API without having competing instances.

[Kevin Buzzard]

Oh ok I guess i can easily imagine a world with Valued gone one day, I think Adam's suggestion is perfectly viable and it could be a long-term project to just deprecate it?

[Kevin Buzzard]

You can't use Valued.v but you can just use v instead

[Kenny Lau]

following the discussion above, I will redefine ValuativeTopology today (cc @Yakov Pechersky ). Is there anything I should look out for?

[Kevin Buzzard]

#26845 . Can you base your PR on top of that? Otherwise whichever PR of yours and mine lands first will cause problems for the other one.

[Kenny Lau]

Why is this PR a month old?

[Kevin Buzzard]

Because I made a 3-line PR expecting it to go straight in, there was a pause while we waited for a reviewer, it was then pointed out that I hadn't deprecated the old version on the day I left for a family holiday, I was then on holiday for a week and then in Oxford for a week, and then I noticed it wasn't in and by this time the lemmas were accruing so it took me some time to re-do the PR.

[Kenny Lau]

I have created #27939 and now I will implement the suggestions I received...

[Kenny Lau]

aha, I linked to #26845, and then realised that it got merged just now :upside_down:

[Kenny Lau]

It is now pre-merged :tada:

[Andrew Yang]

I was suggested by @Filippo A. E. Nuccio to ask on the zulip (and especially @Patrick Massot) about the design choice around UniformSpace.

The current choice is

class IsNonarchimedeanLocalField
  (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K] : Prop extends
  IsValuativeTopology K, LocallyCompactSpace K, ValuativeRel.IsNontrivial K

And the suggested alternative is

class IsNonarchimedeanLocalField
  (K : Type*) [Field K] [ValuativeRel K] [UniformSpace K] : Prop extends
  IsUniformAddGroup K, IsValuativeTopology K,
  LocallyCompactSpace K, ValuativeRel.IsNontrivial K

The reason why I prefer the former is:

1. It enables us to talk about topological spaces being local fields without first putting on a uniform space structure. Although there is a unique sensible one, there might be multiple non-defeq ones.
2. It is easier to prove IsUniformAddGroup K once you have IsNonarchimedeanLocalField K, instead of trying to prove them in one go.
3. One loses no functionality as one could write [IsNonarchimedeanLocalField K] [UniformSpace K] [IsUniformAddGroup K] to recover the latter behaviour.
4. One seldom needs a UniformSpace structure in statements so the invocation in the previous point is rare.

And I personally don't see the benefit of the latter.

[Filippo A. E. Nuccio]

Just for the context (and why I asked this in the first place), I would prefer bundling the uniform structure for three reasons:

1. It aligns better with the suggestion in the docstring where the uniform structure on a group is provided;
2. It allows to manually add several calls of the form letI := isUniformAddGroup_of_addCommGroup (G := K) in proofs (like here)
3. From the forgetful inheritance perspective, it would be a bad practice to define a new instance (the uniformity) on such a field if it does not come from erasure of data.

[Kenny Lau]

I agree because of 1.

[Andrew Yang]

The reason why I view these as non-benifits are

1. I think this question should be evaluated on its own merit, and the docstring should merely be a description of the best approach and could be easily changed if necessary. Of course there must be a reason why the docstring is written this way so I totally agree that asking on Zulip would be helpful.
   In particular I think the usual convention should be to only require UniformSpace when the statement requires it (e.g. we prefer assuming Finite and doing cases nonempty_fintype in proofs unless the statement requires Fintype; especially for data carrying typeclasses).

2. I don't think golfing has high priority when choosing definitions. And a big portion of them are actually symptoms of parts of mathlib superfluously requiring UniformSpace (e.g. docs#Valued)

3. I don't understand this point fully. To me, forgetful inheritance seems to be implemented in both approaches allow arbitrary UniformSpace and TopologicalSpace structure.

[Kenny Lau]

I guess after this I should clarify, I agree based on the reasoning provided in 1's docstring but I have not evaluated the claim of the docstring; that is to say, I would wait for Patrick to show up.

[Filippo A. E. Nuccio]

Certainly waiting for Patrick is a good idea! My two cents are that the claim in the docstring is not very far from my point 3, but at any rate I try to clarify what I meant.

With the current design, you get a UniformStructure on a Local Field by adding some structure (the uniformity), although this is somewhat canonical; if you embed the UniformStructure in it, the arrow NonArchLF -> UniformSpace becomes just an erasure. Am I missing something that you have in mind, @Andrew Yang ?

[Sébastien Gouëzel]

If I read correctly, the current design works fine with [TopologicalSpace K] around, while the new one will require [UniformSpace K] (which is a stronger assumption apparently, although they are in fact equivalent in this context). If that's indeed the case, I would prefer the current design because it requires less assumptions (and topological spaces are less scary than uniform spaces for many people). Do you need the uniform structure for the statement of many definitions / theorems (for instance in terms of completeness)?

[Filippo A. E. Nuccio]

Yes, we need it all the time, because completeness is the key for many properties of nonarchimedean local fields.

[Andrew Yang]

I don't think we need them in the statements, which is what Sébastien was asking.

[Sébastien Gouëzel]

But a locally compact topological field is automatically complete for its uniform structure, right? So the current set of assumptions already implies completeness. My question is really about the statements of theorems, not the proofs.

[Filippo A. E. Nuccio]

OK, I see your (and Andrew's) point.

[Filippo A. E. Nuccio]

And what about my point 3? One problem we encountered with @María Inés de Frutos Fernández is the following set-up: suppose that $L/K$ is a finite extension of nonarchimedean fields, and $F$ is an intermediate extension. You want type class inference to deduce that $F$ is also a nonarchimedean field. If you only need to give it a topology, it will be the one induced from $L$, and now it will have two possible (equal, of course) uniformities, one from $L$ and one since it is a loc. compact field. But if to prove it is a nonarchimedean field you need to fix the uniformity, no diamond can occur.

[Adam Topaz]

I think I agree with Andrew here. If we use

class IsNonarchimedeanLocalField
  (K : Type*) [Field K] [ValuativeRel K] [TopologicalSpace K] : Prop extends
  IsValuativeTopology K, LocallyCompactSpace K, ValuativeRel.IsNontrivial K

and assume [UniformSpace K], we can still talk about [IsNonarchimedeanLocalField K] since the topological space structure is inferred, we can provide an instance of IsUniformAddGroup K which is a Prop.

[Filippo A. E. Nuccio]

I think our messages overlapped, it is still unclear to me how the intermediate field would not end up with two uniformities.

[Andrew Yang]

I view this example as a support for the first approach though. In the second approach, If you prove that it is a local field with the first uniformity, then you are hard stuck if you somehow end up with the second uniformity. But with the first approach, you prove that the underlying topology gives you a local field, and then lemmas will work fine with both uniformities.

[Aaron Liu]

wait which two uniformities can we have here

[Aaron Liu]

we should always only have one uniformity

[Andrew Yang]

You could have the left uniformity, the right uniformity, or the induced uniformity, which should all be equal but not necessarily defeq.

[Filippo A. E. Nuccio]

One is docs#instUniformSpaceSubtype and the other is docs#IsTopologicalGroup.toUniformSpace

[Aaron Liu]

Why would you have docs#IsTopologicalGroup.toUniformSpace

[Aaron Liu]

it's not an instance

[Aaron Liu]

you will not have it

[Filippo A. E. Nuccio]

I agree that it would not be there automatically, but it can be there.

[Filippo A. E. Nuccio]

And I think this was the whole point of the docstring of docs#IsTopologicalGroup.toUniformSpace

[Aaron Liu]

well I think the only way it will be there is if you put it there and at that point it's kind of your own fault

[Filippo A. E. Nuccio]

The problem is that if I need one at a certain point, I'll need to pick up one (both are equal mathematically) and there's no preferred choice.

[Aaron Liu]

the solution is to add it to your assumptions at the top

[Aaron Liu]

unless it doesn't appear in the statement in which case you shouldn't get a conflict (since it's not in the statement)

[Kevin Buzzard]

Note that we have the tactic borelize which puts the standard Borel measure space structure on a topological space; maybe we need some analogous tactic putting the standard uniform space structure on a topological group for convenience in a proof. I am not as convinced as Aaron is that we won't randomly pick up random non-defeq uniform space instances, but as Sebastien points out if these things are not showing up in theorem statements (and I think they're not) then I'm also voting for the current design. I am acutely aware of the disruption that this is causing to Filippo and Maria Ines' work and this is not a decision I am taking lightly; I am also aware that this discussion has been going on for over a year now, and am happy to admit that I had absolutely no idea how complex the question "how to define nonarchimedean local fields in mathlib" would turn out to be. This was not a question I was taking too seriously for a long time, but it clearly needs to be taken very seriously, and has been taken seriously by the community over the last few months. I only hope that now we are near the end of the discussion, but I fear that there is still plenty of work to do ensuring that our ultimate decision is the right one.

More generally discussions like this do I think reveal that our decisions about how to set up topology and algebra in mathlib (via typeclasses) have left us with very complex problems, which so far we have mostly solved, but we certainly have not solved completely; issue #7152 is an example of something which is still unresolved and is causing problems in FLT (perhaps because I am pig-headedly refusing to bow to the design decision of changing whether I write $A\otimes B$ or $B\otimes A$ depending on whether I want this thing to be an $R$-module or an $S$-module, if $R$ acts on $A$ and $S$ acts on $B$). Our design choice to use data-carrying typeclasses have many benefits but also cause problems, as the discussion above clearly shows. But hopefully with local fields we are finally ready to make a decision and then to start dealing with the consequences.

[Filippo A. E. Nuccio]

After all, I must say that I'm quite convinced by Sébastien's, and Andrew's, arguments. Of course we will only be 100% sure once this is implemented, but I now think that some of the care we put in avoiding non-defeq uniformities was not needed, since indeed they very rarely show up in statements. I'm happy merging the current design — I cannot maintainer-merge since this has alredy been done once, but IMHO we can move forward, time will tell better than too many discussions if this is the right approach.

[Riccardo Brasca]

OK, let's merge this and see what happens. Thanks to all for your work!

[Kenny Lau]

yay!