Are the adeles Polish?

Stream: FLT

[Thomas Browning]

Here's a start: FLT#798. One annoying thing that I'm running into is that I need a docs#BorelSpace instance on the quotient, but the only one I can seem to find is docs#QuotientAddGroup.borelSpace which requires a docs#PolishSpace assumption. Will this cause problems?

[Kevin Buzzard]

Huh! So again we're in the situation where I want to put the borel measure on everything but those helpful measure theorists have decided to put another measure space structure on a quotient so if we don't want to cause diamonds I need to hope that my objects satisfy their properties. Hopefully they do but I don't know this time. Everything is a finite product of $\mathbb{A}_\mathbb{Q}.$ Are the adeles of $\mathbb{Q}$ a Polish space? I don't know of any natural metric on them (there's a natural norm on the ideles but the product doesn't converge on the adeles) but maybe there's some general nonsense argument? Is the restricted product of polish spaces over compact open subspaces a polish space?

[Kevin Buzzard]

To be honest I find this sort of thing fascinating. I don't ever remember seeing a discussion of this sort of thing in the literature but formalisation makes you honest.

[Kevin Buzzard]

Does your theorem need the measure space structure on the quotient or can you just use Haar measure on everything? For sure everything is locally compact and second countable.

[David Michael Roberts]

A countable product of Polish spaces is Polish. A subspace of Polish is Polish iff it is the countable intersection of a sequence of opens. This feels close?

[Kevin Buzzard]

Unfortunately the adeles don't get the subspace topology. However if a countable product of polish spaces is polish then maybe a countable restricted product will be too.

This is not a problem for Fermat because the version of blichfeldt in mathlib will apply; the fundamental domain approach will work and this doesn't need the polish assumption. It would not surprise me if it's very easy to check that adeles are polish though, it's just not a question I've ever seen before and I don't know the first thing about polish spaces.

[Kevin Buzzard]

Is a countable direct limit of polish spaces polish? That would also do it

[David Michael Roberts]

Are the adeles completely metrisable?

[David Michael Roberts]

They (adeles of Q) feel like they should be a separable space

[Kevin Buzzard]

I don't know. I don't know of any natural real-valued function on them which sends nonzero things to nonzero things.

[Kevin Buzzard]

All the components are metric spaces and indeed normed fields but the product of the local norms of the components of an element can diverge to zero

[David Michael Roberts]

I'm thinking more like how the Fréchet metric is defined on smooth functions as the weighted infinite sum of the C^k metrics. The C^k metrics come from norms, but the Fréchet metric doesn't. So you have the norms on each Q_p (and R), but you sum them, and the result is only a metric, not anything like norm.

[David Michael Roberts]

This is a complete metric on C^\infty, even though C^\infty is not complete in any of the C^k norms

[David Michael Roberts]

However I have no idea if the adele topology can be described this way

[David Michael Roberts]

I admit it does seem unlikely, and in which case apologies for the distraction!

[Scott Carnahan]

Zp and R are Polish, so the countable product Zhat x R is Polish. To get adeles, we just need to take a union of dilations by 1/n, so is Polishness preserved by taking this union?

[Kevin Buzzard]

Right -- is a countable direct limit of polish spaces polish?

[Notification Bot]

17 messages were moved here from #FLT > Fundamental domains by Kevin Buzzard.

[Kevin Buzzard]

Is every second-countable locally compact Hausdorff space automatically Polish? Again just showing my ignorance here.

[Aaron Liu]

yes!
https://topology.pi-base.org/spaces?q=Second+countable+%2B+Locally+compact+%2B+%24T_2%24+%2B+%7EPolish

[Kevin Buzzard]

Well we seem to be missing an instance:

variable (X : Type*) [TopologicalSpace X]
  [SecondCountableTopology X]
  [T2Space X] [LocallyCompactSpace X] in
#synth PolishSpace X -- fails

but I think this will do it.

[Aaron Liu]

seems to be

• urysohn metrization
• locally compact metrizable spaces are completely metrizable

[Kevin Buzzard]

I wonder if we can take a short cut in this case. The measurable space on a quotient is just

instance Quotient.instMeasurableSpace {α} {s : Setoid α} [m : MeasurableSpace α] :
    MeasurableSpace (Quotient s) :=
  m.map Quotient.mk''

and one can ask whether it's true that for the quotient of an abelian topological group by a closed subgroup, the pushforward of the Borel measure is the Borel measure under mild assumptions. Pushforwards of topologies along quotient maps in group theory are really nicely behaved -- for example IIRC they are open quotient maps. Is this enough?

[David Michael Roberts]

Here's me worrying whether the adeles are locally compact , because of the weird restricted product topology and my complete unfamiliarity with p-adic topologies. Because I had found that the nLab has

"A locally compact Hausdorff space is Polish iff it is second-countable."
https://ncatlab.org/nlab/show/Polish+space#further_examples

[Aaron Liu]

is the borel space on the pushforward (quotient) topology the same as the pushforward of the borel space? found a counterexample

