Extension of valuation to completion creates diamond?

Stream: general

[Oliver Nash]

Given a valued field $K$, there seem to be two ways to obtain a uniform space structure on its completion $\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 $\hat K$.

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

[Oliver Nash]

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]

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]

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

[Johan Commelin]

That sounds like it is a reasonable solution.

[Johan Commelin]

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

[Riccardo Brasca]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Patrick Massot]

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]

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]

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

[Oliver Nash]

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]

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

[Oliver Nash]

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]

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]

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]

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