Finite extensions of Q_p

Stream: mathlib4

[Kevin Buzzard]

Right now mathlib has docs#NumberField for finite field extensions of $\mathbb{Q}$ (a poorly-named Prop), and docs#RCLike for finite field extensions of $\mathbb{R}$ (although for reasons I've never understood, the analysts also want to fix a square root of $-1$ in the degree 2 case, so it's not a Prop, meaning that it can't really be used for archimedean completions of number fields). For FLT I am becoming convinced that I need some way of talking about finite field extensions of $\mathbb{Q}_p$, with the examples I care about being nonarchimedean completions of number fields, and $\mathbb{Q}_p$ itself. #mwe s for these:

import Mathlib

open IsDedekindDomain

-- note [NumberField K]
variable (R : Type*) [CommRing R] [IsDedekindDomain R]
    (K : Type*) [Field K] [NumberField K] [Algebra R K] [IsFractionRing R K]
    (v : HeightOneSpectrum R)

-- this
#check v.adicCompletion K


variable (p : ℕ) [Fact p.Prime]

-- and this
#check ℚ_[p]

I've just knocked up the following proposal: what do people think?

import Mathlib.Algebra.Order.Group.TypeTags
import Mathlib.Analysis.Normed.Field.Lemmas
import Mathlib.Topology.Algebra.Valued.ValuationTopology

open scoped Multiplicative

/-- A field with a discrete valuation is said to be a 𝓹-adic field if
it's characteristic zero, complete, locally compact, and |p|<1. -/
class IsPadicField (K : Type*) [Field K] [Valued K ℤₘ₀] (p : ℕ) [Fact p.Prime] where
  isCompleteSpace : CompleteSpace K
  isCharZero : CharZero K
  isPadic : Valued.v (p : K) < 1
  isLocallyCompact : LocallyCompactSpace K

The $\mathbb{Q}_p$-algebra structure is data which I am reluctant to include (although I guess there will be a def which could be promoted to an instance when appropriate).

[Yakov Pechersky]

Shouldn't we show that for a given degree, the fields satisfying this are isomorphic? As in, there is only one unique extension for each degree

[Yakov Pechersky]

LocallyCompact already implies discreteness of valuation iiuc

[Adam Topaz]

A local field is a non-discrete locally compact field (which I think can be made into a prop). The p-adic case is a Property on top of that, although we may want to add data to the class for convenience as Kevin suggests.

[Adam Topaz]

And it’s not the case that the degree determines the field up to isomorphism

[Yakov Pechersky]

Ah sorry, I think I interpolated unramified into the statement

[Kevin Buzzard]

Aha, so I could remove Valued and just ask for the uniform space instance (and maybe that p^n tends to zero)

[Kevin Buzzard]

It's not true at all that there's a unique extension of each degree, the absolute Galois group of the p-adic numbers is a very complicated thing. In fact what started me off on this is that the thing I really need for FLT if I don't want to sorry data is the Artin map from $F^\times$ to the abelianisation of the absolute Galois group of $F$ and I was contemplating how to do this which led me to the thoughts above

[Adam Topaz]

There are now at least three projects that are interested in LCFT. Should we try to coordinate? Deciding on the definition of IsLocalField would be a good start :)

[Kevin Buzzard]

I only started thinking about this today so deciding to collaborate now would be optimal!

[Adam Topaz]

My proposal for IsLocalField is to say that the type of topologies which make the field into a locally compact nondiscrete topological field is nonempty (so really a prop!). NonArch could be done by saying e.g. that the image of Nat is contained in a compact subset.

[Adam Topaz]

Although from that point of view maybe IsLocalField should take a topology and a topologicaldivisionring instance as mixins?

[Adam Topaz]

docs#IsLocallyCompact

[Adam Topaz]

docs#LocallyCompactSpace

[Yakov Pechersky]

Regarding nonarchimedean topologies, I've been reading references like https://arxiv.org/abs/2111.09722 that discuss the generalization of nonarchimedean norms to uniform spaces -- that the uniformity has a basis of equivalence relations. So that would apply to UniformSpace.Completion without having to establish a norm (there is no UniformRing, unlike Uniform(Add)Group)

[Antoine Chambert-Loir]

@Adam Topaz , do you want this type to be nonempty, or unique?

[Adam Topaz]

I think uniqueness is a theorem? E.g. we know that for p-adic fields the valuation ring is uniformly definable in the ring language, so if a field is p-adic then it's p-adic in a way that's determined by the isomorphism type of the field.

[Adam Topaz]

https://www.sciencedirect.com/science/article/pii/S0168007213000791

[Kevin Buzzard]

These sorts of things are true but it's not clear to me that we want to assume them when making the definition. For example when do you ever get a p-adic field which doesn't come with a topology (and also with a prime p)?

[Adam Topaz]

Yeah, I agree. I think IsLocalField should take NontriviallyNormedField as a parameter.

[Adam Topaz]

Note that NontriviallyNormedField includes a uniform space structure.

[Kevin Buzzard]

But it also includes a real-valued norm, so if $K/\mathbb{Q}_p$ is finite then the two standard norms on $K$ (one satisfying $|p|=1/p$ (i.e. compatible with inclusions) and the other satisfying $|\varpi|=1/q$ (i.e. compatible with additive Haar measure)) will give two "different" p-adic fields?

[Adam Topaz]

Right, with this approach it wouldn't be a p-adic field, but rather a p-adic field together with a choice of normalization.

[Adam Topaz]

But I get the point -- if we want to go between two normalizations this would get annoying.

[Yakov Pechersky]

For nonarchimedean fields, it would still difficult if one said Valued K G0 on its own, because a p-adic field can have a variety of G0s : Zm0, NNReal, Real, and in each, it might not be "normalized". To this end, Maria Ines and Filippo recently added docs#Valuation.IsDiscrete, a class which works only on Zm0 valuations, and requires that is surjective (when over a field). Still, that would then limit you to always discuss _the_ normalization, in other words.

[Yakov Pechersky]

Is there an equivalent of MetrizableSpace for normed spaces?

[Yakov Pechersky]

Does WithAbs help in moving between normalizations?

[Kevin Buzzard]

I guess that a p-adic field has a canonical equivalence class of norms and two norms are equivalent iff they induce the same topology, so I'm led to the same question! The topology must be normable!

[Kevin Buzzard]

Maybe that's the same as metrizable?

[Kevin Buzzard]

So the question is: if $K$ is a topological field and it's known that the topology is metrizable, i.e. is induced by a metric $d:K^2\to\R$ on $K$, then is the topology also "normable", in the sense that it is induced from a norm $|.|:K\to\R$ satisfying the docs#NormedField axioms? Note that a norm on a space gives a topology because it gives a metric defined by $d(x,y)=|x-y|$.

[Yakov Pechersky]

An attempt?

import Mathlib


class NormalizableField (K : Type*) [TopologicalSpace K] extends Field K, TopologicalSpace.MetrizableSpace K where
  norm_mul' x y : (TopologicalSpace.metrizableSpaceMetric K).toDist.dist (x * y) 0 =
    (TopologicalSpace.metrizableSpaceMetric K).toDist.dist x 0 *
    (TopologicalSpace.metrizableSpaceMetric K).toDist.dist y 0
  non_trivial : ∃ (x : K), 1 < (TopologicalSpace.metrizableSpaceMetric K).toDist.dist x 0
  dist_sub_eq x y : (TopologicalSpace.metrizableSpaceMetric K).toDist.dist (x - y) 0 =
    (TopologicalSpace.metrizableSpaceMetric K).toDist.dist x y

noncomputable
def NormalizableField.NontriviallyNormedField {K : Type*} [TopologicalSpace K] [h : NormalizableField K] :
    NontriviallyNormedField K where
  norm x := dist x 0
  __ := TopologicalSpace.metrizableSpaceMetric K
  dist_eq x y := by
    change dist x y = dist (x - y) 0
    exact (h.dist_sub_eq _ _).symm
    -- have : IsometricVAdd Kᵃᵒᵖ K := by
    --   refine ⟨fun c ↦ Isometry.of_dist_eq fun x y ↦ ?_⟩
    --   sorry
    -- rw [eq_comm, ← dist_add_right _ _ y]
    -- simp
  norm_mul' := h.norm_mul'
  non_trivial := h.non_trivial

[Yakov Pechersky]

I got into a circular argument issue in the IsometricVAdd Kᵃᵒᵖ K proof, so I yanked out the dist_sub_eq as a separate axiom

[Kevin Buzzard]

Right now I'd be interested to see a maths strategy rather than launching into Lean. Is it even true?

[Yakov Pechersky]

Not all metrizable spaces are normalizable. Frechet spaces can have a translation invariant metric, but not a scaling one. cf: https://math.stackexchange.com/a/3335507

[Kevin Buzzard]

This doesn't surprise me at all, which is why I specifically asked about topological fields.

[Johan Commelin]

Adam Topaz said:

I think uniqueness is a theorem? E.g. we know that for p-adic fields the valuation ring is uniformly definable in the ring language, so if a field is p-adic then it's p-adic in a way that's determined by the isomorphism type of the field.

Kevin Buzzard said:

These sorts of things are true but it's not clear to me that we want to assume them when making the definition. For example when do you ever get a p-adic field which doesn't come with a topology (and also with a prime p)?

One benefit of the approach that Adam suggests is that it avoids the questions about have a distinguished norm etc... as part of the definition. Parts of the API could then assume a norm compatible with the p-adic field structure. But it won't be forced by the definition.

[Kevin Buzzard]

If $K$ is a finite extension of $\mathbb{Q}_p$ for some prime $p$ then the topology is intrinsic to $K$. You can characterise $\mathcal{O}_K^\times$ as the elements of $K^\times$ which have $n$ th roots for infinitely many positive integers $n$ and then you can get arbitrarily small neighbourhoods of 1 by raising this set to the power $N!$ and now you have a basis of neighbourhoods of any point, by translation. You can figure out which $p$ you're talking about by looking at the indices of these $U^{N!}$ subgroups within each other as $N$ increases. From this I suspect that you can reconstruct the norm without too much trouble. But all this seems like a bit of a crazy detour.

[Johan Commelin]

I'm not saying the norm should be defined that way. Just that it shouldn't be part of the definition. If the definition can be a Prop, then I think that is a win.

[Johan Commelin]

(Just like we should have a Prop-version of RCLike.)

[Sébastien Gouëzel]

We have docs#IsRCLikeNormedField

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

Sorry, @Filippo A. E. Nuccio and I just saw this discussion. We have indeed several definitions of local fields that we are working with. First, in our paper A Formalization of Complete Discrete Valuation Rings and Local Fields we defined mixed and equal characteristic local fields as follows:

variable (p : ℕ) [Fact (Nat.Prime p)]

def Q_p : Type _ := adicCompletion ℚ (pHeightOneIdeal p)

/-- A mixed characteristic local field is a field which has characteristic zero and is finite
dimensional over `Q_p p`, for some prime `p`. -/
class MixedCharLocalField (p : outParam ℕ) [Fact (Nat.Prime p)] (K : Type _) [Field K] extends
    Algebra (Q_p p) K where
  [to_finiteDimensional : FiniteDimensional (Q_p p) K]

def FpXCompletion :=
  (idealX 𝔽_[p]).adicCompletion (RatFunc 𝔽_[p])

/-- An equal characteristic local field is a field which is finite
dimensional over `𝔽_p((X))`, for some prime `p`. -/
class EqCharLocalField (p : outParam ℕ) [Fact (Nat.Prime p)] (K : Type _) [Field K] extends
    Algebra (FpXCompletion p) K where
  [to_finiteDimensional : FiniteDimensional (FpXCompletion p) K]

We also provide a ValuedLocalField class and prove that mixed and equal characteristic local fields are ValuedLocalFields. In this class, we are endowing the field with its normalized Z_m0-valued valuation.

class ValuedLocalField (K : Type*) [Field K] extends Valued K ℤₘ₀ where
  complete : CompleteSpace K
  isDiscrete : IsDiscrete (@Valued.v K _ ℤₘ₀ _ _)
  finiteResidueField : Finite (IsLocalRing.ResidueField (@Valued.v K _ ℤₘ₀ _ _).valuationSubring)

We have recently been experimenting with how best to define a local field without fixing a valuation, as well as adding (non)archimedean versions. Our current definitions are as follows:

