Zp is compact?

Stream: Is there code for X?

[David Loeffler]

Is there a proof formalised somewhere that the p-adic integers (with the usual topology) is a compact space?

I didn't find one in Mathlib, but maybe this has come up in FLT? (@Kevin Buzzard ?)

[Johan Commelin]

@loogle CompactSpace, PadicInt

[loogle]

:shrug: nothing found

[Johan Commelin]

huh?! I'm sure it must be there

[David Loeffler]

Johan Commelin said:

huh?! I'm sure it must be there

Yes, that was my reaction too :surprise:

[Johan Commelin]

Aah, we do have

instance completeSpace : CompleteSpace ℤ_[p] :=
  have : IsClosed { x : ℚ_[p] | ‖x‖ ≤ 1 } := isClosed_le continuous_norm continuous_const
  this.completeSpace_coe

which is of course not what you are asking for

[Johan Commelin]

But I'm still relieved to find it

[Johan Commelin]

I really need to converge to a train now. But I'm sorta taking this personally, that this fact seems to be missing. :stuck_out_tongue_wink:

[Johan Commelin]

@Filippo A. E. Nuccio Do you have more api for dvr's in your project? Like "dvr is compact iff it is complete with finite residue field"

[Johan Commelin]

Or in general, stuff about metric/topology wrt dvrs?

[Johan Commelin]

Examples like $\Z_p$ come with their own metric and topology. So in general we don't want to construct those as instance from the algebraic data. Instead, we should assume them, and have a mixin like [TopologicalDVR R]

[Johan Commelin]

I'm not yet sure if that should assume a metric or only a topology.

[David Loeffler]

With the machinery in mathlib it’s reasonably easy to show that Zp bijects with compatible sequences in the product of ZMod (p^n), and that the latter is compact (in the product topology). However checking that the product top on sequences corresponds to the p-adic metric looks like it will be tedious. (I guess this is an instance of Johan’s last comment.)

[Filippo A. E. Nuccio]

Johan Commelin said:

Filippo A. E. Nuccio Do you have more api for dvr's in your project? Like "dvr is compact iff it is complete with finite residue field"

No, we do not have this yet.

[Johan Commelin]

#16498 does a tiny cleanup of the import structure around DVRs

[David Loeffler]

Tagging @Ashvni Narayanan since this must have come up in her PhD thesis.

[Yakov Pechersky]

I am working on this, almost there. I think @Jou Glasheen has the precise result for Z_p while my PRs are converging to the general result about the conditions for a nonarchimedean field to be locally compact.

[Yakov Pechersky]

For example, I have PRs open that deal with the finite residue field and the complete ring of integers portion. And I have a branch where I have proven

variable {F Γ₀ O : Type*} [Field F] [LinearOrderedCommGroupWithZero Γ₀]
  [CommRing O] [Algebra O F] {v : Valuation F Γ₀}

lemma isPrincipalIdealRing_iff_not_denselyOrdered [MulArchimedean Γ₀] (hv : Integers v O) :
    IsPrincipalIdealRing O ↔ ¬ DenselyOrdered (Set.range v) := sorry

[Yakov Pechersky]

Finite residue field portion: #15424
Complete iff unit ball complete: #15777
IsPrincipalIdealRing iff not DenselyOrdered: branch#pechersky/valuation-integers-zm0

[Yakov Pechersky]

Happy to give more details. I wrote out a small roadmap of the necessary APi to get to the "locally compact iff complete and finite residue field" recently. I can share it later and try to annotate it with the PRs I have out.

[Jou Glasheen]

