From 18936e552fbb42e4599fededbd126cadaad12866 Mon Sep 17 00:00:00 2001 From: Anatole Dedecker Date: Fri, 10 Jun 2022 14:50:29 +0000 Subject: [PATCH] feat(topology/uniform_space/equiv): define uniform isomorphisms (#14537) This adds a new file, mostly copy-pasted from `topology/homeomorph`, to analogously define uniform isomorphisms --- src/data/prod/basic.lean | 5 +- src/topology/uniform_space/basic.lean | 4 + src/topology/uniform_space/equiv.lean | 269 ++++++++++++++++++ .../uniform_space/uniform_embedding.lean | 12 + 4 files changed, 289 insertions(+), 1 deletion(-) create mode 100644 src/topology/uniform_space/equiv.lean diff --git a/src/data/prod/basic.lean b/src/data/prod/basic.lean index 9ccfa0badfa8f..12205a9c38353 100644 --- a/src/data/prod/basic.lean +++ b/src/data/prod/basic.lean @@ -84,9 +84,12 @@ ext_iff.2 ⟨h₁, h₂⟩ lemma map_def {f : α → γ} {g : β → δ} : prod.map f g = λ (p : α × β), (f p.1, g p.2) := funext (λ p, ext (map_fst f g p) (map_snd f g p)) -lemma id_prod : (λ (p : α × α), (p.1, p.2)) = id := +lemma id_prod : (λ (p : α × β), (p.1, p.2)) = id := funext $ λ ⟨a, b⟩, rfl +lemma map_id : (prod.map (@id α) (@id β)) = id := +id_prod + lemma fst_surjective [h : nonempty β] : function.surjective (@fst α β) := λ x, h.elim $ λ y, ⟨⟨x, y⟩, rfl⟩ diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean index 749834476683d..05469d00668ae 100644 --- a/src/topology/uniform_space/basic.lean +++ b/src/topology/uniform_space/basic.lean @@ -1215,6 +1215,10 @@ lemma uniform_continuous_subtype_val {p : α → Prop} [uniform_space α] : uniform_continuous (subtype.val : {a : α // p a} → α) := uniform_continuous_comap +lemma uniform_continuous_subtype_coe {p : α → Prop} [uniform_space α] : + uniform_continuous (coe : {a : α // p a} → α) := +uniform_continuous_subtype_val + lemma uniform_continuous_subtype_mk {p : α → Prop} [uniform_space α] [uniform_space β] {f : β → α} (hf : uniform_continuous f) (h : ∀x, p (f x)) : uniform_continuous (λx, ⟨f x, h x⟩ : β → subtype p) := diff --git a/src/topology/uniform_space/equiv.lean b/src/topology/uniform_space/equiv.lean new file mode 100644 index 0000000000000..9ebf5a9481b64 --- /dev/null +++ b/src/topology/uniform_space/equiv.lean @@ -0,0 +1,269 @@ +/- +Copyright (c) 2022 Anatole Dedecker. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johannes Hölzl, Patrick Massot, Sébastien Gouëzel, Zhouhang Zhou, Reid Barton, +Anatole Dedecker +-/ +import topology.homeomorph +import topology.uniform_space.uniform_embedding +import topology.uniform_space.pi + +/-! +# Uniform isomorphisms + +This file defines uniform isomorphisms between two uniform spaces. They are bijections with both +directions uniformly continuous. We denote uniform isomorphisms with the notation `≃ᵤ`. + +# Main definitions + +* `uniform_equiv α β`: The type of uniform isomorphisms from `α` to `β`. + This type can be denoted using the following notation: `α ≃ᵤ β`. + +-/ + +open set filter +open_locale + +variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} + +/-- Uniform isomorphism between `α` and `β` -/ +@[nolint has_inhabited_instance] -- not all spaces are homeomorphic to each other +structure uniform_equiv (α : Type*) (β : Type*) [uniform_space α] [uniform_space β] + extends α ≃ β := +(uniform_continuous_to_fun : uniform_continuous to_fun) +(uniform_continuous_inv_fun : uniform_continuous inv_fun) + +infix ` ≃ᵤ `:25 := uniform_equiv + +namespace uniform_equiv +variables [uniform_space α] [uniform_space β] [uniform_space γ] [uniform_space δ] + +instance : has_coe_to_fun (α ≃ᵤ β) (λ _, α → β) := ⟨λe, e.to_equiv⟩ + +@[simp] lemma uniform_equiv_mk_coe (a : equiv α β) (b c) : + ((uniform_equiv.mk a b c) : α → β) = a := +rfl + +/-- Inverse of a uniform isomorphism. -/ +protected def symm (h : α ≃ᵤ β) : β ≃ᵤ α := +{ uniform_continuous_to_fun := h.uniform_continuous_inv_fun, + uniform_continuous_inv_fun := h.uniform_continuous_to_fun, + to_equiv := h.to_equiv.symm } + +/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case, + because it is a composition of multiple projections. -/ +def simps.apply (h : α ≃ᵤ β) : α → β := h +/-- See Note [custom simps projection] -/ +def simps.symm_apply (h : α ≃ᵤ β) : β → α := h.symm + +initialize_simps_projections uniform_equiv + (to_equiv_to_fun → apply, to_equiv_inv_fun → symm_apply, -to_equiv) + +@[simp] lemma coe_to_equiv (h : α ≃ᵤ β) : ⇑h.to_equiv = h := rfl +@[simp] lemma coe_symm_to_equiv (h : α ≃ᵤ β) : ⇑h.to_equiv.symm = h.symm := rfl + +lemma to_equiv_injective : function.injective (to_equiv : α ≃ᵤ β → α ≃ β) +| ⟨e, h₁, h₂⟩ ⟨e', h₁', h₂'⟩ rfl := rfl + +@[ext] lemma ext {h h' : α ≃ᵤ β} (H : ∀ x, h x = h' x) : h = h' := +to_equiv_injective $ equiv.ext H + +/-- Identity map as a uniform isomorphism. -/ +@[simps apply {fully_applied := ff}] +protected def refl (α : Type*) [uniform_space α] : α ≃ᵤ α := +{ uniform_continuous_to_fun := uniform_continuous_id, + uniform_continuous_inv_fun := uniform_continuous_id, + to_equiv := equiv.refl α } + +/-- Composition of two uniform isomorphisms. -/ +protected def trans (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) : α ≃ᵤ γ := +{ uniform_continuous_to_fun := h₂.uniform_continuous_to_fun.comp h₁.uniform_continuous_to_fun, + uniform_continuous_inv_fun := h₁.uniform_continuous_inv_fun.comp h₂.uniform_continuous_inv_fun, + to_equiv := equiv.trans h₁.to_equiv h₂.to_equiv } + +@[simp] lemma trans_apply (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α) : h₁.trans h₂ a = h₂ (h₁ a) := rfl + +@[simp] lemma uniform_equiv_mk_coe_symm (a : equiv α β) (b c) : + ((uniform_equiv.mk a b c).symm : β → α) = a.symm := +rfl + +@[simp] lemma refl_symm : (uniform_equiv.refl α).symm = uniform_equiv.refl α := rfl + +protected lemma uniform_continuous (h : α ≃ᵤ β) : uniform_continuous h := +h.uniform_continuous_to_fun + +@[continuity] +protected lemma continuous (h : α ≃ᵤ β) : continuous h := +h.uniform_continuous.continuous + +protected lemma uniform_continuous_symm (h : α ≃ᵤ β) : uniform_continuous (h.symm) := +h.uniform_continuous_inv_fun + +@[continuity] -- otherwise `by continuity` can't prove continuity of `h.to_equiv.symm` +protected lemma continuous_symm (h : α ≃ᵤ β) : continuous (h.symm) := +h.uniform_continuous_symm.continuous + +/-- A uniform isomorphism as a homeomorphism. -/ +@[simps] +protected def to_homeomorph (e : α ≃ᵤ β) : α ≃ₜ β := +{ continuous_to_fun := e.continuous, + continuous_inv_fun := e.continuous_symm, + .. e.to_equiv } + +@[simp] lemma apply_symm_apply (h : α ≃ᵤ β) (x : β) : h (h.symm x) = x := +h.to_equiv.apply_symm_apply x + +@[simp] lemma symm_apply_apply (h : α ≃ᵤ β) (x : α) : h.symm (h x) = x := +h.to_equiv.symm_apply_apply x + +protected lemma bijective (h : α ≃ᵤ β) : function.bijective h := h.to_equiv.bijective +protected lemma injective (h : α ≃ᵤ β) : function.injective h := h.to_equiv.injective +protected lemma surjective (h : α ≃ᵤ β) : function.surjective h := h.to_equiv.surjective + +/-- Change the uniform equiv `f` to make the inverse function definitionally equal to `g`. -/ +def change_inv (f : α ≃ᵤ β) (g : β → α) (hg : function.right_inverse g f) : α ≃ᵤ β := +have g = f.symm, from funext (λ x, calc g x = f.symm (f (g x)) : (f.left_inv (g x)).symm + ... = f.symm x : by rw hg x), +{ to_fun := f, + inv_fun := g, + left_inv := by convert f.left_inv, + right_inv := by convert f.right_inv, + uniform_continuous_to_fun := f.uniform_continuous, + uniform_continuous_inv_fun := by convert f.symm.uniform_continuous } + +@[simp] lemma symm_comp_self (h : α ≃ᵤ β) : ⇑h.symm ∘ ⇑h = id := +funext h.symm_apply_apply + +@[simp] lemma self_comp_symm (h : α ≃ᵤ β) : ⇑h ∘ ⇑h.symm = id := +funext h.apply_symm_apply + +@[simp] lemma range_coe (h : α ≃ᵤ β) : range h = univ := +h.surjective.range_eq + +lemma image_symm (h : α ≃ᵤ β) : image h.symm = preimage h := +funext h.symm.to_equiv.image_eq_preimage + +lemma preimage_symm (h : α ≃ᵤ β) : preimage h.symm = image h := +(funext h.to_equiv.image_eq_preimage).symm + +@[simp] lemma image_preimage (h : α ≃ᵤ β) (s : set β) : h '' (h ⁻¹' s) = s := +h.to_equiv.image_preimage s + +@[simp] lemma preimage_image (h : α ≃ᵤ β) (s : set α) : h ⁻¹' (h '' s) = s := +h.to_equiv.preimage_image s + +protected lemma uniform_inducing (h : α ≃ᵤ β) : uniform_inducing h := +uniform_inducing_of_compose h.uniform_continuous h.symm.uniform_continuous $ + by simp only [symm_comp_self, uniform_inducing_id] + +lemma comap_eq (h : α ≃ᵤ β) : uniform_space.comap h ‹_› = ‹_› := +by ext : 1; exact h.uniform_inducing.comap_uniformity + +protected lemma uniform_embedding (h : α ≃ᵤ β) : uniform_embedding h := +⟨h.uniform_inducing, h.injective⟩ + +/-- Uniform equiv given a uniform embedding. -/ +noncomputable def of_uniform_embedding (f : α → β) (hf : uniform_embedding f) : + α ≃ᵤ (set.range f) := +{ uniform_continuous_to_fun := uniform_continuous_subtype_mk + hf.to_uniform_inducing.uniform_continuous _, + uniform_continuous_inv_fun := + by simp [hf.to_uniform_inducing.uniform_continuous_iff, uniform_continuous_subtype_coe], + to_equiv := equiv.of_injective f hf.inj } + +/-- If two sets are equal, then they are uniformly equivalent. -/ +def set_congr {s t : set α} (h : s = t) : s ≃ᵤ t := +{ uniform_continuous_to_fun := uniform_continuous_subtype_mk uniform_continuous_subtype_val _, + uniform_continuous_inv_fun := uniform_continuous_subtype_mk uniform_continuous_subtype_val _, + to_equiv := equiv.set_congr h } + +/-- Product of two uniform isomorphisms. -/ +def prod_congr (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : α × γ ≃ᵤ β × δ := +{ uniform_continuous_to_fun := (h₁.uniform_continuous.comp uniform_continuous_fst).prod_mk + (h₂.uniform_continuous.comp uniform_continuous_snd), + uniform_continuous_inv_fun := (h₁.symm.uniform_continuous.comp uniform_continuous_fst).prod_mk + (h₂.symm.uniform_continuous.comp uniform_continuous_snd), + to_equiv := h₁.to_equiv.prod_congr h₂.to_equiv } + +@[simp] lemma prod_congr_symm (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : + (h₁.prod_congr h₂).symm = h₁.symm.prod_congr h₂.symm := rfl + +@[simp] lemma coe_prod_congr (h₁ : α ≃ᵤ β) (h₂ : γ ≃ᵤ δ) : + ⇑(h₁.prod_congr h₂) = prod.map h₁ h₂ := rfl + +section +variables (α β γ) + +/-- `α × β` is uniformly isomorphic to `β × α`. -/ +def prod_comm : α × β ≃ᵤ β × α := +{ uniform_continuous_to_fun := uniform_continuous_snd.prod_mk uniform_continuous_fst, + uniform_continuous_inv_fun := uniform_continuous_snd.prod_mk uniform_continuous_fst, + to_equiv := equiv.prod_comm α β } + +@[simp] lemma prod_comm_symm : (prod_comm α β).symm = prod_comm β α := rfl +@[simp] lemma coe_prod_comm : ⇑(prod_comm α β) = prod.swap := rfl + +/-- `(α × β) × γ` is uniformly isomorphic to `α × (β × γ)`. -/ +def prod_assoc : (α × β) × γ ≃ᵤ α × (β × γ) := +{ uniform_continuous_to_fun := (uniform_continuous_fst.comp uniform_continuous_fst).prod_mk + ((uniform_continuous_snd.comp uniform_continuous_fst).prod_mk uniform_continuous_snd), + uniform_continuous_inv_fun := (uniform_continuous_fst.prod_mk + (uniform_continuous_fst.comp uniform_continuous_snd)).prod_mk + (uniform_continuous_snd.comp uniform_continuous_snd), + to_equiv := equiv.prod_assoc α β γ } + +/-- `α × {*}` is uniformly isomorphic to `α`. -/ +@[simps apply {fully_applied := ff}] +def prod_punit : α × punit ≃ᵤ α := +{ to_equiv := equiv.prod_punit α, + uniform_continuous_to_fun := uniform_continuous_fst, + uniform_continuous_inv_fun := uniform_continuous_id.prod_mk uniform_continuous_const } + +/-- `{*} × α` is uniformly isomorphic to `α`. -/ +def punit_prod : punit × α ≃ᵤ α := +(prod_comm _ _).trans (prod_punit _) + +@[simp] lemma coe_punit_prod : ⇑(punit_prod α) = prod.snd := rfl + +end + +/-- If `ι` has a unique element, then `ι → α` is homeomorphic to `α`. -/ +@[simps { fully_applied := ff }] +def fun_unique (ι α : Type*) [unique ι] [uniform_space α] : (ι → α) ≃ᵤ α := +{ to_equiv := equiv.fun_unique ι α, + uniform_continuous_to_fun := Pi.uniform_continuous_proj _ _, + uniform_continuous_inv_fun := uniform_continuous_pi.mpr (λ _, uniform_continuous_id) } + +/-- Uniform isomorphism between dependent functions `Π i : fin 2, α i` and `α 0 × α 1`. -/ +@[simps { fully_applied := ff }] +def {u} pi_fin_two (α : fin 2 → Type u) [Π i, uniform_space (α i)] : (Π i, α i) ≃ᵤ α 0 × α 1 := +{ to_equiv := pi_fin_two_equiv α, + uniform_continuous_to_fun := + (Pi.uniform_continuous_proj _ 0).prod_mk (Pi.uniform_continuous_proj _ 1), + uniform_continuous_inv_fun := uniform_continuous_pi.mpr $ + fin.forall_fin_two.2 ⟨uniform_continuous_fst, uniform_continuous_snd⟩ } + +/-- Uniform isomorphism between `α² = fin 2 → α` and `α × α`. -/ +@[simps { fully_applied := ff }] def fin_two_arrow : (fin 2 → α) ≃ᵤ α × α := +{ to_equiv := fin_two_arrow_equiv α, .. pi_fin_two (λ _, α) } + +/-- +A subset of a uniform space is uniformly isomorphic to its image under a uniform isomorphism. +-/ +def image (e : α ≃ᵤ β) (s : set α) : s ≃ᵤ e '' s := +{ uniform_continuous_to_fun := uniform_continuous_subtype_mk + (e.uniform_continuous.comp uniform_continuous_subtype_val) (λ x, mem_image_of_mem _ x.2), + uniform_continuous_inv_fun := uniform_continuous_subtype_mk + (e.symm.uniform_continuous.comp uniform_continuous_subtype_val) + (λ x, by simpa using mem_image_of_mem e.symm x.2), + to_equiv := e.to_equiv.image s } + +end uniform_equiv + +/-- A uniform inducing equiv between uniform spaces is a uniform isomorphism. -/ +@[simps] def equiv.to_uniform_equiv_of_uniform_inducing [uniform_space α] [uniform_space β] + (f : α ≃ β) (hf : uniform_inducing f) : + α ≃ᵤ β := +{ uniform_continuous_to_fun := hf.uniform_continuous, + uniform_continuous_inv_fun := hf.uniform_continuous_iff.2 $ by simpa using uniform_continuous_id, + .. f } diff --git a/src/topology/uniform_space/uniform_embedding.lean b/src/topology/uniform_space/uniform_embedding.lean index e16c550d076db..02fe5f8840471 100644 --- a/src/topology/uniform_space/uniform_embedding.lean +++ b/src/topology/uniform_space/uniform_embedding.lean @@ -31,6 +31,9 @@ lemma uniform_inducing.mk' {f : α → β} (h : ∀ s, s ∈ 𝓤 α ↔ ∃ t ∈ 𝓤 β, ∀ x y : α, (f x, f y) ∈ t → (x, y) ∈ s) : uniform_inducing f := ⟨by simp [eq_comm, filter.ext_iff, subset_def, h]⟩ +lemma uniform_inducing_id : uniform_inducing (@id α) := +⟨by rw [← prod.map_def, prod.map_id, comap_id]⟩ + lemma uniform_inducing.comp {g : β → γ} (hg : uniform_inducing g) {f : α → β} (hf : uniform_inducing f) : uniform_inducing (g ∘ f) := ⟨ by rw [show (λ (x : α × α), ((g ∘ f) x.1, (g ∘ f) x.2)) = @@ -42,6 +45,15 @@ lemma uniform_inducing.basis_uniformity {f : α → β} (hf : uniform_inducing f (𝓤 α).has_basis p (λ i, prod.map f f ⁻¹' s i) := hf.1 ▸ H.comap _ +lemma uniform_inducing_of_compose {f : α → β} {g : β → γ} (hf : uniform_continuous f) + (hg : uniform_continuous g) (hgf : uniform_inducing (g ∘ f)) : uniform_inducing f := +begin + refine ⟨le_antisymm _ hf.le_comap⟩, + rw [← hgf.1, ← prod.map_def, ← prod.map_def, ← prod.map_comp_map f f g g, + ← @comap_comap _ _ _ _ (prod.map f f)], + exact comap_mono hg.le_comap +end + /-- A map `f : α → β` between uniform spaces is a *uniform embedding* if it is uniform inducing and injective. If `α` is a separated space, then the latter assumption follows from the former. -/ structure uniform_embedding (f : α → β) extends uniform_inducing f : Prop :=