class LocalField (K : Type*) [Field K] extends UniformSpace K, UniformAddGroup K,
  TopologicalDivisionRing K, CompleteSpace K, LocallyCompactSpace K

class NonarchLocalField (K : Type*) [Field K] extends LocalField K where
  isNonarchimedean : IsNonarchimedean (haarFunction K)

class ArchLocalField (K : Type*) [Field K] extends LocalField K where
  Archimedean : 1 < (haarFunction K 2)

The haarFunction is the multiplier function defined in Serre's "Local Fields" Chapter 2, Proposition 2.

[Antoine Chambert-Loir]

I'm not sure I will be very helpful, but Bourbaki, General Topology, Chapter 9, Exercise §4.12 gives a topological characterization topological fields whose topology is defined by an absolute value.
It applies in particular for locally compact fields. So one could imagine setting topological assumptions, and picking up whatever absolute value fits your needs.

image.png

[Kevin Buzzard]

I like Serre's taste and in Cassels-Froehlich he defines a local field to be a field equipped with a discrete valuation such that it's complete and the residue field is finite, so I like ValuedLocalField. I'm wondering whether we should just get this definition into mathlib, and then all the other stuff like proving that certain locally compact fields have this property or proving that the valuation can be recovered from the topology or whatever can come later; my feeling is that ValuedLocalField is a good "middle ground".

Maria Ines is your haarFunction the same as FLT's distrbHaarChar? https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/HaarMeasure/DistribHaarChar/Basic.lean We should also try and get something like this into mathlib because we don't want to duplicate work. I wrote a chunk of blueprint about these characters: https://imperialcollegelondon.github.io/FLT/blueprint/Haar_char_project.html

[Kevin Buzzard]

@Adam Topaz I am happy with Maria Ines' definition of ValuedLocalField as a proposed definition for mathlib, so we can get the ball rolling. Are you?

In the Class Field Theory workshop in Oxford Richard Hill and I are going to try and define the Artin map via the group cohomology approach (and not touch Lubin-Tate formal groups).

[Antoine Chambert-Loir]

I don't absolutely agree with the definition taken for local fields in prime characteristic, because it requires to choose an X to view it as a finite extension of k((X)).
Also, does the valuation have to be normalized? If yes, what happens for extensions?

[Johan Commelin]

I would rather have a definition that uses minimal data, and use that in all statements that don't need the data. And then also have definitions or tactics that easily allow you to scale up the amount of data inside a proof, when needed.

A similar thing is done with Polish spaces in mathlib, and it seems to work well. Whenever you need a metric, it's a 1-line step at the start of the proof.

Having minimal data will avoid all sorts of nasty diamond issues, for example about extensions.

[Filippo A. E. Nuccio]

Dear All, thanks for your comments on our work. Some more detailed answers:

• @Antoine Chambert-Loir : we thought about starting off with nilpotent elements, and live without a predetermined uniformity, but this ended up creating more diamonds than other, because a commutative topological group comes with a uniformity, and this is unique. So, following the suggestion here we decided to put the uniformity structure in the definition of LocalField. This should also address the first of @Johan Commelin 's question: our definition only contains the data of the uniformity (and of a field...) but all the other extended fields are Prop-valued.
• @Antoine Chambert-Loir again: concerning your objection about K((X)), we agree that fixing the place at infinity in this way is really not optimal. But the right way of doing it would be to develop a sensible notion of K-curves and to work with the field of rational functions on them, I believe. Since most of the results one might have in mind should be provable irrespectively that the field be of equal/mixed characteristic, we provide the class mainly so that if someone encounters a finite extension of K((X)), the API for local fields becomes accessible, but I agree this will need to change on the long run.
• @Johan Commelin beyond your point of avoiding data as much as possible, we agree but the comparison with Polish spaces is not 100% accurate: for a local field, there exists a preferred valuation, coming from the maximal ideal (and normalized so as to send generators of this to 1). That being said, we can think at removing some data even from ValuedLocalField, but this definition turns out in our experience to work quite well both for finite/infinite extensions and we think that the way we set up things is quite diamond-safe.
• @Kevin Buzzard Our definition of ValuedLocalField is almost ready to go: in the sense that the definition itself can enter mathlib, but for the API we built around it we need some basic theory of (complete) DVR's, for which there are open PR's that are not yet merged. Concerning the Haar multiplier, I'll have a look later but I think it is indeed the same.

All in all, our strategy was to set up an abstract notion (LocalField) that is pretty general, and almost data-free, but not terribly useful; and an accompanying one ValuedLocalField, that contains more data but is very useful and plays well with the API for DVR's; and of course to show they're equivalent. The classes MixedChar.LocalField, and EqualChar.LocalField are there mainly to show that the ValuedLocalField definition makes sense and it is a workable one; andNonarchimedeanLocalField and ArchimedeanLocalField are there with a view towards Ostrowski.

Concerning the PR process, as said, the definition is ready, but to provide a nice API we are opening the PR's to first set up a good theory for complete DVR's (and extensions theoreof).

[Johan Commelin]

Sounds like a good plan to me.

[Yaël Dillies]

Kevin Buzzard said:

Maria Ines is your haarFunction the same as FLT's distrbHaarChar? https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/HaarMeasure/DistribHaarChar/Basic.lean We should also try and get something like this into mathlib because we don't want to duplicate work.

Sorry I dropped the ball there. Let me PR more stuff now

[Sébastien Gouëzel]

Note that we also have docs#MeasureTheory.Measure.modularCharacterFun with the same flavor (which is not in the right namespace because it does not depend on the choice of a measure, by the way)

[Filippo A. E. Nuccio]

@Sébastien Gouëzel This was the first thing I tried, but it turns out this is not really what we need, because it only treats translation by an element in the group. In our case, it is the units of a (comm) ring acting (multiplicatively) on the additive group of the ring, so what I was doing was to adapt the argument to a HasMeasurableSMul setting.

[Sébastien Gouëzel]

Yes, it's definitely not the same thing! But it has the same flavor, so I wonder if there is a common generalisation, or at least if the API or constructions should be parallel.

[Yaël Dillies]

Yes, this is what I did for FLT too

[Filippo A. E. Nuccio]

My hope was to deduce the modularCharacterFun from a general MeasureableSMul setting, in the special case when a group acts on itself. Perhaps I should coordinate with @Yaël Dillies if they've already thought about this (aka: if they've already finished doing all the work :smirk: )

[Yaël Dillies]

I believe distribHaarChar from FLT is already more general than modularCharacterFun

[Yaël Dillies]

(up to possible mismatches in convention)

[Filippo A. E. Nuccio]

I'll have a look later today and will come back to you (but will be happy to hear from @Kevin Buzzard if he agrees with @Johan Commelin that we can move on as planned insofar ValuedLocalField is concerned).

[Sébastien Gouëzel]

In modularCharacterFun, there is only a multiplicative group, no additive group, so I don't see how it follows from distribHaarChar.

[Yaël Dillies]

Ah yes sorry I misremembered. The crucial difference is the use of DistribMulAction instead of MulAction

[Yakov Pechersky]

Would #16733 still be applicable here? It's sat around for a couple of months now.

[Kevin Buzzard]

Yes definitely! At some point someone is going to have to PR a definition and my main desire is that this happens quickly, despite the fact that different people seem to have different ideas about what that definition should be. Once the decision is made, we will then have to prove that it's the same as all the other definitions, and your PR will definitely be helpful at this point!

[Filippo A. E. Nuccio]

Yes, I agree. I think that @Yakov Pechersky 's PR will be extremely useful to prove the equivalence LocalField iff ValuedLocalField. On the other hand, we take a slightly different approach, so what I'd suggest is that once everything is ready to PR the definition ofValuedLocalFields, we merge both PR's and use his to prove the equivalence. This should not take long, and I am happy to take a look at your PR in the meanwhile.

[Yakov Pechersky]

Great, thanks for the info! Is there anything I can do to help prepare/align on approaches? For example, I'm working on generalizing nonarchimedean metric spaces to nonarchimedean uniformities, which would allow us to have a common prop typeclass IsUltraUniformity that applies to rank-not-necessarily-one valued fields, and such that no particular normalization is required.

[Filippo A. E. Nuccio]

Yakov Pechersky said:

Great, thanks for the info! Is there anything I can do to help prepare/align on approaches? For example, I'm working on generalizing nonarchimedean metric spaces to nonarchimedean uniformities, which would allow us to have a common prop typeclass IsUltraUniformity that applies to rank-not-necessarily-one valued fields, and such that no particular normalization is required.

Sure, let's discuss this in a DM with also @María Inés de Frutos Fernández .

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Yes definitely! At some point someone is going to have to PR a definition and my main desire is that this happens quickly, despite the fact that different people seem to have different ideas about what that definition should be. Once the decision is made, we will then have to prove that it's the same as all the other definitions, and your PR will definitely be helpful at this point!

@Kevin Buzzard I do not have the impression that there are many different points of view: my take of the above discussion is that there was some consensus in what @María Inés de Frutos Fernández and myself are doing, no? Did I misunderstand it? Unfortunately most of our work needs PR's that have been waiting for weeks to be reviewed.

[Yaël Dillies]

I do not look at the queueboard, but if you believe some of your PRs are within my competence then request my review and they shall be reviewed

[Filippo A. E. Nuccio]

OK, thanks!

[Yaël Dillies]

Yaël Dillies said:

Sorry I dropped the ball there. Let me PR more stuff now

First PR: #23595

[Yaël Dillies]

and now #23596

[Kevin Buzzard]

By the way, I mentioned this work to another number theorist last week and they pointed out that Weil developed the basic theory in his "Basic number theory". I've just looked up what he calls this character (because we just made up distribHaarChar and I thought it was better to switch to the name in the literature) but unfortunately Weil calls it the "module" of the automorphism!

Screenshot from 2025-04-02 21-49-25.png

I think we might be better off sticking to our name :-/

[Michał Mrugała]

Iirc the module terminology is also used in Bushnell Henniart

[Antoine Chambert-Loir]

Modulus would be a reasonable alternative

[Kevin Buzzard]

Back to the point, can someone propose a definition of LocalField or IsLocalField which we agree is the one we want in mathlib?

[Adam Topaz]

how about

class LocalField (F : Type*) extends
  NontriviallyNormedField F, LocallyCompactSpace F

(or just use those two existing classes as mixins?).

[Sébastien Gouëzel]

Yeah, no need to have a new class there (especially since the second class is just a Prop mixin)

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

We proposed

class LocalField (K : Type*) [Field K] extends UniformSpace K, UniformAddGroup K,
  TopologicalDivisionRing K, CompleteSpace K, LocallyCompactSpace K

above to avoid having to pick a norm.

[Adam Topaz]

It’s not clear to me that we would want to pick a topology without picking a norm.

[Adam Topaz]

If IsLocalField means Nonempty LocalField, then I think we would want LocalField to have a norm.

[Adam Topaz]

Actually with my proposal IsLocalField can’t just be Nonempy LocalField because NontriviallyNormedField bundles the field structure.

[Kevin Buzzard]

So the two definitions are equivalent; from an instance of Adam's class you can get an instance of Maria Ines', and then by this Bourbaki exercise which Antoine posted you can get an instance of Adam's from an instance of Maria Ines'. Have I got this right? And so the question basically is whether we want to demand a metric or a topology.

[Adam Topaz]

Yes the two are equivalent, and the norm is uniquely determined (up to equivalence) by the field structure alone!

[Adam Topaz]

My perspective is that in practice we won’t ever want the topology without the norm, and if we have the norm, the topology is included as well.

[Kevin Buzzard]

I guess one thing which the topology definition has which the norm doesn't have is that isomorphic local fields really will be isomorphic, but you might have two equivalent-but-not-equal norms on the same field. Do we have equivalence of norms?

[Kevin Buzzard]

I'm not sure this bothers me really though, and indeed for finite extensions of Q_p there are two equally "canonical" but distinct norms, depending on whether you want $|\varpi|=1/q$ (the "module") or $|p|=1/p$ (the one giving compatibility with the usual norm on $\mathbb{Q}_p$). So probably it would be nice to be able to talk about both rather than "the norm constructed by the Bourbaki exercise probably also using some random choice"

[Adam Topaz]

Do we even have a type of isomorphisms of normed fields?

