Completable top field

Stream: maths

[Xavier Roblot]

I would like to prove that the completion at an infinite place of a number field is a field. The way to do that is to use docs#uniform_space.completion.field with a completable_top_field. There are few results about completable_top_field in mathlib but my hope is that one should able to prove that subfields of ℂ are completable_top_field which is all that I need. Is this a true assertion? And, if yes, what would be the strategy to prove that?

[Patrick Massot]

Yes, this is true. In order to prove it you need a more precise statement. If what you want is really that a subfield of $\mathbb{C}$ is completable then it should be very easy. I'll do that soon if nobody is faster (and if I don't forget).

[Patrick Massot]

I quickly did it without carefully checking the existing library (it is rather suspicious that I couldn't find the first two pieces):

import field_theory.subfield
import topology.algebra.uniform_field

open filter
open_locale uniformity

instance subtype.separated_space (α : Type*) [uniform_space α] [separated_space α] (s : set α) : separated_space s :=
separated_iff_t2.mpr t2_5_space.t2_space

lemma uniform_inducing.cauchy_map_iff {α β : Type*} [uniform_space α] [uniform_space β]
  {f : α → β} (hf : uniform_inducing f) {F : filter α} : cauchy (map f F) ↔ cauchy F :=
by simp only [cauchy, map_ne_bot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]

variables (L : Type*) [field L]  [uniform_space L] [completable_top_field L]

instance subfield.completable_top_field (K : subfield L) : completable_top_field K :=
{ nice := begin
    intros F F_cau inf_F,
    let i : K → L := coe,
    have hi : uniform_inducing i, from uniform_embedding_subtype_coe.to_uniform_inducing,
    rw ← hi.cauchy_map_iff at F_cau ⊢,
    rw [map_comm (show (i ∘ λ x, x⁻¹) = (λ x, x⁻¹) ∘ i, by {ext , refl })],
    apply completable_top_field.nice _ F_cau,
    rw [← filter.push_pull', show (0 : L) = i 0, from rfl, ← hi.inducing.nhds_eq_comap, inf_F,
        filter.map_bot]
  end,
  ..subtype.separated_space L K }

[Xavier Roblot]

Thanks! That's great but, if I am not confused, it requires the fact that ℂ is a completable_top_field, or I guess more generally, that a complete field is a completable_top_field and that seems to be missing too...

[Patrick Massot]

Sorry about that, I read your message too quickly and didn't notice we were also missing that. The thing is this completable field type class is really meant to construct the field structure on the completion and nothing else. Morally in your case you don't really want to consider an abstract completion but simply the closure of your number field in $\mathbb{C}$. But proving these things is a good sanity check anyway. So here is your proof:

open_locale topological_space

instance completable_top_field_of_complete (L : Type*) [field L]
  [uniform_space L] [topological_division_ring L] [separated_space L] [complete_space L] :
  completable_top_field L :=
{ nice := λ F cau_F hF, begin
    haveI : ne_bot F := cau_F.1,
    rcases complete_space.complete cau_F with ⟨x, hx⟩,
    have hx' : x ≠ 0,
    { rintro rfl,
      rw inf_eq_right.mpr hx at hF,
      exact cau_F.1.ne hF },
    exact filter.tendsto.cauchy_map (calc map (λ x, x⁻¹) F ≤ map (λ x, x⁻¹) (𝓝 x) : map_mono hx
                                                       ... ≤ 𝓝 (x⁻¹) : continuous_at_inv₀ hx')
  end,
  ..‹separated_space L›}

(with the same imports and openings as in my previous message).

[Xavier Roblot]

Thanks a lot! Do you have plans to PR those results?

[Patrick Massot]

I don't have plans but I can do it tonight if you need them. You can also do it if you prefer. The main work is to make sure the first two items in my first message are indeed missing (and to put them in a relevant location).

[Xavier Roblot]

Well, I would prefer if you PR these results but if you don't have time, I'll do it.

[Patrick Massot]

I opened #16805