feat(topology/algebra): topological fields (#8316)

Including the completion of completeable topological fields.
From the perfectoid spaces project.

src/order/filter/basic.lean

@@ -1545,6 +1545,29 @@ le_antisymm
   (assume c ⟨b, ⟨a, ha, (h₁ : preimage n a ⊆ b)⟩, (h₂ : preimage m b ⊆ c)⟩,
     ⟨a, ha, show preimage m (preimage n a) ⊆ c, from subset.trans (preimage_mono h₁) h₂⟩)
 
+section comm
+variables  {δ : Type*}
+
+/-!
+The variables in the following lemmas are used as in this diagram:
+```
+    φ
+  α → β
+θ ↓   ↓ ψ
+  γ → δ
+    ρ
+```
+-/
+variables {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ} (H : ψ ∘ φ = ρ ∘ θ)
+include H
+
+lemma map_comm (F : filter α) : map ψ (map φ F) = map ρ (map θ F) :=
+by rw [filter.map_map, H, ← filter.map_map]
+
+lemma comap_comm (G : filter δ) : comap φ (comap ψ G) = comap θ (comap ρ G) :=
+by rw [filter.comap_comap, H, ← filter.comap_comap]
+end comm
+
 @[simp] theorem comap_principal {t : set β} : comap m (𝓟 t) = 𝓟 (m ⁻¹' t) :=
 filter_eq $ set.ext $ assume s,
   ⟨assume ⟨u, (hu : t ⊆ u), (b : preimage m u ⊆ s)⟩, subset.trans (preimage_mono hu) b,

src/topology/algebra/field.lean

@@ -1,18 +1,121 @@
 /-
-Copyright (c) 2021 Scott Morrison. All rights reserved.
+Copyright (c) 2021 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Patrick Massot, Scott Morrison
 -/
 import topology.algebra.ring
 import topology.algebra.group_with_zero
 
 /-!
-A topological field is usually described via
-`{𝕜 : Type*} [field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] [has_continuous_inv 𝕜]`.
+# Topological fields
+
+A topological division ring is a topological ring whose inversion function is continuous at every
+non-zero element.
 
-The only construction in this file doesn't need to assume `[has_continuous_inv 𝕜]`.
 -/
 
+
+namespace topological_ring
+open topological_space function
+variables (R : Type*) [ring R]
+
+variables  [topological_space R]
+
+/-- The induced topology on units of a topological ring.
+This is not a global instance since other topologies could be relevant. Instead there is a class
+`induced_units` asserting that something equivalent to this construction holds. -/
+def topological_space_units : topological_space (units R) := induced (coe : units R → R) ‹_›
+
+/-- Asserts the topology on units is the induced topology.
+
+ Note: this is not always the correct topology.
+ Another good candidate is the subspace topology of $R \times R$,
+ with the units embedded via $u \mapsto (u, u^{-1})$.
+ These topologies are not (propositionally) equal in general. -/
+class induced_units [t : topological_space $ units R] : Prop :=
+(top_eq : t = induced (coe : units R → R) ‹_›)
+
+variables [topological_space $ units R]
+
+lemma units_topology_eq [induced_units R] :
+  ‹topological_space (units R)› = induced (coe : units R → R) ‹_› :=
+induced_units.top_eq
+
+lemma induced_units.continuous_coe [induced_units R] : continuous (coe : units R → R) :=
+(units_topology_eq R).symm ▸ continuous_induced_dom
+
+lemma units_embedding [induced_units R] :
+  embedding (coe : units R → R) :=
+{ induced := units_topology_eq R,
+  inj := λ x y h, units.ext h }
+
+instance top_monoid_units [topological_ring R] [induced_units R] :
+  has_continuous_mul (units R) :=
+⟨begin
+  let mulR := (λ (p : R × R), p.1*p.2),
+  let mulRx := (λ (p : units R × units R), p.1*p.2),
+  have key : coe ∘ mulRx = mulR ∘ (λ p, (p.1.val, p.2.val)), from rfl,
+  rw [continuous_iff_le_induced, units_topology_eq R, prod_induced_induced,
+      induced_compose, key, ← induced_compose],
+  apply induced_mono,
+  rw ← continuous_iff_le_induced,
+  exact continuous_mul,
+end⟩
+end topological_ring
+
+variables (K : Type*) [division_ring K] [topological_space K]
+
+/-- A topological division ring is a division ring with a topology where all operations are
+    continuous, including inversion. -/
+class topological_division_ring extends topological_ring K : Prop :=
+(continuous_inv : ∀ x : K, x ≠ 0 → continuous_at (λ x : K, x⁻¹ : K → K) x)
+
+namespace topological_division_ring
+open filter set
+/-!
+In this section, we show that units of a topological division ring endowed with the
+induced topology form a topological group. These are not global instances because
+one could want another topology on units. To turn on this feature, use:
+
+```lean
+local attribute [instance]
+topological_ring.topological_space_units topological_division_ring.units_top_group
+```
+-/
+
+local attribute [instance] topological_ring.topological_space_units
+
+@[priority 100] instance induced_units : topological_ring.induced_units K := ⟨rfl⟩
+
+variables [topological_division_ring K]
+
+lemma units_top_group : topological_group (units K) :=
+{ continuous_inv := begin
+     have : (coe : units K → K) ∘ (λ x, x⁻¹ : units K → units K) =
+            (λ x, x⁻¹ : K → K) ∘ (coe : units K → K), from funext units.coe_inv',
+     rw continuous_iff_continuous_at,
+     intros x,
+     rw [continuous_at, nhds_induced, nhds_induced, tendsto_iff_comap, comap_comm this],
+     apply comap_mono,
+     rw [← tendsto_iff_comap, units.coe_inv'],
+     exact topological_division_ring.continuous_inv (x : K) x.ne_zero
+   end ,
+  ..topological_ring.top_monoid_units K}
+
+local attribute [instance] units_top_group
+
+lemma continuous_units_inv : continuous (λ x : units K, (↑(x⁻¹) : K)) :=
+(topological_ring.induced_units.continuous_coe K).comp topological_group.continuous_inv
+
+end topological_division_ring
+
+
+section affine_homeomorph
+/-!
+This section is about affine homeomorphisms from a topological field `𝕜` to itself.
+Technically it does not require `𝕜` to be a topological field, a topological ring that
+happens to be a field is enough.
+-/
 variables {𝕜 : Type*} [field 𝕜] [topological_space 𝕜] [topological_ring 𝕜]
 
 /--
@@ -24,3 +127,5 @@ def affine_homeomorph (a b : 𝕜) (h : a ≠ 0) : 𝕜 ≃ₜ 𝕜 :=
   inv_fun := λ y, (y - b) / a,
   left_inv := λ x, by { simp only [add_sub_cancel], exact mul_div_cancel_left x h, },
   right_inv := λ y, by { simp [mul_div_cancel' _ h], }, }
+
+end affine_homeomorph

src/topology/algebra/uniform_field.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2019 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot
+-/
+import topology.algebra.uniform_ring
+import topology.algebra.field
+
+/-!
+# Completion of topological fields
+
+The goal of this file is to prove the main part of Proposition 7 of Bourbaki GT III 6.8 :
+
+The completion `hat K` of a Hausdorff topological field is a field if the image under
+the mapping `x ↦ x⁻¹` of every Cauchy filter (with respect to the additive uniform structure)
+which does not have a cluster point at `0` is a Cauchy filter
+(with respect to the additive uniform structure).
+
+Bourbaki does not give any detail here, he refers to the general discussion of extending
+functions defined on a dense subset with values in a complete Hausdorff space. In particular
+the subtlety about clustering at zero is totally left to readers.
+
+Note that the separated completion of a non-separated topological field is the zero ring, hence
+the separation assumption is needed. Indeed the kernel of the completion map is the closure of
+zero which is an ideal. Hence it's either zero (and the field is separated) or the full field,
+which implies one is sent to zero and the completion ring is trivial.
+
+The main definition is `completable_top_field` which packages the assumptions as a Prop-valued
+type class and the main results are the instances `field_completion` and
+`topological_division_ring_completion`.
+-/
+
+
+noncomputable theory
+
+open_locale classical uniformity topological_space
+
+open set uniform_space uniform_space.completion filter
+
+variables (K : Type*) [field K]  [uniform_space K]
+
+local notation `hat` := completion
+
+@[priority 100]
+instance [separated_space K] : nontrivial (hat K) :=
+⟨⟨0, 1, λ h, zero_ne_one $ (uniform_embedding_coe K).inj h⟩⟩
+
+/--
+A topological field is completable if it is separated and the image under
+the mapping x ↦ x⁻¹ of every Cauchy filter (with respect to the additive uniform structure)
+which does not have a cluster point at 0 is a Cauchy filter
+(with respect to the additive uniform structure). This ensures the completion is
+a field.
+-/
+class completable_top_field extends separated_space K : Prop :=
+(nice : ∀ F : filter K, cauchy F → 𝓝 0 ⊓ F = ⊥ → cauchy (map (λ x, x⁻¹) F))
+
+variables {K}
+
+/-- extension of inversion to the completion of a field. -/
+def hat_inv : hat K → hat K := dense_inducing_coe.extend (λ x : K, (coe x⁻¹ : hat K))
+
+lemma continuous_hat_inv [completable_top_field K] {x : hat K} (h : x ≠ 0) :
+  continuous_at hat_inv x :=
+begin
+  haveI : regular_space (hat K) := completion.regular_space K,
+  refine dense_inducing_coe.continuous_at_extend _,
+  apply mem_sets_of_superset (compl_singleton_mem_nhds h),
+  intros y y_ne,
+  rw mem_compl_singleton_iff at y_ne,
+  apply complete_space.complete,
+  rw ← filter.map_map,
+  apply cauchy.map _ (completion.uniform_continuous_coe K),
+  apply completable_top_field.nice,
+  { haveI := dense_inducing_coe.comap_nhds_ne_bot y,
+    apply cauchy_nhds.comap,
+    { rw completion.comap_coe_eq_uniformity,
+      exact le_rfl } },
+  { have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥,
+    { by_contradiction h,
+      exact y_ne (eq_of_nhds_ne_bot $ ne_bot_iff.mpr h).symm },
+    erw [dense_inducing_coe.nhds_eq_comap (0 : K), ← comap_inf,  eq_bot],
+    exact comap_bot },
+end
+
+/-
+The value of `hat_inv` at zero is not really specified, although it's probably zero.
+Here we explicitly enforce the `inv_zero` axiom.
+-/
+instance completion.has_inv : has_inv (hat K) := ⟨λ x, if x = 0 then 0 else hat_inv x⟩
+
+variables [topological_division_ring K]
+
+lemma hat_inv_extends {x : K} (h : x ≠ 0) : hat_inv (x : hat K) = coe (x⁻¹ : K) :=
+dense_inducing_coe.extend_eq_at _
+    ((continuous_coe K).continuous_at.comp (topological_division_ring.continuous_inv x h))
+
+variables [completable_top_field K]
+
+@[norm_cast]
+lemma coe_inv (x : K) : (x : hat K)⁻¹ = ((x⁻¹ : K) : hat K) :=
+begin
+  by_cases h : x = 0,
+  { rw [h, inv_zero],
+    dsimp [has_inv.inv],
+    norm_cast,
+    simp [if_pos] },
+  { conv_lhs { dsimp [has_inv.inv] },
+    norm_cast,
+    rw if_neg,
+    { exact hat_inv_extends h },
+    { exact λ H, h (dense_embedding_coe.inj H) } }
+end
+
+variables [uniform_add_group K] [topological_ring K]
+
+lemma mul_hat_inv_cancel {x : hat K} (x_ne : x ≠ 0) : x*hat_inv x = 1 :=
+begin
+  haveI : t1_space (hat K) := t2_space.t1_space,
+  let f := λ x : hat K, x*hat_inv x,
+  let c := (coe : K → hat K),
+  change f x = 1,
+  have cont : continuous_at f x,
+  { letI : topological_space (hat K × hat K) := prod.topological_space,
+    have : continuous_at (λ y : hat K, ((y, hat_inv y) : hat K × hat K)) x,
+      from continuous_id.continuous_at.prod (continuous_hat_inv x_ne),
+    exact (_root_.continuous_mul.continuous_at.comp this : _) },
+  have clo : x ∈ closure (c '' {0}ᶜ),
+  { have := dense_inducing_coe.dense x,
+    rw [← image_univ, show (univ : set K) = {0} ∪ {0}ᶜ,
+                      from (union_compl_self _).symm, image_union] at this,
+    apply mem_closure_of_mem_closure_union this,
+    rw image_singleton,
+    exact compl_singleton_mem_nhds x_ne },
+  have fxclo : f x ∈ closure (f '' (c '' {0}ᶜ)) := mem_closure_image cont clo,
+  have : f '' (c '' {0}ᶜ) ⊆ {1},
+  { rw image_image,
+    rintros _ ⟨z, z_ne, rfl⟩,
+    rw mem_singleton_iff,
+    rw mem_compl_singleton_iff at z_ne,
+    dsimp [c, f],
+    rw hat_inv_extends z_ne,
+    norm_cast,
+    rw mul_inv_cancel z_ne,
+    norm_cast },
+  replace fxclo := closure_mono this fxclo,
+  rwa [closure_singleton, mem_singleton_iff] at fxclo
+end
+
+instance field_completion : field (hat K) :=
+{ exists_pair_ne := ⟨0, 1, λ h, zero_ne_one ((uniform_embedding_coe K).inj h)⟩,
+  mul_inv_cancel := λ x x_ne, by { dsimp [has_inv.inv],
+                                   simp [if_neg x_ne, mul_hat_inv_cancel x_ne], },
+  inv_zero := show ((0 : K) : hat K)⁻¹ = ((0 : K) : hat K), by rw [coe_inv, inv_zero],
+  ..completion.has_inv,
+  ..(by apply_instance : comm_ring (hat K)) }
+
+instance topological_division_ring_completion : topological_division_ring (hat K) :=
+{ continuous_inv := begin
+    intros x x_ne,
+    have : {y | hat_inv y = y⁻¹ } ∈ 𝓝 x,
+    { have : {(0 : hat K)}ᶜ ⊆ {y : hat K | hat_inv y = y⁻¹ },
+      { intros y y_ne,
+        rw mem_compl_singleton_iff at y_ne,
+        dsimp [has_inv.inv],
+        rw if_neg y_ne },
+      exact mem_sets_of_superset (compl_singleton_mem_nhds x_ne) this },
+    exact continuous_at.congr (continuous_hat_inv x_ne) this
+  end,
+  ..completion.top_ring_compl }

src/topology/basic.lean

@@ -902,6 +902,17 @@ end
 lemma closure_inter_open' {s t : set α} (h : is_open t) : closure s ∩ t ⊆ closure (s ∩ t) :=
 by simpa only [inter_comm] using closure_inter_open h
 
+lemma mem_closure_of_mem_closure_union {s₁ s₂ : set α} {x : α} (h : x ∈ closure (s₁ ∪ s₂))
+  (h₁ : s₁ᶜ ∈ 𝓝 x) : x ∈ closure s₂ :=
+begin
+  rw mem_closure_iff_nhds_ne_bot at *,
+  rwa ← calc
+    𝓝 x ⊓ principal (s₁ ∪ s₂) = 𝓝 x ⊓ (principal s₁ ⊔ principal s₂) : by rw sup_principal
+    ... = (𝓝 x ⊓ principal s₁) ⊔ (𝓝 x ⊓ principal s₂) : inf_sup_left
+    ... = ⊥ ⊔ 𝓝 x ⊓ principal s₂ : by rw inf_principal_eq_bot.mpr h₁
+    ... = 𝓝 x ⊓ principal s₂ : bot_sup_eq
+end
+
 /-- The intersection of an open dense set with a dense set is a dense set. -/
 lemma dense.inter_of_open_left {s t : set α} (hs : dense s) (ht : dense t) (hso : is_open s) :
   dense (s ∩ t) :=
@@ -1187,6 +1198,19 @@ lemma is_closed.preimage {f : α → β} (hf : continuous f) {s : set β} (h : i
   is_closed (f ⁻¹' s) :=
 continuous_iff_is_closed.mp hf s h
 
+lemma mem_closure_image {f : α → β} {x : α} {s : set α} (hf : continuous_at f x)
+  (hx : x ∈ closure s) : f x ∈ closure (f '' s) :=
+begin
+  rw [mem_closure_iff_nhds_ne_bot] at hx ⊢,
+  rw ← bot_lt_iff_ne_bot,
+  haveI : ne_bot _ := ⟨hx⟩,
+  calc
+    ⊥   < map f (𝓝 x ⊓ principal s) : bot_lt_iff_ne_bot.mpr ne_bot.ne'
+    ... ≤ (map f $ 𝓝 x) ⊓ (map f $ principal s) : map_inf_le
+    ... = (map f $ 𝓝 x) ⊓ (principal $ f '' s) : by rw map_principal
+    ... ≤ 𝓝 (f x) ⊓ (principal $ f '' s) : inf_le_inf hf le_rfl
+end
+
 lemma continuous_at_iff_ultrafilter {f : α → β} {x} : continuous_at f x ↔
   ∀ g : ultrafilter α, ↑g ≤ 𝓝 x → tendsto f g (𝓝 (f x)) :=
 tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))

src/topology/constructions.lean

@@ -287,6 +287,21 @@ begin
   simp only [and_assoc, and.left_comm]
 end
 
+/-- A product of induced topologies is induced by the product map -/
+lemma prod_induced_induced {α γ : Type*} (f : α → β) (g : γ → δ) :
+  @prod.topological_space α γ (induced f ‹_›) (induced g ‹_›) =
+  induced (λ p, (f p.1, g p.2)) prod.topological_space :=
+begin
+  set fxg := (λ p : α × γ, (f p.1, g p.2)),
+  have key1 : f ∘ (prod.fst : α × γ → α) = (prod.fst : β × δ → β) ∘ fxg, from rfl,
+  have key2 : g ∘ (prod.snd : α × γ → γ) = (prod.snd : β × δ → δ) ∘ fxg, from rfl,
+  unfold prod.topological_space,
+  conv_lhs {
+    rw [induced_compose, induced_compose, key1, key2],
+    congr, rw ← induced_compose, skip, rw ← induced_compose, },
+  rw induced_inf
+end
+
 lemma continuous_uncurry_of_discrete_topology_left [discrete_topology α]
   {f : α → β → γ} (h : ∀ a, continuous (f a)) : continuous (function.uncurry f) :=
 continuous_iff_continuous_at.2 $ λ ⟨a, b⟩,