[Antoine Chambert-Loir]

As soon as the norm defines its topology (and/or its uniform structure), you'll be fine with it.

[Antoine Chambert-Loir]

Even on the complex numbers you have various equivalent norms. (You can take the standard norm to the power $\varepsilon$, for $0<\varepsilon\leq 1$.)

[Kevin Buzzard]

The module has $\varepsilon=2$!

[Filippo A. E. Nuccio]

One of the mathematical reasons we did not want to pick a norm is what @Kevin Buzzard mentioned, about two possible reasonable normalisations, both with $\vert p\vert=1/p$ or with $\vert \varpi\vert = 1/p$. One "mathlib"-reason we wanted to avoid the norm is that we might want to speak about general complete non-archimedean fields (like $\mathbb{C}_p$) and to be able to upgrade them to locals field as soon as they are locally compact, eg when their residue field is finite. With @Adam Topaz 's definition this seems more complicated.

[Kevin Buzzard]

Your first point I think boils down to whether you want the two copies of same field with two distinct equivalent norms to be equal or not, and I'm not sure in practice if we're going to care about this because equality of types isn't really a thing. A general nonarchimedean field has a real-valued norm so I don't understand your second point

[Filippo A. E. Nuccio]

A general nonarch field is not locally compact unless the residue field is finite; now, if you want to have a general class Nonarch of which $\mathbb{C}_p$ is an instance, and then to prove the

instance [Nonarch F] [Finite (ResidueField F)] : LocalField F

how can you do this if LocalField is as in Adam's definition?

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Your first point I think boils down to whether you want the two copies of same field with two distinct equivalent norms to be equal or not, and I'm not sure in practice if we're going to care about this because equality of types isn't really a thing. A general nonarchimedean field has a real-valued norm so I don't understand your second point

Yes, I understand your "equality of types is not a thing", but I find it slightly awkward to have two types for the same field, it worries me that it can create troubles if we prove things for one and not for the other. In particular, if you define a valuation using the norm, and then you want to say that the valuation of a uniformiser is -1 (in Multiplicative Z), this is only true for one of the two definitions and not the other.

[Sébastien Gouëzel]

Do you really need a definition of local fields? Why not just develop the theory assuming [NontriviallyNormedField k] [LocallyCompactSpace k] (which should be the right assumptions 99% of the time), and if you want to apply such a theorem to a field which doesn't have a norm, then apply the theorem saying there is a compatible norm on the field?

[Sébastien Gouëzel]

In particular, the example with Nonarch would just be

instance [NontriviallyNormedField k] [CompleteSpace k] [Nonarch K] [Finite (ResidueField K)] : LocallyCompactSpace K

[Filippo A. E. Nuccio]

I can think about it, but what is the downside of the definition we propose with @María Inés de Frutos Fernández ? Just to compare pros and cons.

[Sébastien Gouëzel]

If you don't have a norm, a bunch of analysis is not available (including calculus, or good behavior of the space of continuous linear maps or continuous bilinear maps). And just using Prop mixins on top of [NontriviallyNormedField K] ensures you will never get any kind of diamond.

[Filippo A. E. Nuccio]

I see, but I wonder if there is any analytical result we want to prove about general local fields, irrespectively of them being archimedean or nonarchimedean. But I understand your point.

[Kevin Buzzard]

Re: "why define local fields at all?": The reason I want a definition of local fields is that local fields are a thing. Serre wrote an entire book called "Corps locaux". I'm running a summer school in October where we will develop the class field theory of local fields. More to the point, I am scared that Adam will start developing some API using one definition and Filippo will start developing API using another one, and then it's the representation theory car crash all over again.

If our conventions are fighting against having a definition of local fields (just as they fight against us having a definition of vector spaces and of unique factorisation domains) then I think this is a little sad. I do take your point that this is what the conventions are pushing us to do. But I can see downsides to this.

[Kevin Buzzard]

Filippo, the downside of your definition is that the entire theory is developed assuming that a norm exists.

[Kevin Buzzard]

And I still don't understand your Nonarch question. Firstly there is a (probably irrelevant) mathematical point that it's not true that a nonarch field with finite residue field is locally compact (think about the completion of the cyclotomic extension of Qp). But secondly I don't see the problem at all in using Adam's definition once the theorem is correctly stated. What are you worried about? You just have to prove a theorem in topological ring theory. It's much harder to construct the norm from the topology and also very artificial.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Filippo, the downside of your definition is that the entire theory is developed assuming that a norm exists.

Well, this is why we provide the class ValuedLocalField, which is the one we suggest to work with most of the time in the nonarch case. This LocalField only serves at unifying archimedean and nonarchimedean fields, but I'd say that 90% of Serre's book focuses on the nonarchimedean case, for which ValuedLocalField (with its valuation <-> norm) does the job.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

And I still don't understand your Nonarch question. Firstly there is a (probably irrelevant) mathematical point that it's not true that a nonarch field with finite residue field is locally compact (think about the completion of the cyclotomic extension of Qp). But secondly I don't see the problem at all in using Adam's definition once the theorem is correctly stated. What are you worried about? You just have to prove a theorem in topological ring theory. It's much harder to construct the norm from the topology and also very artificial.

For the math question, it depends on what you call nonarch (I thought it also have discrete in it), but that's not the point, I believe we agree on the math. All in all, I certainly agree we do not want to develop two different concurrent works, so I'd take a moment to reflect upon all this and to discuss with María Inés.

[Kevin Buzzard]

I think I should just note the bottom line here: I don't care what the definition is or even if we have a definition. What I care about is that we do not have a bunch of API written for two or more competing definitions and this is why I think it's important that the community at least decides which definition will have the API built for it. I should say to Filippo that yes I only care about the nonarch case, the people interested in reals and complexes will just use \R and \C anyway, and the small amount of work necessary to extend this stuff to the third Archimedean local field, namely an algebraic closure of R with no preferred square root of -1, won't be too hard.

[Johan Commelin]

Concerning multiple definitions: as long as there is a hierarchy, it shouldn't be a problem. An instance from one to the other is good. But if they are competing, and it cause a bifurcation, then that is bad.

[Kevin Buzzard]

So let me give a concrete example so that we have something concrete to talk about rather than classes like Nonarch which don't actually exist. Right now I need: given $K$ a nonarch local field and $n$ a positive natural, I want the degree $n$ unramified extension of $K$, equipped with the canonical isomorphism of its Galois group with the Galois group of the residue field (i.e. existence), I want uniqueness (given two unramified extensions of the same degree, they're isomorphic) and I want the theory to apply to $\mathbb{Q}_p$, to Filippo/Maria-Ines' definition, to Adam's definition, and to $$k((X))$ for $k$ a finite field. Obviously that will take a while. But what I want to avoid is someone saying they've "done the construction" but the construction not being applicable in every possible case where people might want to use it. So what should the existence part of this claim look like?

[Filippo A. E. Nuccio]

Need to run now, but either @María Inés de Frutos Fernández or myself will answer soon with what we've currently got in mind, on which we've been working the last two weeks, so we have a bit of code to share.

Kevin Buzzard said:

So let me give a concrete example so that we have something concrete to talk about rather than classes like Nonarch which don't actually exist. Right now I need: given $K$ a nonarch local field and $n$ a positive natural, I want the degree $n$ unramified extension of $K$, equipped with the canonical isomorphism of its Galois group with the Galois group of the residue field (i.e. existence), I want uniqueness (given two unramified extensions of the same degree, they're isomorphic) and I want the theory to apply to $\mathbb{Q}_p$, to Filippo/Maria-Ines' definition, to Adam's definition, and to $$k((X))$ for $k$ a finite field. Obviously that will take a while. But what I want to avoid is someone saying they've "done the construction" but the construction not being applicable in every possible case where people might want to use it. So what should the existence part of this claim look like?

[Kevin Buzzard]

Is this what it should look like?

import Mathlib

universe u

variable (K : Type u) [NontriviallyNormedField K]
    [LocallyCompactSpace K]
    [NonarchimedeanRing K]

def ResidueCharacteristic : ℕ := sorry -- get p from K

def UnramifiedExtension {n : ℕ} (hn : 0 < n) : Type u := sorry

variable {n : ℕ} (hn : 0 < n)

instance : Field (UnramifiedExtension hn) := sorry

instance : Algebra K (UnramifiedExtension hn) := sorry

[Filippo A. E. Nuccio]

We actually use the language of Galois insertions, but if you can wait until this afternoon there will be more details (I am really sorry, I am running... :runner: )

[Filippo A. E. Nuccio]

@Kevin Buzzard , I'm finally back. So: most of our results with @María Inés de Frutos Fernández are in this file but we must warn you that is is very much WIP.

What we're doing is to

1. set up a Galois insertion+coinsertion between the intermediate fields in a tower L/K and and integrally closed $\mathcal{O}_K$-subalgebras of $\mathcal{O}_L$, where K is a ValuedLocalField (in our mind, the structure really representing nonarchimedean local fields); and L is a (complete?) topological field with a valuation extending that of K.
2. Set up a Galois coinsertion between extensions of the residue field of $K$ and integrally closed $\mathcal{O}_K$-subalgebras of $\mathcal{O}_L$.
3. Show that the above is also a Galois insertion when $\mathcal{O}_L/\mathcal{O}_K$ is docs#Algebra.Etale.

As you observe, we systematically work in the setting where we've fixed an ambient extensions $L$ of $K$, and this for two reasons:

1. The unramified extensions will at any rate be unique only once we fix a separable/algebraic extension of the base field
2. From a more mathlib-point of view: it would be highly desirable that finite extensions of (valued) local fields are again local fields. This can clearly be a theorem (or def depending on what we end up with as a class, for the time being our ValuedLocalField carries data, so rather a def); but it cannot be an instance for the same reason as finite extensions of number fields don't have an instance of number field. We have docs#NumberField.of_module_finite showing this is the case (as a theorem) but to have a nice instance we need to live in a pre-fixed ambient extension, as in docs#NumberField.of_intermediateField. The reason is the type-class inference cannot pick up K from the mere knowledge of L, so it cannot start looking for a Finite K L instance; whereas if the gadget has type IntermediateField K L, both K and L are known to type-class inference, and everything goes smoothly.

To reconnect all this with the previous discussion, one of the reasons we want to be able to have nice classes describing fields like $\mathbb{C}_p$ that yield instances of ValuedLocalField when adding the assumption FiniteResidueField is that we'd like to apply the above setting to (the completion of) a separable/algebraic closure, so that for every finite extension of the residue field of $K$ the Galois coinsertion yields your unramified extension contained in the fixed separable/algebraic closure. If you really want to get this for a specified degree you can use GaloisField.algEquivGaloisFieldOfFintype or some variation thereof.

[Kevin Buzzard]

Surely the relationship between the intermediate fields and the integrally-closed subalgebras in (1) is an order-preserving bijection, which is much stronger than a Galois insertion. Or am I missing something? Again finite residue field is not enough to give a local field, you need discreteness of the valuation.

If you want to do it this way you will presumably need some way of saying "I am the residue field of you" for abstract fields k and K, so it applies for ZMod p and the p-adic numbers, or for a finite field and the field of fractions of its Witt vectors. How are you doing this?

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Surely the relationship between the intermediate fields and the integrally-closed subalgebras in (1) is an order-preserving bijection, which is much stronger than a Galois insertion. Or am I missing something? Again finite residue field is not enough to give a local field, you need discreteness of the valuation.

If you want to do it this way you will presumably need some way of saying "I am the residue field of you" for abstract fields k and K, so it applies for ZMod p and the p-adic numbers, or for a finite field and the field of fractions of its Witt vectors. How are you doing this?

You're right that this is an order-preserving bijection, which will give us the coinsertion (and of course we'd implement first the order-preserving bijection); the second part is only a Galois (co)-insertion, so for the whole business of going from intermediate extensions of the local field and those of the residue field, that's the only bit that matters. Concerning finite residue fields vs. discreteness, again: we agree on the math, and currently our definition of ValuedLocalField contains IsDiscrete for the valuation (see the above code posted by María Inés).

[Filippo A. E. Nuccio]

For your second question: our way to speak about the residue field of a local field is to take the unit ball (= valuation subring) and the residue field of this (since it has a local ring instance); but I feel this is not really your question, so I haven't probably understood it.

[Aaron Liu]