I have this sorry-free for Zp! I am working on it with @Kevin Buzzard for my MSc. I can PR it, if helpful (I have not PR'd something before, so this may be relatively slow).

[Jou Glasheen]

Specifically, I have

    TotallyBounded (Set.univ : Set ℤ_[p])```

and
``` theorem is_compact : IsCompact (Set.univ : Set ℤ_[p]) := ```

and
```theorem locally_compact_space :
    LocallyCompactSpace ℚ_[p] :=```

[David Loeffler]

Please do PR it, that would be great! Happy to help with reviewing / cleanup.

[Jou Glasheen]

David Loeffler said:

Please do PR it, that would be great! Happy to help with reviewing / cleanup.

Thank you! I will do this rn.

[Jou Glasheen]

@David Loeffler @Yakov Pechersky I opened this PR #16505 https://github.com/leanprover-community/mathlib4/pull/16505 Not sure if I did this correctly.

[Johan Commelin]

I'm really quite happy to learn about all this progress that I was unaware of 12 hours ago :octopus:

[Ashvni Narayanan]

David Loeffler said:

Tagging Ashvni Narayanan since this must have come up in her PhD thesis.

Hello! Sorry I'm just seeing this. If the question is regarding Z_p is compact, I did prove this in Lean 3. In particular, I had shown that Z_p is profinite. All the code is here . I managed to partly port some of the code to Lean4, which is here.

If you are looking for results regarding Z_p, ZMod or Bernoulli numbers, there is a high chance it exists in these repos. Happy to assist further in any way I can! :)

[Ruben Van de Velde]

Your links seem to be broken

[David Loeffler]

@Ashvni Narayanan did you formalize the Amice--Velu--Vishik extension of Mahler's theorem, that one can characterize the functions on $\mathbb{Z}_p$ that are of class $C^{\alpha}$, for $\alpha \in \mathbb{R}_{\ge 0}$, in terms of the decay rate of their Mahler coefficients?

[Ashvni Narayanan]

David Loeffler said:

Ashvni Narayanan did you formalize the Amice--Velu--Vishik extension of Mahler's theorem, that one can characterize the functions on $\mathbb{Z}_p$ that are of class $C^{\alpha}$, for $\alpha \in \mathbb{R}_{\ge 0}$, in terms of the decay rate of their Mahler coefficients?

I don't think so

[Ashvni Narayanan]

Ruben Van de Velde said:

Your links seem to be broken

Apologies! It should be working now.

[Ashvni Narayanan]

David Loeffler said:

Ashvni Narayanan did you formalize the Amice--Velu--Vishik extension of Mahler's theorem, that one can characterize the functions on $\mathbb{Z}_p$ that are of class $C^{\alpha}$, for $\alpha \in \mathbb{R}_{\ge 0}$, in terms of the decay rate of their Mahler coefficients?

There is now a group of students working on this

[David Loeffler]

Glad to hear it! I hope this code will actually make it into mathlib eventually ("mathlib or it didn't happen" as the expression is). My student Giulio Caflisch at ETH is working on getting Mahler's theorem itself into mathlib.

[Ashvni Narayanan]

David Loeffler said:

Glad to hear it! I hope this code will actually make it into mathlib eventually ("mathlib or it didn't happen" as the expression is). My student Giulio Caflisch at ETH is working on getting Mahler's theorem itself into mathlib.

Ah ok! This is what the students at BICMR have also begun working on, before getting to the Mahler basis.

[Jz Pan]

Ashvni Narayanan said:

David Loeffler said:

Glad to hear it! I hope this code will actually make it into mathlib eventually ("mathlib or it didn't happen" as the expression is). My student Giulio Caflisch at ETH is working on getting Mahler's theorem itself into mathlib.

Ah ok! This is what the students at BICMR have also begun working on, before getting to the Mahler basis.

Hi! Do you have plan to formalize various distribution spaces over Qp in Colmez's 1998 paper Theorie d'Iwasawa des representations de de Rham d'un corps local?

[Jz Pan]

David Loeffler said:

Is there a proof formalised somewhere that the p-adic integers (with the usual topology) is a compact space?

I didn't find one in Mathlib

... which means that currently mathlib doesn't know Zp is profinite. Maybe profinite is a better approach?

[David Loeffler]

Actually compactness of Zp is in mathlib now – Jou Glasheen announced her PR in this thread (2 months ago) and it was merged shortly afterwards.

[David Loeffler]

I think we still don't have profiniteness though; the existing library code about Zp and Qp is developed from a more analytic, norm/metric/Cauchy-sequence viewpoint, and I'm not sure anyone's yet tried to link it up with the super-abstract categorical approach to profinite spaces elsewhere in the library. EDIT: this is wrong, see below.

@Dagur Asgeirsson @Adam Topaz any thoughts?

[Johan Commelin]

The definition of profinite is still the topological one, right? So showing that Z_[p] is totally disconnected/separated should be enough. (I assume Hausdorff is done.)

[David Loeffler]

Johan Commelin said:

The definition of profinite is still the topological one, right? So showing that Z_[p] is totally disconnected/separated should be enough. (I assume Hausdorff is done.)

Apparently I am wrong! What a nice thing to be wrong about :smile:

#check Profinite.of ℤ_[p]
/- Profinite.of ℤ_[p] : Profinite -/

Many thanks to @Jou Glasheen and @Yakov Pechersky for adding the instances showing that Zp is compact and totally disconnected, which are the inputs to this.

[Jou Glasheen]

David Loeffler said:

Johan Commelin said:

The definition of profinite is still the topological one, right? So showing that Z_[p] is totally disconnected/separated should be enough. (I assume Hausdorff is done.)

Apparently I am wrong! What a nice thing to be wrong about :smile:

#check Profinite.of ℤ_[p]
/- Profinite.of ℤ_[p] : Profinite -/

Many thanks to Jou Glasheen and Yakov Pechersky for adding the instances showing that Zp is compact and totally disconnected, which are the inputs to this.

Thanks! This is good to know (profinite was the goal).

[Ashvni Narayanan]

Jz Pan said:

Ashvni Narayanan said:

David Loeffler said:

Glad to hear it! I hope this code will actually make it into mathlib eventually ("mathlib or it didn't happen" as the expression is). My student Giulio Caflisch at ETH is working on getting Mahler's theorem itself into mathlib.

Ah ok! This is what the students at BICMR have also begun working on, before getting to the Mahler basis.

Hi! Do you have plan to formalize various distribution spaces over Qp in Colmez's 1998 paper Theorie d'Iwasawa des representations de de Rham d'un corps local?

Yes, there is definitely interest in this area and on the radar. I can put you in touch with the people who are working in this direction, if you like.

[Jz Pan]

Ashvni Narayanan said:

Jz Pan said:

Ashvni Narayanan said:

David Loeffler said:

Glad to hear it! I hope this code will actually make it into mathlib eventually ("mathlib or it didn't happen" as the expression is). My student Giulio Caflisch at ETH is working on getting Mahler's theorem itself into mathlib.

Ah ok! This is what the students at BICMR have also begun working on, before getting to the Mahler basis.

Hi! Do you have plan to formalize various distribution spaces over Qp in Colmez's 1998 paper Theorie d'Iwasawa des representations de de Rham d'un corps local?

Yes, there is definitely interest in this area and on the radar. I can put you in touch with the people who are working in this direction, if you like.

Sure!

[David Loeffler]

My student Giulio Caflisch at ETH is working on getting Mahler's theorem itself into mathlib.

PR #19340 adds the key technical lemma for Mahler's theorem, which is that the iterated forward differencesΔ^[n] f 0 tend to 0 for all continuous functions f on ℤ_[p].

[Jz Pan]

Maybe someone could also look at this #maths>Refactor `krullTopology`? which should be related to "Zp is compact" discussion.