refactor(src/analysis/normed_space/linear_isometry): generalize to se…

…mi_normed_group (#7122)

This is part of a series of PR to include the theory of seminormed things in mathlib.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/normed_space/linear_isometry.lean

@@ -13,23 +13,28 @@ embedding of `E` into `F` and `linear_isometry_equiv` (notation: `E ≃ₗᵢ[R]
 isometric equivalence between `E` and `F`.
 
 We also prove some trivial lemmas and provide convenience constructors.
+
+Since a lot of elementary properties don't require `∥x∥ = 0 → x = 0` we start setting up the
+theory for `semi_normed_space` and we specialize to `normed_space` when needed.
 -/
 open function set
 
-variables {R E F G G' : Type*} [semiring R]
-  [normed_group E] [normed_group F] [normed_group G] [normed_group G']
+variables {R E F G G' E₁ : Type*} [semiring R]
+  [semi_normed_group E] [semi_normed_group F] [semi_normed_group G] [semi_normed_group G']
   [semimodule R E] [semimodule R F] [semimodule R G] [semimodule R G']
+  [normed_group E₁] [semimodule R E₁]
 
 /-- An `R`-linear isometric embedding of one normed `R`-module into another. -/
-structure linear_isometry (R E F : Type*) [semiring R] [normed_group E] [normed_group F]
-  [semimodule R E] [semimodule R F] extends E →ₗ[R] F :=
+structure linear_isometry (R E F : Type*) [semiring R] [semi_normed_group E]
+  [semi_normed_group F] [semimodule R E] [semimodule R F] extends E →ₗ[R] F :=
 (norm_map' : ∀ x, ∥to_linear_map x∥ = ∥x∥)
 
 notation E ` →ₗᵢ[`:25 R:25 `] `:0 F:0 := linear_isometry R E F
 
 namespace linear_isometry
 
-variables (f : E →ₗᵢ[R] F)
+/-- We use `f₁` when we need the domain to be a `normed_space`. -/
+variables (f : E →ₗᵢ[R] F) (f₁ : E₁ →ₗᵢ[R] F)
 
 instance : has_coe_to_fun (E →ₗᵢ[R] F) := ⟨_, λ f, f.to_fun⟩
 
@@ -62,11 +67,11 @@ f.to_linear_map.to_add_monoid_hom.isometry_of_norm f.norm_map
 @[simp] lemma dist_map (x y : E) : dist (f x) (f y) = dist x y := f.isometry.dist_eq x y
 @[simp] lemma edist_map (x y : E) : edist (f x) (f y) = edist x y := f.isometry.edist_eq x y
 
-protected lemma injective : injective f := f.isometry.injective
+protected lemma injective : injective f₁ := f₁.isometry.injective
 
-lemma map_eq_iff {x y : E} : f x = f y ↔ x = y := f.injective.eq_iff
+@[simp] lemma map_eq_iff {x y : E₁} : f₁ x = f₁ y ↔ x = y := f₁.injective.eq_iff
 
-lemma map_ne {x y : E} (h : x ≠ y) : f x ≠ f y := f.injective.ne h
+lemma map_ne {x y : E₁} (h : x ≠ y) : f₁ x ≠ f₁ y := f₁.injective.ne h
 
 protected lemma lipschitz : lipschitz_with 1 f := f.isometry.lipschitz
 
@@ -93,7 +98,7 @@ def to_continuous_linear_map : E →L[R] F := ⟨f.to_linear_map, f.continuous
 
 @[simp] lemma comp_continuous_iff {α : Type*} [topological_space α] {g : α → E} :
   continuous (f ∘ g) ↔ continuous g :=
-f.isometry.uniform_embedding.to_uniform_inducing.inducing.continuous_iff.symm
+f.isometry.comp_continuous_iff
 
 /-- The identity linear isometry. -/
 def id : E →ₗᵢ[R] E := ⟨linear_map.id, λ x, rfl⟩
@@ -157,8 +162,8 @@ ker_subtype _
 end submodule
 
 /-- A linear isometric equivalence between two normed vector spaces. -/
-structure linear_isometry_equiv (R E F : Type*) [semiring R] [normed_group E] [normed_group F]
-  [semimodule R E] [semimodule R F] extends E ≃ₗ[R] F :=
+structure linear_isometry_equiv (R E F : Type*) [semiring R] [semi_normed_group E]
+  [semi_normed_group F] [semimodule R E] [semimodule R F] extends E ≃ₗ[R] F :=
 (norm_map' : ∀ x, ∥to_linear_equiv x∥ = ∥x∥)
 
 notation E ` ≃ₗᵢ[`:25 R:25 `] `:0 F:0 := linear_isometry_equiv R E F

src/data/complex/is_R_or_C.lean

@@ -764,7 +764,8 @@ noncomputable def conj_clm : K →L[ℝ] K := conj_li.to_continuous_linear_map
 
 @[simp] lemma conj_clm_apply : (conj_clm : K → K) = conj := rfl
 
-@[simp] lemma conj_clm_norm : ∥(conj_clm : K →L[ℝ] K)∥ = 1 := conj_li.norm_to_continuous_linear_map
+@[simp] lemma conj_clm_norm : ∥(conj_clm : K →L[ℝ] K)∥ = 1 :=
+linear_isometry.norm_to_continuous_linear_map conj_li
 
 @[continuity] lemma continuous_conj : continuous (conj : K → K) := conj_li.continuous
 
@@ -788,7 +789,7 @@ noncomputable def of_real_clm : ℝ →L[ℝ] K := of_real_li.to_continuous_line
 @[simp] lemma of_real_clm_apply : (of_real_clm : ℝ → K) = coe := rfl
 
 @[simp] lemma of_real_clm_norm : ∥(of_real_clm : ℝ →L[ℝ] K)∥ = 1 :=
-of_real_li.norm_to_continuous_linear_map
+linear_isometry.norm_to_continuous_linear_map of_real_li
 
 @[continuity] lemma continuous_of_real : continuous (coe : ℝ → K) := of_real_li.continuous
 

src/data/padics/padic_integers.lean

@@ -195,13 +195,8 @@ variables (p : ℕ) [fact p.prime]
 instance : metric_space ℤ_[p] := subtype.metric_space
 
 instance complete_space : complete_space ℤ_[p] :=
-begin
-  delta padic_int,
-  rw [complete_space_iff_is_complete_range uniform_embedding_subtype_coe,
-    subtype.range_coe_subtype],
-  have : is_complete (closed_ball (0 : ℚ_[p]) 1) := is_closed_ball.is_complete,
-  simpa [closed_ball],
-end
+have is_closed {x : ℚ_[p] | ∥x∥ ≤ 1}, from is_closed_le continuous_norm continuous_const,
+this.complete_space_coe
 
 instance : has_norm ℤ_[p] := ⟨λ z, ∥(z : ℚ_[p])∥⟩
 

src/measure_theory/set_integral.lean

@@ -796,11 +796,11 @@ variables [borel_space E] [second_countable_topology E] [complete_space E]
 @[norm_cast] lemma integral_of_real {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜]
   {f : α → ℝ} :
   ∫ a, (f a : 𝕜) ∂μ = ↑∫ a, f a ∂μ :=
-linear_isometry.integral_comp_comm is_R_or_C.of_real_li f
+linear_isometry.integral_comp_comm (@is_R_or_C.of_real_li 𝕜 _) f
 
 lemma integral_conj {𝕜 : Type*} [is_R_or_C 𝕜] [measurable_space 𝕜] [borel_space 𝕜] {f : α → 𝕜} :
   ∫ a, is_R_or_C.conj (f a) ∂μ = is_R_or_C.conj ∫ a, f a ∂μ :=
-linear_isometry.integral_comp_comm is_R_or_C.conj_li f
+linear_isometry.integral_comp_comm (@is_R_or_C.conj_li 𝕜 _) f
 
 lemma fst_integral {f : α → E × F} (hf : integrable f μ) :
   (∫ x, f x ∂μ).1 = ∫ x, (f x).1 ∂μ :=

src/topology/metric_space/antilipschitz.lean

@@ -22,7 +22,7 @@ we do not have a `posreal` type.
 
 variables {α : Type*} {β : Type*} {γ : Type*}
 
-open_locale nnreal
+open_locale nnreal uniformity
 open set
 
 /-- We say that `f : α → β` is `antilipschitz_with K` if for any two points `x`, `y` we have
@@ -108,33 +108,39 @@ begin
   rwa [hg x, hg y] at this
 end
 
-lemma uniform_embedding_of_injective (hfinj : function.injective f) (hf : antilipschitz_with K f)
-  (hfc : uniform_continuous f) : uniform_embedding f :=
+lemma comap_uniformity_le (hf : antilipschitz_with K f) :
+  (𝓤 β).comap (prod.map f f) ≤ 𝓤 α :=
 begin
-  refine emetric.uniform_embedding_iff.2 ⟨hfinj, hfc, λ δ δ0, _⟩,
-  by_cases hK : K = 0,
-  { refine ⟨1, ennreal.zero_lt_one, λ x y _, lt_of_le_of_lt _ δ0⟩,
-    simpa only [hK, ennreal.coe_zero, zero_mul] using hf x y },
-  { refine ⟨K⁻¹ * δ, _, λ x y hxy, lt_of_le_of_lt (hf x y) _⟩,
-    { exact canonically_ordered_semiring.mul_pos.2 ⟨ennreal.inv_pos.2 ennreal.coe_ne_top, δ0⟩ },
-    { rw [mul_comm, ← div_eq_mul_inv] at hxy,
-      have := ennreal.mul_lt_of_lt_div hxy,
-      rwa mul_comm } }
+  refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 (λ ε h₀, _),
+  refine ⟨K⁻¹ * ε, ennreal.mul_pos.2 ⟨ennreal.inv_pos.2 ennreal.coe_ne_top, h₀⟩, _⟩,
+  refine λ x hx, (hf x.1 x.2).trans_lt _,
+  rw [mul_comm, ← div_eq_mul_inv] at hx,
+  rw mul_comm,
+  exact ennreal.mul_lt_of_lt_div hx
 end
 
-lemma uniform_embedding {α : Type*} {β : Type*} [emetric_space α] [pseudo_emetric_space β] {K : ℝ≥0}
-  {f : α → β} (hf : antilipschitz_with K f) (hfc : uniform_continuous f) : uniform_embedding f :=
-uniform_embedding_of_injective hf.injective hf hfc
+protected lemma uniform_inducing (hf : antilipschitz_with K f) (hfc : uniform_continuous f) :
+  uniform_inducing f :=
+⟨le_antisymm hf.comap_uniformity_le hfc.le_comap⟩
+
+protected lemma uniform_embedding {α : Type*} {β : Type*} [emetric_space α] [pseudo_emetric_space β]
+  {K : ℝ≥0} {f : α → β} (hf : antilipschitz_with K f) (hfc : uniform_continuous f) :
+  uniform_embedding f :=
+⟨hf.uniform_inducing hfc, hf.injective⟩
+
+lemma is_complete_range [complete_space α] (hf : antilipschitz_with K f)
+  (hfc : uniform_continuous f) : is_complete (range f) :=
+(hf.uniform_inducing hfc).is_complete_range
+
+lemma is_closed_range {α β : Type*} [pseudo_emetric_space α] [emetric_space β] [complete_space α]
+  {f : α → β} {K : ℝ≥0} (hf : antilipschitz_with K f) (hfc : uniform_continuous f) :
+  is_closed (range f) :=
+(hf.is_complete_range hfc).is_closed
 
 lemma closed_embedding {α : Type*} {β : Type*} [emetric_space α] [emetric_space β] {K : ℝ≥0}
   {f : α → β} [complete_space α] (hf : antilipschitz_with K f) (hfc : uniform_continuous f) :
   closed_embedding f :=
-{ closed_range :=
-  begin
-    apply is_complete.is_closed,
-    rw ← complete_space_iff_is_complete_range (hf.uniform_embedding hfc),
-    apply_instance,
-  end,
+{ closed_range := hf.is_closed_range hfc,
   .. (hf.uniform_embedding hfc).embedding }
 
 lemma subtype_coe (s : set α) : antilipschitz_with 1 (coe : s → α) :=

src/topology/metric_space/closeds.lean

@@ -282,14 +282,15 @@ end
 from the same statement for closed subsets -/
 instance nonempty_compacts.complete_space [complete_space α] :
   complete_space (nonempty_compacts α) :=
-(complete_space_iff_is_complete_range nonempty_compacts.to_closeds.uniform_embedding).2 $
+(complete_space_iff_is_complete_range
+  nonempty_compacts.to_closeds.uniform_embedding.to_uniform_inducing).2 $
   nonempty_compacts.is_closed_in_closeds.is_complete
 
 /-- In a compact space, the type of nonempty compact subsets is compact. This follows from
 the same statement for closed subsets -/
 instance nonempty_compacts.compact_space [compact_space α] : compact_space (nonempty_compacts α) :=
 ⟨begin
-  rw embedding.compact_iff_compact_image nonempty_compacts.to_closeds.uniform_embedding.embedding,
+  rw nonempty_compacts.to_closeds.uniform_embedding.embedding.compact_iff_compact_image,
   rw [image_univ],
   exact nonempty_compacts.is_closed_in_closeds.compact
 end⟩

src/topology/metric_space/isometry.lean

@@ -75,6 +75,11 @@ assume x y, calc
   edist ((g ∘ f) x) ((g ∘ f) y) = edist (f x) (f y) : hg _ _
                             ... = edist x y : hf _ _
 
+/-- An isometry from a metric space is a uniform inducing map -/
+theorem isometry.uniform_inducing (hf : isometry f) :
+  uniform_inducing f :=
+hf.antilipschitz.uniform_inducing hf.lipschitz.uniform_continuous
+
 /-- An isometry from a metric space is a uniform embedding -/
 theorem isometry.uniform_embedding {α : Type u} {β : Type v} [emetric_space α]
   [pseudo_emetric_space β] {f : α → β} (hf : isometry f) :
@@ -109,15 +114,14 @@ by { rw ← image_univ, exact hf.ediam_image univ }
 lemma isometry_subtype_coe {s : set α} : isometry (coe : s → α) :=
 λx y, rfl
 
-lemma isometry.comp_continuous_on_iff {α : Type u} [emetric_space α] {f : α → β} {γ}
-  [topological_space γ] (hf : isometry f) {g : γ → α} {s : set γ} :
+lemma isometry.comp_continuous_on_iff {γ} [topological_space γ] (hf : isometry f) {g : γ → α}
+  {s : set γ} :
   continuous_on (f ∘ g) s ↔ continuous_on g s :=
-hf.uniform_embedding.to_uniform_inducing.inducing.continuous_on_iff.symm
+hf.uniform_inducing.inducing.continuous_on_iff.symm
 
-lemma isometry.comp_continuous_iff {α : Type u} [emetric_space α] {f : α → β} {γ}
-  [topological_space γ] (hf : isometry f) {g : γ → α} :
+lemma isometry.comp_continuous_iff {γ} [topological_space γ] (hf : isometry f) {g : γ → α} :
   continuous (f ∘ g) ↔ continuous g :=
-hf.uniform_embedding.to_uniform_inducing.inducing.continuous_iff.symm
+hf.uniform_inducing.inducing.continuous_iff.symm
 
 end emetric_isometry --section
 

src/topology/metric_space/pi_Lp.lean

@@ -184,9 +184,9 @@ end
 lemma aux_uniformity_eq :
   𝓤 (pi_Lp p hp β) = @uniformity _ (Pi.uniform_space _) :=
 begin
-  have A : uniform_embedding (pi_Lp.equiv p hp β) :=
-    (antilipschitz_with_equiv p hp β).uniform_embedding_of_injective (pi_Lp.equiv p hp β).injective
-      (lipschitz_with_equiv p hp β).uniform_continuous,
+  have A : uniform_inducing (pi_Lp.equiv p hp β) :=
+    (antilipschitz_with_equiv p hp β).uniform_inducing
+    (lipschitz_with_equiv p hp β).uniform_continuous,
   have : (λ (x : pi_Lp p hp β × pi_Lp p hp β),
     ((pi_Lp.equiv p hp β) x.fst, (pi_Lp.equiv p hp β) x.snd)) = id,
     by ext i; refl,

src/topology/uniform_space/basic.lean

@@ -1065,10 +1065,14 @@ lemma uniform_continuous_comap' {f : γ → β} {g : α → γ} [v : uniform_spa
   (h : uniform_continuous (f ∘ g)) : @uniform_continuous α γ u (uniform_space.comap f v) g :=
 tendsto_comap_iff.2 h
 
+lemma to_nhds_mono {u₁ u₂ : uniform_space α} (h : u₁ ≤ u₂) (a : α) :
+  @nhds _ (@uniform_space.to_topological_space _ u₁) a ≤
+    @nhds _ (@uniform_space.to_topological_space _ u₂) a :=
+by rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]; exact (lift'_mono h le_rfl)
+
 lemma to_topological_space_mono {u₁ u₂ : uniform_space α} (h : u₁ ≤ u₂) :
   @uniform_space.to_topological_space _ u₁ ≤ @uniform_space.to_topological_space _ u₂ :=
-le_of_nhds_le_nhds $ assume a,
-  by rw [@nhds_eq_uniformity α u₁ a, @nhds_eq_uniformity α u₂ a]; exact (lift'_mono h $ le_refl _)
+le_of_nhds_le_nhds $ to_nhds_mono h
 
 lemma uniform_continuous.continuous [uniform_space α] [uniform_space β] {f : α → β}
   (hf : uniform_continuous f) : continuous f :=

src/topology/uniform_space/uniform_embedding.lean

@@ -177,40 +177,48 @@ begin
   exact ⟨x, hx, hyf⟩
 end
 
-/-- A set is complete iff its image under a uniform embedding is complete. -/
-lemma is_complete_image_iff {m : α → β} {s : set α} (hm : uniform_embedding m) :
+lemma is_complete.complete_space_coe {s : set α} (hs : is_complete s) :
+  complete_space s :=
+complete_space_iff_is_complete_univ.2 $
+  is_complete_of_complete_image uniform_embedding_subtype_coe.to_uniform_inducing $ by simp [hs]
+
+/-- A set is complete iff its image under a uniform inducing map is complete. -/
+lemma is_complete_image_iff {m : α → β} {s : set α} (hm : uniform_inducing m) :
   is_complete (m '' s) ↔ is_complete s :=
 begin
-  refine ⟨is_complete_of_complete_image hm.to_uniform_inducing, λ c f hf fs, _⟩,
-  rw filter.le_principal_iff at fs,
-  have hfm : range m ∈ f, from mem_sets_of_superset fs (image_subset_range _ _),
-  let f' := comap m f,
-  have cf' : cauchy f' := hf.comap' hm.comap_uniformity.le (ne_bot.comap_of_range_mem hf.1 hfm),
-  have : f' ≤ 𝓟 s := by simp [f']; exact
-    ⟨m '' s, by simpa using fs, by simp [preimage_image_eq s hm.inj]⟩,
-  rcases c f' cf' this with ⟨x, xs, hx⟩,
-  existsi [m x, mem_image_of_mem m xs],
-  rwa [(uniform_embedding.embedding hm).to_inducing.nhds_eq_comap, comap_le_comap_iff hfm] at hx
+  refine ⟨is_complete_of_complete_image hm, λ c, _⟩,
+  haveI : complete_space s := c.complete_space_coe,
+  set m' : s → β := m ∘ coe,
+  suffices : is_complete (range m'), by rwa [range_comp, subtype.range_coe] at this,
+  have hm' : uniform_inducing m' := hm.comp uniform_embedding_subtype_coe.to_uniform_inducing,
+  intros f hf hfm,
+  rw filter.le_principal_iff at hfm,
+  have cf' : cauchy (comap m' f) :=
+    hf.comap' hm'.comap_uniformity.le (ne_bot.comap_of_range_mem hf.1 hfm),
+  rcases complete_space.complete cf' with ⟨x, hx⟩,
+  rw [hm'.inducing.nhds_eq_comap, comap_le_comap_iff hfm] at hx,
+  use [m' x, mem_range_self _, hx]
 end
 
-lemma complete_space_iff_is_complete_range {f : α → β} (hf : uniform_embedding f) :
+lemma complete_space_iff_is_complete_range {f : α → β} (hf : uniform_inducing f) :
   complete_space α ↔ is_complete (range f) :=
 by rw [complete_space_iff_is_complete_univ, ← is_complete_image_iff hf, image_univ]
 
+lemma uniform_inducing.is_complete_range [complete_space α] {f : α → β}
+  (hf : uniform_inducing f) :
+  is_complete (range f) :=
+(complete_space_iff_is_complete_range hf).1 ‹_›
+
 lemma complete_space_congr {e : α ≃ β} (he : uniform_embedding e) :
   complete_space α ↔ complete_space β :=
-by rw [complete_space_iff_is_complete_range he, e.range_eq_univ,
+by rw [complete_space_iff_is_complete_range he.to_uniform_inducing, e.range_eq_univ,
   complete_space_iff_is_complete_univ]
 
 lemma complete_space_coe_iff_is_complete {s : set α} :
   complete_space s ↔ is_complete s :=
-(complete_space_iff_is_complete_range uniform_embedding_subtype_coe).trans $
+(complete_space_iff_is_complete_range uniform_embedding_subtype_coe.to_uniform_inducing).trans $
   by rw [subtype.range_coe]
 
-lemma is_complete.complete_space_coe {s : set α} (hs : is_complete s) :
-  complete_space s :=
-complete_space_coe_iff_is_complete.2 hs
-
 lemma is_closed.complete_space_coe [complete_space α] {s : set α} (hs : is_closed s) :
   complete_space s :=
 hs.is_complete.complete_space_coe