Kevin Buzzard said:

an order-preserving bijection, which is much stronger than a Galois insertion.

These are incomparable? Unless you actually meant docs#OrderIso, which is stronger than a monotone bijection.

[Kevin Buzzard]

Oh so we are now talking about ValuedLocalField not NonarchLocalField?

These two classes represent the same mathematical objects, right? Are you developing API for both of them? This is exactly what I want to avoid.

[Filippo A. E. Nuccio]

No: we're developing API only for ValuedLocalField; we are defining the structure NonarchLocalField(which we don't even know whether we want to promote to a class) simply to be able to state some nice form of Ostrowsky. But as said the only gadget that we study (vis. that we consider the "right/useful" formalisation of what Serre calls local fields) is ValuedLocalField.

[Kevin Buzzard]

In which case can you PR the definition so that we can establish that this is the definition the community is happy with? Otherwise things are going to get really complicated. I personally don't like the name, for example; nobody in the real world calls these things "valued local fields", they all call them "nonarchimedean local fields".

[Filippo A. E. Nuccio]

Oh, for that matter we're more than happy to change the name :smile:

[Kevin Buzzard]

I will reiterate what I've already said several times before; there are now three groups of people independently working on local fields (although me and Richard Hill are "working on local fields" in the sense that we are just about to start developing API and want to work fast in preparation for July; I don't know how far Adam has got) and I am really concerned that if we keep working independently rather than in mathlib (and unfortunately our repo is private right now so we can release it for the workshop, although it is also completely empty) then there will be a huge mess.

[Filippo A. E. Nuccio]

We have the same fear, and we're trying to PR things; but you know the process is slow. We are currently refactoring the definition of IsDiscrete, which is needed in our definition. We hope it will be done and PR'd soon (say next week?).

[Filippo A. E. Nuccio]

At first, we wanted to PR the def once we also had some API's for extensions of such gadgets, but if you tell us that you prefer the definition to land immediately and to postpone the API for extensions, let be it.

[Filippo A. E. Nuccio]

For example, we thought that the community would not accept the definition of NonarchimedeanLocalField if there is no def of LocalField, so we were trying to have a complete set of things to PR.

[Kevin Buzzard]

Yes we all know that PRing is slow. One positive thing is that FLT is my job right now and I need this stuff for FLT so I am keen to review PRs. I know that Maria Ines requested my review on #23184 but this is blocked on #23178 which is awaiting-author . If we can just get definitions in then we can start writing API and marking it proof_wanted; this is an underused functionality in mathlib and I think that if we want to harmonise our approach then this might be a really good use case for it. The definition will go through the usual discussion and you didn't answer the question about whether you're going to have a predicate for "you are a nonarch local field and I am your residue field" (like we have IsLocalization etc, but this seems to need more thought) which will also need some discussion, but once we have definitions in place it seems to me that we can race through a bunch of proof_wanted API and get it in quickly so we can see where we're going.

[Filippo A. E. Nuccio]

OK, how does it sound if we finish our refactor of what IsDiscrete means, we PR it and once this is done we PR the def of ValuedLocalField (called NonarchimedeanLocalField)?

[Filippo A. E. Nuccio]

Concerning the question about " hey, I'm your residue field!",

[Filippo A. E. Nuccio]

Filippo A. E. Nuccio said:

For your second question: our way to speak about the residue field of a local field is to take the unit ball (= valuation subring) and the residue field of this (since it has a local ring instance); but I feel this is not really your question, so I haven't probably understood it.

[Kevin Buzzard]

Furthermore if you have code then you will be well-informed about how well various definitions work. But above Maria-Ines mentioned a function haarFunction and the FLT version of this is already being PRed in #23603 and that is going to cause you problems. The longer we wait to get down the plan the more times problems like this will occur. And it seems to me that you two have written far more code than anyone else so you should be writing the plan or you will be experiencing most of the pain :-/

[Filippo A. E. Nuccio]

Yes, I agree... we weren't just aware that there were many people around working on this. We are more than happy to coordinate the effort and to speed up. I hope the Nonarchimedean def to be PR somewhen next week, with a link to this Zulip discussion.

[Kevin Buzzard]

By "working on it" in my case I mean "started thinking about it a week ago and have no code" :-) But I think @Edison Xie might also be thinking about this?

[Filippo A. E. Nuccio]

We coordinated with him and he's using the definition from our repo (but I'll let him add whatever he feels to).

[Kevin Buzzard]

Oh nice! That's one less thing to worry about then :-)

[Patrick Massot]

Filippo and Kevin, I think you should have a video call about that. That thread seems pretty inefficient.

[Edison Xie]

Filippo A. E. Nuccio said:

We coordinated with him and he's using the definition from our repo (but I'll let him add whatever he feels to).

I'm not currently copying the definition (i.e I don't need local compact), but I think mine should just adapt to yours :)) Also not working on this tight now because I've got exams to revise and research project report to worry and after that I will adapt whatever definition that's in mathlib (if there isn't then I'm sticking to complete normed field with finite residue) :smile:

[Filippo A. E. Nuccio]

OK, I have advanced in opening some PR's getting to the definition of nonarchimedean local fields. In detail:

• #23725 contains generalities about generators of cyclic linearly ordered commutative groups.
• #23726 defines non-trivial valuations.
• #23727 refactors the definition of discrete valuation to go beyond the special case where $\Gamma=\mathbb{Z}_{m0}$, extending to more general targets.
• #23730 contains the definition of ValuedLocalField. I have well noted that @Kevin Buzzard does not like the name, and prefers NonarchLocalField (say): my point in keeping this name is that I would use NonarchLocalField for a non-trivially normed locally compact field whose norm is non-archimedean; but for many practical purposes we have found with @María Inés de Frutos Fernández that the easiest class to work with is one extending Valued Γ K, together with the assumption that the field is complete, the valuation discrete, the residue field finite, which motivates introducing two structures and making the "valued" one our "preferred" class. Whether the other structure (the normed version) should also be updated to a class can be discussed later, at any rate it is not introduced in any of the above PR's.

We're of course open to discussion and to change the name ValuedLocalField to something else, but in case we want to change it to NonarchLocalField we'd need a suggestion for a name for the other, normed structure.

[Kevin Buzzard]

Looking at

class ValuedLocalField (K : Type*) [Field K] extends Valued K Γ where
  complete : CompleteSpace K
  isDiscrete : IsDiscrete <| Valued.v (R := K)
  finiteResidueField : Finite <| IsLocalRing.ResidueField (Valued.v (R := K)).valuationSubring

in #23730 , all of the fields are Props. I'm wondering whether we're digging ourselves into a hole here. Currently there is a huge effort being made to remove classes like OrderedRing, OrderedCommRing, LinearOrderedRing and LinearOrderedCommRing and replace them all with IsOrderedRing, a predicate which you put on top of the algebra assumption (Ring or CommRing) and the order assumption (PartialOrder or LinearOrder). This has led to a huge speedup in typeclass inference. Here things are different because Gamma is involved, but I'm wondering whether we want the algebra (Field K), the norm (Valued K \Gamma) and then the predicate (IsValuedLocalField, although I think I'd rather call it IsNonarchimedeanLocalField or even just IsLocalField given that the analysts won't care about this sort of thing and the adeles has separated the arch and nonarch cases instead of trying to unify things).

Here's a concrete question for an expert in typeclass inference (@Eric Wieser ?). With the above definition we have the instance

instance : CompleteSpace K := ValuedLocalField.complete

Is this going to send typeclass inference off on some wild goose chase whenever it wants to prove that something is a complete space, looking for some ?Gamma and Valued K ?Gamma and then looking for LinearOrderedCommGroupWithZero ?Gamma?

[Filippo A. E. Nuccio]

The final point about sending type class inference on goose chase is a good one, haven't thought about it. I have also seen the discussion about the new efforts but haven't had time to dig into it yet. Thanks @Kevin Buzzard for the feedback, I'll think about it while waiting for Eric's opinion.

[Eric Wieser]

I think it's safe only if the second argument to docs#Valued is an outParam

[Eric Wieser]

Which it is! So probably it's fine, though I don't fully know the details.

[Eric Wieser]

attribute [instance] ValuedLocalField.complete would be better style than making a copy as an instance

[Yakov Pechersky]

Unfortunately outParam on Valued has a bit of an impedance mismatch because, iiuc, outParam assumes that the param is wholly determined by the other parameters, but we often have Valued K Zm0 and also Valued K NNReal, etc.

[Kevin Buzzard]

So Filippo and Maria Ines are encouraging us away from $\Z_{m0}$ and towards a general totally ordered group with zero, and Yakov is pointing out that for a nontrivial finite extension of $\mathbb{Q}_p$ one might even want to consider two different $\R_{\geq0}$-valued norms ($|p|=1/p$ or $|\varpi|=1/q$) calling into question the entire [Valued K Gamma] set-up. But one thing I learnt from the perfectoid project was that different but equivalent valuations induce the same preorder on $K$. So how about this for a definition. It keeps the algebra and order heirarchy completely separate and joins them with a Prop-valued mixin.

import Mathlib

class IsNonarchPreorder (K : Type*) [Field K] [Preorder K] : Prop where
  le_total (a b : K) : a ≤ b ∨ b ≤ a
  add_le (a b c : K) (h₁ : a ≤ c) (h₂ : b ≤ c) : a + b ≤ c
  mul_le_mul_right (a b c : K) (h : a ≤ b) : a * c ≤ b * c
  zero_lt_one : (0 : K) < 1

Then K inherits a canonical valuation to K/A, the set of cosets of A in K, where A is the element of K such that 1<=a and a<=1, a subgroup of K.

[Filippo A. E. Nuccio]

First of all, just to explain why we're advocating for more general things rather than $\mathbb{Z}_{m0}$: this is related, although not really the same thing, to Yakov's point. When considering arbitrary complete, separable extensions of a local field (irrespective of this very definition), it might be handy to have a general set-up to treat finite and infinite ones on an equal footing, postponing the analysis of the finite case when needed. But for things like $\mathbb{C}_p$ the valuation is $\mathbb{R}_{\geq 0}$-valued, and even for finite extensions the definition of the $\mathbb{Z}_{m0}$-valued one goes through a $\mathbb{R}_{\geq 0}$-valued one, that actually lands in $p^\mathbb{Z}$ and we can "chose a log". So, in this respect, the flexibility of allowing $\Gamma$ to be whatever it should, is much handy.

[Filippo A. E. Nuccio]

Concerning @Kevin Buzzard 's suggestion: I suppose that then the point is to endow K with the Preorder.topology (as a local/scoped instance), right? In principle I agree, but what I am not still sure about is the "canonical" valuation: if you start with a Dedekind domain (local or not local), and pick a prime, you have the IsDedekindDomain.HeightOneSpectrum.valuation, which is $\mathbb{Z}_{m0}$-valued: we could in principle make it $K/A$-valued, but this requires a whole refactor. Is this what you suggest? And how would you treat extensions? If $L/K$ is an extension and the unit ball in $L$ is $B$, saying that a valuation on $L$ extends that on $K$ seems a bit nasty, since the former is $L/B$-valued, the latter is $K/A$-valued. But perhaps I am too scary and things will play out nice, I am just wondering whether you have already thought about this.

[Antoine Chambert-Loir]

What you write suggests me that “Valued fields” (possibly “Valuation Rings”) should be “rings with a lot of stuff — topology and algebra — that is enough to imply that there is a valuation that can define this stuff”, and then we need properties that say that “this valuation is admissible”. In this way, you could use any valuation you like, normalize it, compare it to some other (in extensions, to compositions, etc.).

[Filippo A. E. Nuccio]

Well, the class docs#Valued is indeed what you suggest: a ring with a lot of stuff, including a valuation, a topology and a compatibility between the topology and the valuation. When you say " admissible" do you mean "compatible with the topology"? This is basic the field is_topological_valuation in Valued, and it is indeed the way we use to come up with a Valued instance when we have a valuation as in docs#Valued.mk and docs#Valued.mk'. Or am I misunderstanding what you mean?

[Kevin Buzzard]

Yes I'm suggesting that Valued is a bad idea because it's like OrderedRing. We had eight ordered ring classes, for each pair of ring/semiring, non-commutative/commutative and partial order/total order. Now we have IsOrderedRing which covers all of them. This is both a simplification of the typeclass system and also it resulted in a 20% speedup in typeclass inference.

