Zulip Chat Archive

Stream: general

Topic: Extension of valuation to completion creates diamond?


Oliver Nash (Apr 21 2022 at 18:09):

Given a valued field KK, there seem to be two ways to obtain a uniform space structure on its completion K^\hat K.

  1. The uniform space space structure that it carries because it is a completion.
  2. The uniform space structure induced by the extension of the valuation to K^\hat K.

I haven't thought about it but I presume these are mathematically equal. Is that true?

Oliver Nash (Apr 21 2022 at 18:09):

Assuming this is true, IIUC, we have the following diamond problem:

import topology.algebra.valued_field

noncomputable theory

variables {K Γ₀ : Type*} [field K] [linear_ordered_comm_group_with_zero Γ₀] [hv : valued K Γ₀]

instance foo : valued (@uniform_space.completion K $ @valued.uniform_space _ _ _ _ hv) Γ₀ :=
valued.extension_valuation

example :
  uniform_space.completion.uniform_space K = @valued.uniform_space _ _ _ _ (@foo _ _ _ _ hv) :=
rfl -- Fails!

Oliver Nash (Apr 21 2022 at 18:10):

And now assuming I've got that right, does this mean that we should require a valuation to carry a bundled uniform_space structure (+ proof that it is the one induced by the valuation) so that we can solve this diamond?

Oliver Nash (Apr 21 2022 at 18:11):

This came up in #13462 cc @María Inés de Frutos Fernández

Johan Commelin (Apr 21 2022 at 18:20):

That sounds like it is a reasonable solution.

Johan Commelin (Apr 21 2022 at 18:21):

@Patrick Massot Do you remember if we thought about this issue during the perfectoid project?

Riccardo Brasca (Apr 21 2022 at 18:28):

Mathematically I think everything is OK, the two metrics are the same (if we use the same norm for the uniformizer).

Adam Topaz (Apr 21 2022 at 19:11):

I would vote against bundling a uniform space structure with a valuation.
There is this notion of a V-topology which is quite important in valuation theory (not to be confused with "the" v-topology, which is a Grothendieck topology). One of the classical results in valuation theory is that a V-topology always arises from a valuation or an absolute value, and two valuations are dependent if and only if they induce the same V-topology.

Adam Topaz (Apr 21 2022 at 19:12):

Stating such results would be quite annoying if the topology was bundled with the valuation.

Adam Topaz (Apr 21 2022 at 19:22):

On the other hand, maybe the class valued_field (or valued_ring) could indeed be bundled with a uniform space structure?

Patrick Massot (Apr 21 2022 at 21:03):

Could you ask me the same question in two days? I'm chairing a hiring committee tomorrow and I really can't do math (or Lean) now.

Oliver Nash (Apr 22 2022 at 07:45):

Thanks @Adam Topaz I agree; it is valued rather than valuation that should carry the bundled uniform_space structure. I'll try to get to this later today.

Anne Baanen (Apr 22 2022 at 09:51):

(For the record, this pattern of bundling equal-but-not-defeq instances is called forgetful inheritance)

Oliver Nash (Apr 25 2022 at 11:51):

I'm going to see if I can produce a PR (probably draft) solving the diamond problem here this afternoon based on changing the definition of valued to:

class valued (R : Type u) [ring R] (Γ₀ : out_param (Type v))
  [linear_ordered_comm_group_with_zero Γ₀] extends uniform_space R :=
(v : valuation R Γ₀)
(is_uniform_valuation :  s, s  𝓤 R   (γ : Γ₀ˣ), { p : R × R | v (p.2 - p.1) < γ }  s)

Oliver Nash (Apr 25 2022 at 17:00):

Still WIP but hopefully going in the right direction: #13691

Oliver Nash (Apr 26 2022 at 17:09):

I spent most of the day on #13691 (again) but I think I should finish tomorrow. Mathematically there are now just two sorries, both of which seem to be elementary results in Bourbaki.

Oliver Nash (Apr 26 2022 at 17:11):

Maybe I'll get lucky and someone will fill them in for me. Here's one of them:

import topology.algebra.group_completion

open_locale topological_space
open uniform_space

-- Bourbaki GT III §3 no.4 Proposition 7 [I hope]
lemma filter.has_basis.completion_nhds_zero {G ι : Type*}
  [add_group G] [uniform_space G] [uniform_add_group G] [separated_space G] -- `separated_space` really necessary?
  {s : ι  set G} {p : ι  Prop}
  (h : (𝓝 (0 : G)).has_basis p s) :
  (𝓝 (0 : completion G)).has_basis p $ λ i, closure $ coe '' (s i) :=
sorry

Oliver Nash (Apr 27 2022 at 15:53):

I think #13691 is ready for review now. Any comments welcome, especially from @Patrick Massot @Adam Topaz @María Inés de Frutos Fernández

Oliver Nash (Apr 27 2022 at 15:54):

Incidentally the Bourbaki lemma above is true with much weaker hypotheses:

import topology.algebra.group_completion

open_locale topological_space
open set uniform_space

lemma filter.has_basis.has_basis_of_dense_inducing' {α β : Type*}
  [topological_space α] [topological_space β] [regular_space β]
  {ι : Type*} {s : ι  set α} {p : ι  Prop} {x : α} (h : (𝓝 x).has_basis p s)
  {f : α  β} (hf : dense_inducing f) :
  (𝓝 (f x)).has_basis p $ λ i, closure $ f '' (s i) :=
begin
  rw filter.has_basis_iff at h ,
  intros T,
  refine λ hT, _, λ hT, _⟩,
  { obtain T', hT₁, hT₂, hT₃ := nhds_is_closed hT,
    have hT₄ : f⁻¹' T'  𝓝 x,
    { rw hf.to_inducing.nhds_eq_comap x,
      exact T', hT₁, subset.rfl⟩, },
    obtain i, hi, hi' := (h _).mp hT₄,
    exact i, hi, (closure_mono (image_subset f hi')).trans (subset.trans (closure_minimal
      (image_subset_iff.mpr subset.rfl) hT₃) hT₂)⟩, },
  { obtain i, hi, hi' := hT,
    suffices : closure (f '' s i)  𝓝 (f x), { filter_upwards [this] using hi', },
    replace h := (h (s i)).mpr i, hi, subset.rfl⟩,
    exact hf.closure_image_mem_nhds h, },
end

-- Bourbaki GT III §3 no.4 Proposition 7
example {G ι : Type*} [has_zero G] [uniform_space G]
  {s : ι  set G} {p : ι  Prop}
  (h : (𝓝 (0 : G)).has_basis p s) :
  (𝓝 (0 : completion G)).has_basis p $ λ i, closure $ coe '' (s i) :=
h.has_basis_of_dense_inducing' completion.dense_inducing_coe

Last updated: Dec 20 2023 at 11:08 UTC