[Kevin Buzzard]

Yeah the adeles had better be locally compact because this is what makes Tate's thesis work. An infinite product of compact spaces is compact, but an infinite product of locally compact spaces is not in general locally compact: for example the "big" space $\mathbb{R}\times\prod_p\mathbb{Q}_p$ which the adeles sit in algebraically is \emph{not} locally compact because neither the $p$-adics $\mathbb{Q}_p$ nor the reals are compact, and the definition of open sets in the product topology forces lots of these things in, so you can't find a compact neighbourhood of 0. But even though this "big" space is a great place to put the adeles algebraically, topologically it is the wrong model. The adeles are topologised to make $\R\times\prod_p\Z_p$ an open subgroup, and this is locally compact so we're fine.

[Kevin Buzzard]

Tate's thesis shows that a bunch of classical results about analytic and meromorphic continuation of $L$-functions of Hecke characters (simplest example: the Riemann zeta function) can be deduced very elegantly using abstract Fourier analysis and Pontrjagin duality on the adeles, which applies because the adeles are locally compact.

[Kevin Buzzard]

I've got sorry-free instances for adeles of a number field being locally compact and Hausdorff, so it's only the hardest bit (second countable) left.
Modulo #Is there code for X? > second countable topology question @ 💬 I have the infinite places; the hardest question
instance : SecondCountableTopology (FiniteAdeleRing (𝓞 K) K) := sorry remains.

[Kevin Buzzard]

OK I think I have a plan for SecondCountableTopology (FiniteAdeleRing) so the only thing left is why it's Polish. I might try Aristotle on this...

[Aaron Liu]

Kevin Buzzard said:

so the only thing left is why it's Polish.

By urysohn metrization theorem (docs#TopologicalSpace.metrizableSpace_of_t3_secondCountable), the space is metrizable. It is second countable by assumption. And it's completely metrizable because it's locally compact and metrizable (I saw a draft PR with an intermediate result for this, #32706).

[Stepan Nesterov]

Here's what I got:

import Mathlib.Topology.Metrizable.Urysohn
import Mathlib.Topology.MetricSpace.Polish
import Mathlib.Topology.UniformSpace.Completion
import Mathlib.Topology.MetricSpace.Completion

open TopologicalSpace UniformSpace Set Topology

lemma open_of_locally_compact_dense_metrizable {X Y : Type*} [TopologicalSpace X]
    [MetrizableSpace X] [TopologicalSpace Y] [MetrizableSpace Y] [LocallyCompactSpace Y]
    (f : Y → X) (hf : Continuous f) (indf : IsInducing f) (dn : DenseRange f) :
    IsOpen (Set.range f) := by
  rw [isOpen_iff_mem_nhds]
  intro x hx
  rw [_root_.mem_nhds_iff]
  rw [mem_range] at hx
  obtain ⟨y, hy⟩ := hx
  obtain ⟨s, s_op, y_in_s, s_cc⟩ := exists_isOpen_mem_isCompact_closure y
  rw [IsInducing.isOpen_iff indf] at s_op
  obtain ⟨t, t_op, s_preim_t⟩ := s_op
  have clt_im_cls : closure t = closure (f '' s) := by
    rw [Subset.antisymm_iff]
    constructor
    · refine closure_minimal ?_ isClosed_closure
      intro z hz
      rw [mem_closure_iff]
      intro o o_op z_in_o
      unfold DenseRange at dn
      rw [dense_iff_inter_open] at dn
      specialize dn (o ∩ t) (o_op.inter t_op) ⟨z, z_in_o, hz⟩
      have : t ∩ range f = f '' s := by
        rw [← s_preim_t]
        exact Eq.symm image_preimage_eq_inter_range
      rw [inter_assoc, this] at dn
      exact dn
    · apply closure_mono
      intro z hz
      obtain ⟨w, hw, h⟩ := hz
      rw [← h]
      rw [← s_preim_t] at hw
      exact hw
  use t
  refine ⟨?_, t_op, ?_⟩
  · calc
      t ⊆ closure t := subset_closure
      _ = closure (f '' s) := clt_im_cls
      _ ⊆ range f := by
        rw [← closure_image_closure hf]
        have : IsClosed (f '' closure s) := by
          apply IsCompact.isClosed
          exact IsCompact.image s_cc hf
        rw [IsClosed.closure_eq this]
        exact image_subset_range f (closure s)
  · rw [← hy]
    rw [← s_preim_t] at y_in_s
    exact y_in_s

theorem polish_of_locally_compact_second_countable (X : Type*) [TopologicalSpace X] [SecondCountableTopology X] [T2Space X]
    [LocallyCompactSpace X] : PolishSpace X := by
  letI _ : MetrizableSpace X := metrizableSpace_of_t3_secondCountable X
  letI _ : MetricSpace X := metrizableSpaceMetric X
  have dn : IsOpen (range (Completion.coe' : X → Completion X)) := by
    apply open_of_locally_compact_dense_metrizable Completion.coe'
    exact Completion.continuous_coe X
    exact IsDenseInducing.isInducing Completion.isDenseInducing_coe
    exact Completion.denseRange_coe
  letI _ : PolishSpace (range (Completion.coe' : X → Completion X)) :=
    IsOpen.polishSpace dn
  have hHomeo : X ≃ₜ range (Completion.coe' : X → Completion X) :=
    (Completion.coe_isometry.isEmbedding).toHomeomorph
  exact hHomeo.isClosedEmbedding.polishSpace

[Stepan Nesterov]

Actually you can replace MetrizableSpace X Y with T2Space X Y

[Kevin Buzzard]

Aristotle did it too but its proof was longer

[David Michael Roberts]

FWIW here's an explicit metric for the adeles, and moreover the adeles inside the unrestricted product are carved out by the expression being < \infty

https://mathoverflow.net/a/504887/4177

[David Michael Roberts]

Screenshot 2025-12-12 at 10.18.52 AM.png

[David Michael Roberts]

I don't know if this helps with thinking about the Haar measure, but just in case...

[Thomas Browning]

Looks like one other thing we'll need is that D_𝔸 has infinite measure, so that we can construct a set of large measure (see FLT#798). Do we know this?

[Kevin Buzzard]

My proposal here was to write down an arbitrary compact open subgroup at the finite places and take the product with a large closed ball at the infinite place.

[Anatole Dedecker]

Let me just note that since the adeles already come with a uniform structure, it would be cleaner to show that the uniform structure is complete and countably generated (not just that there exists such a uniform structure)

[Anatole Dedecker]

More precisely, the fact that the uniformity is countably generated should come pretty easily from docs#IsUniformAddGroup.uniformity_countably_generated, and then there is a general statement that locally compact groups are complete (I don’t remember seeing this in Mathlib, but I haven’t searched for it)

[Anatole Dedecker]

I think both approaches are valuable: in the specific case of the adeles, this tells you more than "they are Polish". But there is also the statement that a reasonable restricted product is Polish, which is less strong but more general.

[Kevin Buzzard]

FLT#797 (just merged) contains proofs that the adeles of a number field are locally compact, T2 and second countable (and also the construction of a fundamental domain for $\mathbb{Q}$ in $\mathbb{A}$ in case the measure theory approach doesn't work out ;-) ). Sounds like second countable was not quite the right thing to prove and I should have instead proved that the uniformity IsCountablyGenerated but maybe this follows? I don't know if it's just abstract nonsense now.

[Anatole Dedecker]

The fact that the uniformity is countably generated definitely follows, thanks to IsUniformAddGroup.uniformity_countably_generated (and indeed you need way less than second-countable).

[Anatole Dedecker]

The problem is completeness. I checked this weekend to be sure I wasn't saying nonsense, but it seems that there are indeed Polish groups which are not complete for their (left or right, it doesn't matter) uniform structure. This is because the uniformity induced by some complete distance and the uniformity induced by the group structure have no reason to coincide.
It also seems, however, that this pathology disappears in the abelian case, but I haven't thought about the proof.

[Anatole Dedecker]

In any case, I think Mathlib deserves to know that a locally compact uniform group is complete (maybe it does already ?), and this is the "correct" proof in your setting.

[Bryan Wang]

On the completeness of locally compact groups, I couldn't find it in mathlib, but here's what I have:

import Mathlib

open Set Filter
open scoped Pointwise

example {G : Type*} [Group G] [UniformSpace G] [IsUniformGroup G] [LocallyCompactSpace G] : CompleteSpace G := by
  constructor; intro f ⟨hfn, hf⟩
  obtain ⟨K, hK, hKf⟩ : ∃ K : Set G, IsCompact K ∧ K ∈ f := by
    obtain ⟨K', hK', hK'₁⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)
    let U : Set (G × G) := {p : G × G | p.1⁻¹ * p.2 ∈ K'}
    have hU : U ∈ uniformity G := by rw [uniformity_eq_comap_inv_mul_nhds_one]; exact preimage_mem_comap hK'₁
    obtain ⟨S, hSf, hSU⟩ : ∃ S ∈ f, S ×ˢ S ⊆ U := by
      rcases mem_prod_iff.1 (hf hU) with ⟨A, hA, B, hB, hAB⟩
      exact ⟨A ∩ B, ⟨inter_mem_iff.mpr ⟨hA, hB⟩, (prod_mono inter_subset_left inter_subset_right).trans hAB⟩⟩
    obtain ⟨x, hx⟩ := f.nonempty_of_mem hSf
    exact ⟨x • K', hK'.smul x, mem_of_superset hSf (fun y hy ↦ ⟨x⁻¹ * y, hSU <| mk_mem_prod hx hy, by simp⟩)⟩
  obtain ⟨x, hx, h⟩ := hK.isComplete f ⟨hfn, hf⟩ <| le_principal_iff.mpr hKf
  exact ⟨x, h⟩

[Kevin Buzzard]

Please PR to mathlib!

[Bryan Wang]

#32944