I'm suggesting that Filippo's proposal is going back down the old route. We have Valued which I think dates back to the perfectoid days when we were using lean 3 with a different typeclass algorithm. Filippo is suggesting that then ValuedLocalField extends this and these are both Type-valued, it feels like exactly the same path and I'm suggesting that we don't go down it at all.

I'm proposing IsValuableField which can be Prop-valued and will eat [Field K] [Preorder K] [UniformSpace K] and will say that the preorder and uniform space both come from a valuation (the preorder is a<=b iff v(a) <= v(b)), and we demand IsUniformAddGroup and is_topological_valuation. The point is that then we can drop Gamma completely. If you want an explicit Gamma and v then you can have another Prop-valued class IsValuation K v extending IsValuableField K which just says that v a <= v b iff a <= b.Then you can drop Valued.v and just have v : K -> Gamma for whatever Gamma you like.

[Antoine Chambert-Loir]

I was meaning everything without a specified valuation.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Yes I'm suggesting that Valued is a bad idea because it's like OrderedRing. We had eight ordered ring classes, for each pair of ring/semiring, non-commutative/commutative and partial order/total order. Now we have IsOrderedRing which covers all of them. This is both a simplification of the typeclass system and also it resulted in a 20% speedup in typeclass inference.

I'm suggesting that Filippo's proposal is going back down the old route. We have Valued which I think dates back to the perfectoid days when we were using lean 3 with a different typeclass algorithm. Filippo is suggesting that then ValuedLocalField extends this and these are both Type-valued, it feels like exactly the same path and I'm suggesting that we don't go down it at all.

I'm proposing IsValuableField which can be Prop-valued and will eat [Field K] [Preorder K] [UniformSpace K] and will say that the preorder and uniform space both come from a valuation (the preorder is a<=b iff v(a) <= v(b)), and we demand IsUniformAddGroup and is_topological_valuation. The point is that then we can drop Gamma completely. If you want an explicit Gamma and v then you can have another Prop-valued class IsValuation K v extending IsValuableField K which just says that v a <= v b iff a <= b.Then you can drop Valued.v and just have v : K -> Gamma for whatever Gamma you like.

Thanks Kevin. I think I see what you mean, it will probably take a while to refactor our project on this direction, but we'll report here or advances and/or doubts.

[Filippo A. E. Nuccio]

Antoine Chambert-Loir said:

I was meaning everything without a specified valuation.

Ah, in that case it is a bit different, you're right. At any rate I think we'll try to implement Kevin's suggestion, and see where it brings us.

[Kevin Buzzard]

@Antoine Chambert-Loir are you talking about local fields? In that case you can have the uniform space and field structure but not the partial order.

[Michael Stoll]

"Valuable field" has a nice double meaning... :wink:

[Kevin Buzzard]

Yeah of course here I mean "it's possible to put a valuation on this field". Probably this stuff should extend to commutative rings.

[Adam Topaz]

Kevin Buzzard said:

import Mathlib

class IsNonarchPreorder (K : Type*) [Field K] [Preorder K] : Prop where
  le_total (a b : K) : a ≤ b ∨ b ≤ a
  add_le (a b c : K) (h₁ : a ≤ c) (h₂ : b ≤ c) : a + b ≤ c
  mul_le_mul_right (a b c : K) (h : a ≤ b) : a * c ≤ b * c
  zero_lt_one : (0 : K) < 1

I think this is a valuable ( :wink: ) definition, but could we remove add_le so that this can also capture Archimedean valuations? Such preorders are called "localities" by some people, and it's actually possible to prove stuff about them! (e.g. https://arxiv.org/abs/1901.02632 ). This does also generalize to commutative rings, and I guess if you look at the set of all a which are indistinguishable from 0 w.r.t. to the preorder, that would be a prime ideal, and the preorder would induce one on the residue field of the prime, etc.

[Adam Topaz]

In other words, I would suggest the following:

import Mathlib

class Locality (K : Type*) [Monoid K] [Preorder K] : Prop where
  le_total (a b : K) : a ≤ b ∨ b ≤ a
  mul_le_mul (a b a' b' : K) (h : a ≤ b) (h' : a' ≤ b') :
    a * a' ≤ b * b'

[Kevin Buzzard]

So you want no add_le field at all?

It is not clear to me that we want to capture archimedean valuations. These always take values in $\mathbb{R}$ and the analysts are already happily using Norm for these. They don't want our silly Localitys and it seems to me that mathlib is making no attempt to unify the archimedean and the nonarchimedean setting, e.g. look at our definition of adeles: it's "do something algebraic at the finite places using HeightOneSpectrum and get a theory which works fine for any Dedekind domain, and then do something totally different at the infinite places using InfinitePlace, and then take the product". I think that any attempt to unify these two approaches would be ludicrous, it would make both developments worse.

I am prejudiced against unification having worked through Jacquet-Langlands. This book attempted to unify nonarchimedean and archimedean points of view when doing the representation theory of local fields and it just makes the book far more obscure than it could be. For example they spend a lot of time talking about Schwarz space, which IIRC they don't even define, but I eventually figured out that what they meant was something like "normal Schwarz space in the real/complex case, and locally constant functions with compact support in the p-adic case" (or possibly some L^2 extension of this). It meant that they could write statements which superficially make sense in both the arch and nonarch case, but then the proofs often split into cases anyway. Eventually after a few chapters even the authors got bored of this approach and just started writing separate chapters for arch and nonarch theorems.

In short: I am not convinced that the analysts will ever care about Localitys. So why bother attempting to accommodate them?

[Filippo A. E. Nuccio]

Just for the record: in the first version of our project with @María Inés de Frutos Fernández , we defined LocalField to be a nonarchimedean local field (through the Valued class discussed above), thinking that at any rate the "uniform" statement of local class field theory for both archimedean and non-archimedean complete locally compact normed fields is a bit artificial: it is true that $\hat{H}^n(G,\mathbb{C}^\times)\cong \hat{H}^{n-2}(G,\mathbb{Z})$, for $G=\{1,\tau\}$ but for much more superficial reasons than for non-archimedean fields (with "quasi-finite" residue field, following Serre's Corps Locaux, Chap. XIII, § 2 --- let me observe in passing that, to the best of my reading, Serre never defines what a local field is in a 250 pages-long, beautiful book entitled "Local Fields"...): in particular, it does not follow from $\operatorname{Br}(\mathbb{C})=\mathbb{Q}/\mathbb{Z}$ (which is false), although Tate--Nakayama's lemma still applies. So, albeit for slightly different reasons (but ultimately analogous), I completely agree with @Kevin Buzzard that keeping the two worlds apart looks the most sensible thing to do.

Later on, we received objections that it was a pity to define local fields only in the nonarchimedean setting, and we tried to accomodate this. I believe that this discussion is mainly a social one (which is perfectly fine, IMHO), and should be treated as such. So, I'd like to propose the following poll, suggesting to postpone the technical discussion about how these gadgets must be implemented to when we'll have agreed about what "these gadget" ought to be:

[Filippo A. E. Nuccio]

/poll Do you agree that Local Field should mean "nonarchimedean"?
Yes, and we can keep the two theories separate.
Yes, but I would insist in having a class containing rings/fields either with a non-archimedean valuation or with a real-valued archimedean norm.
No, we must strive for a uniform approach for all definitions and statements, even if proofs differ in the two cases.

[Antoine Chambert-Loir]

The arguments of Kevin and Filippo convincingly explain that it would probably be an unnecessary burden to develop both theories at the same time, but it would also be misleading that the name departs from classical terminology. So I advocate for something such as “NALocalField” or “NonArchimedeanLocalField”.

[Kevin Buzzard]

Yes my vote is for development of the theory to have nonarchimedean baked in, on the basis that the people developing the theory of $\R$ and $\mathbb{C}$ are already leaps and bounds ahead of us and will not need to use any infrastructure which we build here. I agree with Antoine that we should stick to the literature when it comes to naming conventions.

[Antoine Chambert-Loir]

Or,maybe clearer, two type classes, one “LocalField”, together with “Nonarchimedean” although that is probably too polysemic and no real gain in terms of typing.

[Johan Commelin]

Adam Topaz said:

In other words, I would suggest the following:

import Mathlib

class Locality (K : Type*) [Monoid K] [Preorder K] : Prop where
  le_total (a b : K) : a ≤ b ∨ b ≤ a
  mul_le_mul (a b a' b' : K) (h : a ≤ b) (h' : a' ≤ b') :
    a * a' ≤ b * b'

This fails on $\R$, right? Because the "valuation preorder" conflicts with the usual order on the reals.

[Johan Commelin]

I agree that the two theories will be separate 99% of the time. But I would like to have support for clean unifying statements in that 1% of cases. But if that requires something like [ArakelovLocalField K] (I just made this up) then I'm happy with that.

[Filippo A. E. Nuccio]

OK, so if I understand correctly there is some agreement to define a class NALocalField for locally compact fields endowed with a non-archimedean discrete valuation (we'll decide later if this should extend Preorder or something else); and to postpone the definition of what a LocalField should be, if it will ever be a thing.

This will allow for a speedy process and will allow @María Inés de Frutos Fernández and myself to pull (or adapt+pull) our API reasonably soon. The downside is that for a while @Johan Commelin 's hope will come to a halt. One other option is that we also PR this "umbrella" class as for instance here: I am personally not in favour of this, mainly because if we're not planning to invest time and energy in the general theory for these "archimedean agnostically" local fields, it would simply be a flag put on this def rather than a proper addition to the library.

Is my understanding correct? Shall I proceed like this?

[Kevin Buzzard]

I am not pushing for LocalField, I suspect that there are several different usages of the phrase in the literature. NonArchimedeanLocalField I think we all agree what this means mathematically. Johan can have some LocalField later on if he wants, just by saying "either nonarchimedean local field or RorCLike" or whatever. I cannot imagine it getting much use at present but then again I don't know any Arakelov theory...

[Adam Topaz]

Johan Commelin said:

Adam Topaz said:

In other words, I would suggest the following:

import Mathlib

class Locality (K : Type*) [Monoid K] [Preorder K] : Prop where
  le_total (a b : K) : a ≤ b ∨ b ≤ a
  mul_le_mul (a b a' b' : K) (h : a ≤ b) (h' : a' ≤ b') :
    a * a' ≤ b * b'

This fails on $\R$, right? Because the "valuation preorder" conflicts with the usual order on the reals.

Yes, good point. But then a similar issue would come up with Kevin's original suggestion, e.g. for the nonstandard reals which can be ordered and which have a "canonical" valuation.

[Adam Topaz]

My thoughts on whether to keep things separate is to at least have the core of the theory be common, and, probably very quickly, specialize to the "nonarchimedean" and "archimedean" case on top of this common core. So in practice the development would be separate, but in the 1% of situations where there is something uniform that can be said, we wouldn't have to develop some hacks around the hierarchy to be able to say it.

[Adam Topaz]

@Johan Commelin maybe we need a name change:

class LocalIntegralStructure (M : Type*) [Monoid M] where
  r : M → M → Prop
  r_refl (m : M) : r m m
  r_trans (a b c : M) : r a b → r b c → r a c
  r_mul (a a' b b' : M) : r a b → r a' b' → r (a * a') (b * b')
  r_total (a b : M) : r a b ∨ r b a

[Johan Commelin]

Possibly. Do you think the r will be used? Or should we just record S = {x | r x 1} + axioms about how S behaves under scaling?
Getting flashbacks to the pseudo-normed monoids and balls of radius c from LTE...

[Adam Topaz]

I think with arbitrary commutative rings you probably do need the whole relation.

[Filippo A. E. Nuccio]

But is this needed straight away, or can we wait until we have something to say about this 1%? What scares me a bit is that this introduces data, so it would be wiser that LocalFields (or NALocalFields, are they'll probably be called) extend this class. On the other hand, the library would be at a funny stage, with this class left alone and immediately after another class extending it.

[Filippo A. E. Nuccio]

Johan Commelin said:

Possibly. Do you think the r will be used? Or should we just record S = {x | r x 1} + axioms about how S behaves under scaling?
Getting flashbacks to the pseudo-normed monoids and balls of radius c from LTE...

This gives me also flashbacks about the "fundamental" example in the forgetful inheritance paper; if we have r and we define the unit ball out of it, what happens on M x M? It will come with its own r, giving rise to a "squared" ball and I'm not sure that this is what we want.

[Kevin Buzzard]

Surely in practice we can get away with $S$ not $r$? A more appropriate name for $a \geq b$ is $a\mid b$ meaning $b=za$ for some $z$ with $v(z)\leq 1$.

[Adam Topaz]

If you take $A = \Z$ and the r to come from the trivial valuation on $\mathbb{F}_2$, so that the valuation ring of $\mathbb{F}_2$ is all of $\mathbb{F}_2$, then $S$ would be all of $\mathbb{Z}$. But with r you can distinguish this from the valuation arising from the trivial valuation on $\mathbb{Q}$ since r 3 2 doesn't hold.

[Adam Topaz]

Kevin Buzzard said:

Yeah of course here I mean "it's possible to put a valuation on this field". Probably this stuff should extend to commutative rings.

My point is that if we want to have something work for rings, then we need the relation, not just the "unit ball".

[Antoine Chambert-Loir]

About Locality, what does exactly fail with the real numbers? It seems that the preorder underlying this definition is the one on absolute values. Is it enough to recover the classical ordering on reals?

[Johan Commelin]

@Antoine Chambert-Loir There isn't any math failure. What I meant is that you get to conflicting instances on the reals. So TC will be confused.

[Kevin Buzzard]

OK so all the dependencies of #23730 are now merged, and we're ready to make a decision about the definition. Having talked to various people I am now reluctantly coming around to the fact that we need to extend Valued despite it being a bit of a crappy design, because my proposed alternative (make the definition a Prop built on other things) will be really longwinded. My conclusions from thinking about this is that Lean 4's typeclass system is pushing us towards (R : Type*) [Add R] [Mul R] [Neg R] [Zero R] [One R] [IsCommutativeAdd R] [IsDistrib R]... and we have to choose between slowdowns and this explosion, and until we have machinery which can hide the explosion we're going to have to live with the slowdown, so I'm reluctantly agreeing with extending Valued even though it's data.

Unless I've made some mistake, the PR doesn't compile with current master for some reason; I get

typeclass instance problem is stuck, it is often due to metavariables
  Ring ?m.557

on the isDiscrete field in the definition. Can you merge master @Filippo A. E. Nuccio ?

[Yakov Pechersky]

Is there a reason to prefer IsDiscrete v over IsDiscreteValuationRing v.valuationSubring, especially since you already refer to the subring with IsLocalRing.ResidueField v.valuationSubring?

[Yakov Pechersky]

Similarly, IsCyclic vs MulArchimedean

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

Kevin Buzzard said:

OK so all the dependencies of #23730 are now merged,

Kevin, #23727 is still open (bors closed it by mistake).

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

Yakov Pechersky said:

Is there a reason to prefer IsDiscrete v over IsDiscreteValuationRing v.valuationSubring, especially since you already refer to the subring with IsLocalRing.ResidueField v.valuationSubring?

We prefer IsDiscrete so that v is the normalized valuation.

[Yakov Pechersky]

That's a great line to include in the module docstring and/or the structure field docstring.

[Filippo A. E. Nuccio]

@Kevin Buzzard I see it building, but as @María Inés de Frutos Fernández mentioned the previous #23727 is still not merged, so I'm devoting today/tomorrow to the comments from you and @Yakov Pechersky and once that will be also merged I'll go back to #23730

[Kevin Buzzard]

Note that #23730 has conflicts with master but this is not being picked up by CI right now because #23730 is built off the base branch of #23727 rather than off master. Unfortunately #23727 is currently borked on github (it changes 419 files right nowe). @Filippo A. E. Nuccio I left some suggestions on how to proceed with #23727 on github. We can worry about #23730 github issues later.

Modulo that, I'm reluctantly going to agree to the set-up of extending Valued on the basis that whilst it might cause us problems later on, the alternatives are currently worse, and I'd like to again raise the discussion of what this class should be called. Serre says this in Cassels-Froehlich:

Screenshot from 2025-04-27 10-03-27.png

so for him a local field is equipped with a discrete valuation, which makes me think that this class defined in #23730 should just be called LocalField, or if people are really against this because they still believe in this dream (which I do not believe in) that we are going to prove a nontrivial number of lemmas which are true for the p-adics and the reals but not true for general valuations or norms, then we should call it NonarchimedeanLocalField. I think that calling it ValuedLocalField will just cause confusion because we have made this term up and nobody else uses it.

[Kevin Buzzard]

I think that if we want a class which encapsulates local fields in the sense of complete locally compact fields with a real-valued norm inducing the topology, we can just say that, because all of that is in mathlib.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Note that #23730 has conflicts with master but this is not being picked up by CI right now because #23730 is built off the base branch of #23727 rather than off master. Unfortunately #23727 is currently borked on github (it changes 419 files right nowe). Filippo A. E. Nuccio I left some suggestions on how to proceed with #23727 on github. We can worry about #23730 github issues later.

Modulo that, I'm reluctantly going to agree to the set-up of extending Valued on the basis that whilst it might cause us problems later on, the alternatives are currently worse, and I'd like to again raise the discussion of what this class should be called. Serre says this in Cassels-Froehlich:

Screenshot from 2025-04-27 10-03-27.png

so for him a local field is equipped with a discrete valuation, which makes me think that this class defined in #23730 should just be called LocalField, or if people are really against this because they still believe in this dream (which I do not believe in) that we are going to prove a nontrivial number of lemmas which are true for the p-adics and the reals but not true for general valuations or norms, then we should call it NonarchimedeanLocalField. I think that calling it ValuedLocalField will just cause confusion because we have made this term up and nobody else uses it.

This was indeed our initial design. Since we also develop mixed (resp equal) characteristic local fields as finite extensions of Q_p (resp of F_p((X)) ) we eventually need two more names for those. In order to keep everything somewhat homogenous and to simultaneously go in the directions of some comments above, avoiding attaching once and for all the name Local Field to something, what about deciding that all these gadgets are named XXLocalField, with

• XX = NA for the general one extending Valued
• XX=EC for equal char ones
• XX=MC for mixed char ones
  ?

[Yakov Pechersky]

I'm trying to understand how one would phrase this statement using the proposed classes.
image.png

[Yakov Pechersky]

What I have is the following sketch. IsGalois is stronger than it needs to be to describe an extension. Does this look about right?

import Mathlib

class IsDiscrete' {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] {A : Type*} [Ring A] (v : Valuation A Γ) : Prop where
  exists_generator_lt_one : ∃ (γ : Γˣ), Subgroup.zpowers γ = ⊤ ∧ γ < 1 ∧ ↑γ ∈ Set.range v

variable {K L Γ₀ Γ₀' : Type*}
  [Field K] [Field L]
  [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀']
  [Valued K Γ₀] [Valued L Γ₀']
  -- inlining proposed ValuedLocalField
  [CompleteSpace K] [CompleteSpace L]
  [IsDiscrete' (Valued.v (R := K))] [IsDiscrete' (Valued.v (R := L))]
  [Finite <| IsLocalRing.ResidueField (Valued.v (R := K)).valuationSubring]
  [Finite <| IsLocalRing.ResidueField (Valued.v (R := L)).valuationSubring]
  -- let's simplify to the mixed characteristic case
  [CharZero K]
  [CharZero L] -- is this necessary unde the galois condition, or inferrable?
  -- now we say L/K
  [Algebra K L] [IsGalois K L]
  -- do we need to say `[FiniteDimensional K L]`?

def v_orderIso : Γ₀ →*o Γ₀' := sorry
-- something like
-- gen_Γ₀ ↦ gen_Γ₀' ^ (Ideal.ramificationIdx (algebraMap K L) 𝓂[K] 𝓂[L])

lemma foo (x : K) : Valued.v (algebraMap K L x) = v_orderIso (Valued.v x) := sorry

[Adam Topaz]

I completely lost track of the proposed classes, but it's always possible to take $v(p)/v(\pi)$ where $\pi$ is a uniformizer.

[Yakov Pechersky]

Right, when discussing an extension over the concrete Q_p. Here, I'm discussing an extension over an unspecified base field K.

[Johan Commelin]

Kevin Buzzard said:

My conclusions from thinking about this is that Lean 4's typeclass system is pushing us towards (R : Type*) [Add R] [Mul R] [Neg R] [Zero R] [One R] [IsCommutativeAdd R] [IsDistrib R]... and we have to choose between slowdowns and this explosion

Minor comment: There shouldn't be an explosion of IsFoo assumptions stacked on top of each other. Since those are Prop's they can extend each other (and avoid https://www.ralfj.de/blog/2019/05/15/typeclasses-exponential-blowup.html).
To be precise: they can extend each other if they depend on the same set of types. So you would still have [IsRing R] [IsAddGroup M] [IsModule R M].

[Filippo A. E. Nuccio]

Adam Topaz said:

I completely lost track of the proposed classes, but it's always possible to take $v(p)/v(\pi)$ where $\pi$ is a uniformizer.

Yes, this is the approach we take in our project, and we similarly proved that an extensions is "absolutely unramified" iff p stays a uniformizer.

[Filippo A. E. Nuccio]

Yakov Pechersky said:

What I have is the following sketch. IsGalois is stronger than it needs to be to describe an extension. Does this look about right?

import Mathlib

class IsDiscrete' {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] {A : Type*} [Ring A] (v : Valuation A Γ) : Prop where
  exists_generator_lt_one : ∃ (γ : Γˣ), Subgroup.zpowers γ = ⊤ ∧ γ < 1 ∧ ↑γ ∈ Set.range v

variable {K L Γ₀ Γ₀' : Type*}
  [Field K] [Field L]
  [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ₀']
  [Valued K Γ₀] [Valued L Γ₀']
  -- inlining proposed ValuedLocalField
  [CompleteSpace K] [CompleteSpace L]
  [IsDiscrete' (Valued.v (R := K))] [IsDiscrete' (Valued.v (R := L))]
  [Finite <| IsLocalRing.ResidueField (Valued.v (R := K)).valuationSubring]
  [Finite <| IsLocalRing.ResidueField (Valued.v (R := L)).valuationSubring]
  -- let's simplify to the mixed characteristic case
  [CharZero K]
  [CharZero L] -- is this necessary unde the galois condition, or inferrable?
  -- now we say L/K
  [Algebra K L] [IsGalois K L]
  -- do we need to say `[FiniteDimensional K L]`?

def v_orderIso : Γ₀ →*o Γ₀' := sorry
-- something like
-- gen_Γ₀ ↦ gen_Γ₀' ^ (Ideal.ramificationIdx (algebraMap K L) 𝓂[K] 𝓂[L])

lemma foo (x : K) : Valued.v (algebraMap K L x) = v_orderIso (Valued.v x) := sorry

@Yakov Pechersky I am not sure to understand what you're aiming at.

[Yakov Pechersky]

Let's say we have a tower of extensions of nonarchimedean local fields K/Q_p and L/K, where v is the valuation of K and w is the valuation of L, k is the uniformizer in K and l is the uniformizer in L.. We know that the ramification index of K/Q_p is v(p) / v(k), and similarly, the ramification index of L/Q_p is w(p) / w(l). However, how does one state the similar statement about the ramification index of L/K?

This would be useful, for example, if we were discussing an intermediate field situation, where L/K is totally ramified and K/Q_p is unramified. I'm asking about how to state that L/K is totally ramified -- somehow talk about how w(algebraMap K L k) relates to v(k).

[Yakov Pechersky]

image.png

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

@Filippo A. E. Nuccio and I are working towards constructing the maximal unramified subextension. It is still very much WIP, but Filippo explained our current strategy a few weeks ago in this comment.

[Kevin Buzzard]

In the FLT repo we assume $v$ and $w$ are taking values in the same totally ordered group with 0, and we talk about an $e$ such that for all $x\in K$ we have $w(x)=v(x)^e$, where by $w(x)$ I mean w (algebraMap K L x).

[Filippo A. E. Nuccio]

Consider also that this would be quite easy to prove if we relate the absolute ramification index (i.e. over Q_p) to the valuation of p (which we have in our project), and then using Ideal.ramificationIdx_tower.

[Adam Topaz]

Why don't we just define the ramification degree of $L|K$ to be the size of $L^\times/(K^\times \cdot \mathcal{O}_L^\times)$?

[Adam Topaz]

This also has the benefit of working for any finite extension of valued fields, not just in the local field case.

[Adam Topaz]

In general, I'm a bit concerned that a lot of the discussion above is very specialized to local fields, while most of the desired results hold in much greater generality.

[Filippo A. E. Nuccio]

Well, actually my point is that most of the work has already been done more generally (as in Ideal.ramificationIdx_tower ) and what we do is to try to align to the library as much as possible, so we simply provide a small bridge to what is already available, and rely on that.

[Adam Topaz]

But even this ramificationIdx_tower is only for discrete rank 1 valuations.

[Filippo A. E. Nuccio]

True.

[Filippo A. E. Nuccio]

But I see two (not necessarily disjoint) paths: generalising what is currently in the library and adding results about extensions of local fields. What we're doing, and what I think is the most sensible thing, is to keep the valued fields results aligned to what is already in the library. If we eventually generalise these results, of course the valued fields part can be generalised as well, eg in rank > 1, but departing from what is available only on the valued side seems a bit dangerous, it would make the local/global bridge more painful.

[Kevin Buzzard]

Adam Topaz said:

In general, I'm a bit concerned that a lot of the discussion above is very specialized to local fields, while most of the desired results hold in much greater generality.

The reason I'm pushing for a local fields definition is that I want to start on arithmetic (e.g. the Artin map with no sorried data) for the Oxford class field theory thing and here you definitely need local compactness. I'm aware that $ef\leq n$ holds in huge generality and that $ef=n$ holds quite often (e.g. for complete discretely-valued fields so e.g. completion of field of fractions of a DVR at a nonzero prime), I'm not suggesting we start proving theorems in the wrong generality, but I am really hoping that we can get a definition down which does have these strong arithmetic constraints so I can start proving things like "Q_p is an example" or "completion of a number field at a finite place is an example". To give a concrete example: I need to prove that integers of K_v is compact for K a number field because I want local compactness results for adeles of number fields to prove finiteness of spaces of quaternionic modular forms, which I need for Hecke algebras so I can state R=T theorems. And I felt that it was silly just proving these results for K_v when they should be being proved for a general nonarch local field.

[Adam Topaz]

I understand Kevin. Just to help me catch up again, is the following the current proposal for defining a nonarch local field (of possibly equal characteristic)?

import Mathlib

class IsDiscrete
    {Γ : Type*} [LinearOrderedCommGroupWithZero Γ]
    {A : Type*} [Ring A]
    (v : Valuation A Γ) : Prop where
  exists_generator_lt_one : ∃ (γ : Γˣ), Subgroup.zpowers γ = ⊤ ∧ γ < 1 ∧ ↑γ ∈ Set.range v

open Valued IsLocalRing

variable {Γ K : Type*}
  [Field K]
  [LinearOrderedCommGroupWithZero Γ]
  [Valued K Γ]
  [CompleteSpace K]
  [IsDiscrete (v : Valuation K Γ)]
  [Finite <| ResidueField (v : Valuation K Γ).valuationSubring]

[Kevin Buzzard]

Your IsDiscrete is #23727 but the proposal for local field is #23730 and it's currently a data-carrying class ValuedLocalField (which I'm pushing to be renamed NonarchimedeanLocalField) and which extends docs#Valued .

[Adam Topaz]

ok thanks :)

[Kevin Buzzard]

I have misgivings about extending Valued but my proposal was too extreme in the other direction (drop Valued completely because it's mixing algebra and topology (it wants Ring R and UniformSpace R and it's data so it's going to cause trouble for typeclass inference) and instead have a Prop-valued extension extending Ring, UniformSpace and Preorder. But it was pointed out to me that this would make all statements really unwieldy and that we might want to wait until we have some viable variable? or [[ LocalField ]] thing going. But I like your definition, removing Valued from mathlib will be a pain but I am still reluctant to extend it, I worry that it will just end up being like OrderedSemiring, OrderedRing, OrderedCommRing all over again if we keep allowing extensions of Valued. We removed all the ordered ring stuff and replaced it by docs#IsOrderedRing and got a 20% speedup of typeclass inference across the entire library!

[Kevin Buzzard]

The history of Valued is that it originally came from the perfectoid project when (a) we (or at least I) didn't really know what we were doing (I shouldn't speak for the other authors!) and (b) it was Lean 3, so the typeclass system worked differently. Originally (https://github.com/leanprover-community/mathlib3/pull/9589) Gamma was bundled data in the same universe and it was a class (so you were only allowed on Gamma per R) but there was a diamond issue when it came to completions so in https://github.com/leanprover-community/mathlib3/pull/13691 it was refactored to be the definition you see now, extending uniform rings with more data and with the usual forgetful inheritance note.

[Kevin Buzzard]

It will be a lot of work to remove Valued, but it will be less work than it was to remove ordered rings #20676 , which changed 169 files and took me about 4 hours to review, but resulted in this glorious sea of green including the 20% reduction in typeclass inference.

[Kevin Buzzard]

But until it's gone, people are going to want to extend it which will just result in more work when we're ready to remove it and replace it with some Prop-valued mixin.

[Matthew Jasper]

Kevin Buzzard said:

Your IsDiscrete is #23727 but the proposal for local field is #23720 and it's currently a data-carrying class ValuedLocalField (which I'm pushing to be renamed NonarchimedeanLocalField) and which extends docs#Valued .

#23730

[Adam Topaz]

I agree we should remove it and go with the mixin approach as much as possible. I learned yesterday that it may soon be possible to write macros that expand to binders (maybe @Kyle Miller can confirm?) which would make the dream of [[LocalField F]] et al within reach.

[Matthew Jasper]

So [Valued R Γ] would become (v : Valuation R Γ) [UniformSpace R] [IsTopologicalValuation R v]?

[Kevin Buzzard]

I'm thinking that that is a better design pattern. But if we don't bite the bullet yet with that refactor then I am wondering whether Yakov's

class IsNonarchimedeanLocalField (K Γ : Type*) [Field K]
    [LinearOrderedCommGroupWithZero Γ] [Valued K Γ] : Prop where
  complete : CompleteSpace K
  isDiscrete : IsDiscrete <| Valued.v (R := K)
  finiteResidueField : Finite <| IsLocalRing.ResidueField (Valued.v (R := K)).valuationSubring

is better than #23730 because the analogue is that we're sort of stuck with OrderedRing but at least we avoided OrderedCommRing.

[Kevin Buzzard]

But I should say that I'm not really clear on how good the analogy is. The problem with OrderedRing R is that that say typeclass inference is trying to find an instance of Ring R. The sad and frustrating thing which you would see happening time and time again in problematic slow typeclass searches is that typeclass inference notices the instance OrderedRing R -> Ring R and thinks "ooh I know, maybe I can prove R is a ring by proving it's an ordered ring" and this is just a totally boneheaded move sometimes because you look at the question and it's 100% algebra and there is no partial order anywhere in the question. But the Lean 4 typeclass algorithm does this anyway, especially if it is wrong to be looking for a ring structure on R in which case it tries everything including OrderedRing -> Ring and then all of a sudden it has a new problem, trying to prove that this ring R is ordered, and there is no way of doing this because there is no ordering in the question but it now goes off on a merry dance saying "hmm well maybe I can do this by proving R is well-ordered, no, that didn't work, maybe I can prove it's a lattice, hmm, aah this looks promising, there are lots of ways of proving something is a lattice, maybe I'll now try and prove it's a conditionally complete orderbot lattice" and 2 seconds later when it's half way through traversing the entire order heirarchy for no good reason you've overflowed the heartbeats timer and have an error suggesting you should increase the maxInstanceHeartbeats from 20000.

[Kevin Buzzard]

#20676 made all of those problems go away because now there is no OrderedRing R -> Ring R, there is this completely independent IsOrderedRing R [Ring R] [LE R] which typeclass inference never notices when trying to solve [Ring R] as Ring R is now an input not an output, so you no longer get these crazy traversals of the order heirarchy in questions where there is no order in sight.

[Yakov Pechersky]

To be clear, I was not proposing unbundling the class, I had the snippet above just to provide a currently-working-in-Mathlib example of TC arguments that was an approximation to what's being PR'd. It was a mwe so people could load it and think about the interaction of different valuation groups.

[Kevin Buzzard]

The difference here is that there's this Gamma involved so maybe we don't see the same problems with Valued.

[Kevin Buzzard]

Thinking about it more, I'm now coming to the conclusion that one of my worries (that Valued will cause typeclass inference to do silly things) is spurious. There is this extra Gamma, so maybe [Valued R Gamma] is just like [Module R M] which doesn't cause these typeclass explosions .

I am still concerned about this (Γ₀ : outParam (Type v)) in Valued though. #23727 is saying "we need to move away from Zm0, it's more convenient to work with a general cyclic group with 0" but I think that this means you shouldn't have [Valued R Gamma1] and [Valued R Gamma2] at the same time, and there are instances like docs#FunctionField.valuedFqtInfty giving us Valued (FqtInfty Fq) ℤₘ₀ meaning that for this field that's it now, if you want another valuation or an isomorphic value group then you can't use Valued any more, and I think that this means that you won't be able to have [Valued v.adicCompletion (FqtInfty Fq) Gamma] for a general group with zero Gamma, right? Should docs#FunctionField.valuedFqtInfty not be an instance? But this is an objection to Valued, not to the definition of a local field.

And my other concern (which Yakov's suggestion solves) is that local fields extending Valued and then mixed char ones extending this and equichar ones extending this topo could just result in a big collection of type-valued classes which maybe runs the risk of diamonds, which the Prop variant definitely doesn't have.

I think I'm talking myself into the following conclusion: maybe leave Valued alone for now, but go with Yakov's suggestion in #23730 ?

[Yakov Pechersky]

(Note: I was not suggesting anything! I was trying to work with the API as currently proposed, asking about how Gamma_K and Gamma_L will interact, which Maria Ines and Filippo explained above with the Galois coinsertion work)

[Filippo A. E. Nuccio]

As a matter of fact, we do want to have the liberty of findingValued R Gamma1 and Valued R Gamma2; this is one of the reasons why we pushed away from $\mathbb{Z}_{m0}$. The point is that the valuation from a DVR defined using multiplicities of the maximal ideal is naturally valued in $\mathbb{Z}_{m0}$ while the one used in the Valuation library (as done in Bourbaki) is $K^\times/R\cup\{0\}$-valued; and we ended up realising that it is better to leave with both rather than forcing them to land in the same place and carrying the iso over.

[Kevin Buzzard]

So do you think outParam should be removed from Γ₀ in the definition of docs#Valued ? Can someone remind me what this means in practice for this declaration? I thought it meant "this class comes with a promise that given R, we'll only ever use one Gamma".

[Kevin Buzzard]

In other words, given an R, the class is currently designed in such a way that Lean would only ever expect one instance of Valued R Gamma for one Gamma.

[Kevin Buzzard]

Huh, removing the outParam from the definition of Valued changes the binder type of Γ₀ in Valued.toUniformSpace from implicit to explicit.

[Kevin Buzzard]

#24445 begins to explore this

[Kevin Buzzard]

Why is docs#Valuation.RankOne a class? This is data. Do you want to allow a change of choice in this data? If so it shouldn't be a class. [RankOne v] is currently only used once outside the file in which it's defined, in Topology/Algebra/Valued/NormedValued, and it's used as [hv : RankOne val.v], and then hv is explicitly used 9 times in that file. Shouldn't this be a structure not a class if you want to use it in this way?

[Filippo A. E. Nuccio]

Kevin Buzzard said:

So do you think outParam should be removed from Γ₀ in the definition of docs#Valued ? Can someone remind me what this means in practice for this declaration? I thought it meant "this class comes with a promise that given R, we'll only ever use one Gamma".

I am not sure that this is my mental model of outParam. I think that the point is that variables that are outParam are meant to be outputs of TC, the idea being that when TC looks for [Ring R] [LinearCommGroup G] [Valued R G] it looks for [Ring R] and before trying to come up with some G (and with its LinearCommGroup structure) it tries to find Valued R G: if it finds it, this will output a G, and only at this point will it try to look for a LinearCommGroup structure on this very G. I don't think there is any risk in marking G as outParam in general (sometimes it might be useless), but it makes sense that G becomes explicit if it is not an outParam any more.

[Kevin Buzzard]

I might have all this wrong, I am always a bit unsure about outParams.

[Kevin Buzzard]

The bottom line is: are you planning on doing [Valued K Zm0] and then later on [Valued K (K/O^*)] and, if so, will typeclass inference still be happy?

[Filippo A. E. Nuccio]

I see no reason why it should be unhappy (of course, as long as I do not try to say that these two things coincide)

[Filippo A. E. Nuccio]

But we've been living with outParam in Valued for a while, we already have enough on our plate: perhaps we can postpone this point?

[Kevin Buzzard]

The point of #23727 is "the design pattern used to be that discrete valuations took values in ℤₘ₀ and we want to change it so that discrete valuations can take values in a more general class of groups with 0 which are isomorphic to this because sometimes we want to change the group with 0" (which is something we weren't doing before, the point of Zm0 was so that every discrete valuation could take values there). My question is "is this new design pattern compatible with the outParam in Valued?" and the answer might be "yes", but my understanding of outParam is not good enough to be sure. Thanks for your explanation. I'm still a bit confused by it. Does it answer my question?

[Johan Commelin]

Kevin Buzzard said:

The bottom line is: are you planning on doing [Valued K Zm0] and then later on [Valued K (K/O^*)] and, if so, will typeclass inference still be happy?

If you have

instance : Valued K Zm0 := ...

-- and then a bit later

instance : Valued K (K/O^*) := ...

then Lean will get confused in the outParam case.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

The point of #23727 is "the design pattern used to be that discrete valuations took values in ℤₘ₀ and we want to change it so that discrete valuations can take values in a more general class of groups with 0 which are isomorphic to this because sometimes we want to change the group with 0" (which is something we weren't doing before, the point of Zm0 was so that every discrete valuation could take values there). My question is "is this new design pattern compatible with the outParam in Valued?" and the answer might be "yes", but my understanding of outParam is not good enough to be sure. Thanks for your explanation. I'm still a bit confused by it. Does it answer my question?

Oh, now I understand your question better, sorry.

[Filippo A. E. Nuccio]

Ah, and Johan replied... :smile:

[Filippo A. E. Nuccio]

...and the two of you together convinced me that it is indeed a good idea to remove it :sweat_smile:

[Kevin Buzzard]

I agree that this is not something which #23727 should be doing!

[Filippo A. E. Nuccio]

But we must certainly fix it before going towards #23730

[Antoine Chambert-Loir]

The more I read of this, the more I believe that any specific choice of valuation has to be taken out of the story.

[Antoine Chambert-Loir]

could statements be given as “there is a valuation such that… ” for the definition of the structure, and “this valuation is such that…” when we use it?

[Kevin Buzzard]

I can quite believe that in a completely natural proof we might want a Zm0-valued valuation and a real-valued one. The question is how to use docs#Valued in that situation (or if we should be using it at all?).

[Adam Topaz]

I think that eventually we should shift toward mixins of the following form:

import Mathlib

open Topology in
class IsTopologicalValuation
    {R Γ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ] [TopologicalSpace R]
    (v : Valuation R Γ) : Prop where
  condition : ∀ s, s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γˣ, { x : R | v x < γ } ⊆ s

class IsValuativePreorder
    {R Γ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ] [Preorder R]
    (v : Valuation R Γ) : Prop where
  condition : ∀ a b : R, a ≤ b ↔ v a ≤ v b

[Adam Topaz]

Then the "discrete" condition would be a class on $\Gamma$ itself:

class IsDiscreteRankOne (Γ : Type*) [LinearOrderedCommGroupWithZero Γ] : Prop where
  condition : Nonempty (Γˣ ≃* Multiplicative ℤ)

(or some alternative e.g. as suggested by @Filippo A. E. Nuccio in the PR)

[Adam Topaz]

I don't think removing the outParam from Valued will really solve much. Yes, that means you would be able to write Valued K G for various Gs, but Lean is very likely to get confused about what G you're using unless you tell it explicitly. Also, maybe G is fixed, but you have a different normalization. For example, think about $\mathbb{C}_p$ with its canonical valuation. The value group (additive, without zero) is $\mathbb{Q}$, and you can normalize this single value group by choosing any positive rational to be the valuation of $p$. I think v itself has to be a parameter to what ever class we end up with.

[Kevin Buzzard]

Adam's comments are convincing. It's difficult to imagine typeclass inference working with Valued and also having the flexibility to change both v and Gamma.

[Filippo A. E. Nuccio]

Well, but in our definition local fields have finite residue fields (as in Serre's book) and therefore have a unique preferred valuation. I think that @Adam Topaz suggestions are very much reasonable if we're trying to set-up the more general notion of "valuable" (nonarchimedean, say) field.

Our starting observation is that in practice almost all proofs/arguments require the choice of a valuation, and typically consider the normalized one. In this sense, although in principle a local field can come with several valuations (but not "as many" as $\mathbb{C}_p$, in the sense that there exists a preferred one), fixing the normalized valuation on it is the first step one systematically performs.

The situation reminded us very much of the class TopologicalSpace.MetrizableSpace, together with its def TopologicalSpace.metrizableSpaceMetric: observe that even for metrizable spaces, most of the library is developed for MetricSpace and the user systematically applies the def. In this perspective, it seems to me that

• Adam's and Antoine's suggestions somewhat go towards defining a parallel of the Metrizable structure;
• Our work is alike the Metric structure, in the sense that we're setting up the technology needed to formalise all statements/proofs that use, or involve, the normalized valuation.

Am I wrong in saying that we seem to be addressing two problems at once (and, if so, we might want to find two separate solutions, so it feels like we're going back to the ValuedLocalField proposal), namely:

1. What is the most elegant set-up to speak about a valuable field, possibly with the least number of assumptions? And
2. What is the best approach to put your hands on all proofs e.g. in Serre's Local Fields that use the normalised valuation all over the places?

[Kevin Buzzard]

and therefore have a unique preferred valuation

But they don't have a unique preferred valuation any more because in #23727 you want to move away from Zm0 so suddenly there is this ambiguity in Gamma

[Kevin Buzzard]

And right now the entire theory is set up so that Gamma is supposed to be uniquely guessable

[Filippo A. E. Nuccio]

Oh well, concerning the "guessability" of Gamma, I agreed with you that this should be removed

[Filippo A. E. Nuccio]

At any rate, I am in principle OK with Adam's approach, so long we have a way, given a local field and a Gamma (with the right assumptions, like "being isomorphic to Z", morally), to pick up "the normalized Gamma-valued valuation "

[Filippo A. E. Nuccio]

But, as expressed in my message above, it is not entirely clear to me if we're not trying to solve the problem "this definition involves valuations whereas it should not be part of the data", by shifting away from a design that concretely provides us with a working way to swiftly pick up a discrete valuation on every local field.

[Kevin Buzzard]

What would you want for the choice of Gamma for this discrete valuation? Would the idea be that the user provides it or would you want this swift discrete valuation to take values in Zm0? I think design decisions will be affected by how exactly you want to use this general cyclic Gamma, and you and Maria Ines know about this much better than anyone else.

[Filippo A. E. Nuccio]

We expected the author to provide it explicitly, but I am experimenting something along Adam's suggestions. I hope to soon report on the outcome.

[Yakov Pechersky]

Note on the following: I am not trying to bikeshed on the class, and have been working at trying to generalize my previous work from NontriviallyNormedField to Valued, because I trust in our common designs.

The difference between Valued and MetricSpace is that in MetricSpace, we don't parametrize over an arbitrary linearly ordered (semi) field. We could, but for all intents and purposes, they would be injective into or isomorphic as ordered (semi)fields to the reals.

If we are working here over the extensions (not necessarily finite) over Q_p, and talking about discrete and normalized valuations, then necessarily these are rank one valuations. If discrete, they _could_ take values in Zm0. And thus, they can take values in NNReal in a way that is compatible with "upgrading" the valuation to a nonarchimedean norm. Yes, the "base" of the norm in the upgrade is arbitrary, but the uniform space structure is the same -- the norms are equivalent.

I understand why going all the way to the norm is limiting for further generalizations, and makes it a little clunky if discussing how valuations extend in extensions. But if we're comparing to MetricSpace, I would say the more parallel comparison is to NontriviallyNormedField. And Valued is a class that does not have a parallel between MetrizableSpace and MetricSpace.

I can't find it right now, but I remember working on a PR with Maria Ines and David Loeffler where we upgraded to a NormedAddGroup during a proof about some nonarchimedean sums (iirc) . The statement didn't refer to a norm, but one could do the upgrade and use the more narrow lemmas.

[Adam Topaz]

FWIW, here is how I would set up the notion of a (possibly equal characteristic) nonarch local field:

import Mathlib

open Topology in
class Valuation.IsTopologicalValuation
    {R Γ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ] [TopologicalSpace R]
    (v : Valuation R Γ) : Prop where
  condition : ∀ s, s ∈ 𝓝 (0 : R) ↔ ∃ γ : Γˣ, { x : R | v x < γ } ⊆ s

open Multiplicative in
class Valuation.IsDiscreteRankOne
    {R Γ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation R Γ) : Prop where
  condition : Nonempty <| (MonoidHom.mrange v.toMonoidHom) ≃* ℤₘ₀

abbrev Valuation.ResidueField {K Γ : Type*}
    [Field K] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) : Type _ := IsLocalRing.ResidueField v.valuationSubring

variable
  {K Γ : Type*} [Field K] [LinearOrderedCommGroupWithZero Γ] {v : Valuation K Γ}
  [UniformSpace K] [TopologicalDivisionRing K]
  [v.IsTopologicalValuation] [v.IsDiscreteRankOne]
  [CompleteSpace K] [Fintype v.ResidueField]

[Adam Topaz]

Note that this doesn't assume that the valuation is surjective onto $\Z$ with zero, but just that its image is isomorphic to this.

[Yakov Pechersky]

BTW Nonempty <| (MonoidHom.mrange v.toMonoidHom) ≃* ℤₘ₀ is equivalent to not DenselyOrdered: docs#LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered. This does require MulArchimedean, but if you had such an mul-order-iso, you could transfer over MulArchimedean.

[Adam Topaz]

But not all value groups that show up in nature are MulArchemedean :)

[Adam Topaz]

For example you may want to consider the $x$-adic valuation on $k(x)$ taking values in the value group of the rank 2 valuation on $k(x,y)$ associated to the flag $(x = y = 0) \subset (y = 0)$.

[Yakov Pechersky]

Yes, agreed, but the mrange would be! If the mrange is mul-order-iso to Zm0.

[Adam Topaz]

Concretely the value group of the rank 2 valuation is $\Z \times \Z$ with the lexicographic order and the value group of the valuation on $k(x)$ is $0 \times \Z$.

[Adam Topaz]

Oh, I see.

[Yakov Pechersky]

As seen in the statement of docs#isPrincipalIdealRing_iff_not_denselyOrdered

[Yakov Pechersky]

(Ah, that statement does have MulArchimedean Γ₀ ...)

[Adam Topaz]

So you want something like this:

open Multiplicative in
class Valuation.IsDiscreteRankOne
    {R Γ : Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation R Γ) : Prop where
  rankOne : MulArchimedean <| MonoidHom.mrange v
  nonDense : ¬ (DenselyOrdered <| MonoidHom.mrange v)

[Yakov Pechersky]

Yes, these are all equivalent.

[Yakov Pechersky]

And I'm pretty sure that if you have a mul-order-iso to Zm0, that is unique. Haven't formalized it.

[Adam Topaz]

Yeah it's unique, there is a unique largest element $< 1$ which is "the value of a uniformizer".

[Adam Topaz]

These are all props at the end of the day, so we can pretty easily go back and forth between the various approaches.

[Matthew Jasper]

Yakov Pechersky said:

And I'm pretty sure that if you have a mul-order-iso to Zm0, that is unique. Haven't formalized it.

https://github.com/matthewjasper/mathlib4/commit/ebefa469e075a5226a56111c75b972a0217f00eb has a proof for Unique (ℤₘ₀ ≃*o ℤₘ₀), which is most of the way there.

[Filippo A. E. Nuccio]

Thanks! I am currently trying to perform some tests on our repo but I am very busy in Beijing and cannot work a lot on the project until next Tue. I will probably use much of the work I'm seeing here though :smile: