refactor(topology/continuous_functions): change file layout (#6890)

Moves `topology/bounded_continuous_function.lean` to `topology/continuous_functions/bounded.lean`, splitting out the content about continuous functions on a compact space to `topology/continuous_functions/compact.lean`.

Renames `topology/continuous_map.lean` to `topology/continuous_functions/basic.lean`.

Renames `topology/algebra/continuous_functions.lean` to `topology/continuous_functions/algebra.lean`.

Also changes the direction of the equivalences, replacing `bounded_continuous_function.equiv_continuous_map_of_compact` with `continuous_map.equiv_bounded_of_compact` (and also the more structured version).

There's definitely more work to be done here, particularly giving at least some lemmas characterising the norm on `C(α, β)`, but I wanted to do a minimal PR changing the layout first.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/geometry/manifold/times_cont_mdiff_map.lean

@@ -5,7 +5,7 @@ Authors: Nicolò Cavalleri
 -/
 
 import geometry.manifold.times_cont_mdiff
-import topology.continuous_map
+import topology.continuous_function.basic
 
 /-!
 # Smooth bundled map

src/topology/algebra/affine.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Frédéric Dupuis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Frédéric Dupuis
 -/
-import topology.algebra.continuous_functions
+import topology.continuous_function.algebra
 import linear_algebra.affine_space.affine_map
 
 /-!

src/topology/category/Top/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Scott Morrison, Mario Carneiro
 -/
 import category_theory.concrete_category.unbundled_hom
-import topology.continuous_map
+import topology.continuous_function.basic
 import topology.opens
 
 /-!

src/topology/compact_open.lean

@@ -6,7 +6,7 @@ Authors: Reid Barton
 Type of continuous maps and the compact-open topology on them.
 -/
 import topology.subset_properties
-import topology.continuous_map
+import topology.continuous_function.basic
 import topology.homeomorph
 import tactic.tidy
 

src/topology/algebra/continuous_functions.lean → src/topology/continuous_function/algebra.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Nicolò Cavalleri
 -/
 import topology.algebra.module
-import topology.continuous_map
+import topology.continuous_function.basic
 import algebra.algebra.subalgebra
 
 /-!

src/topology/continuous_map.lean → src/topology/continuous_function/basic.lean

@@ -144,6 +144,8 @@ instance [linear_order β] [order_closed_topology β] : lattice C(α, β) :=
 { ..continuous_map.semilattice_inf,
   ..continuous_map.semilattice_sup }
 
+-- TODO transfer this lattice structure to `bounded_continuous_function`
+
 end lattice
 
 end continuous_map

src/topology/bounded_continuous_function.lean → src/topology/continuous_function/bounded.lean

@@ -3,8 +3,7 @@ Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Mario Carneiro, Yury Kudryashov, Heather Macbeth
 -/
-import analysis.normed_space.linear_isometry
-import tactic.equiv_rw
+import analysis.normed_space.basic
 
 /-!
 # Bounded continuous functions
@@ -87,14 +86,6 @@ def forget_boundedness : (α →ᵇ β) → C(α, β) :=
 @[simp] lemma forget_boundedness_coe (f : α →ᵇ β) : (forget_boundedness α β f : α → β) = f :=
 rfl
 
-/--
-When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
-equivalent to `C(α, 𝕜)`.
--/
-@[simps]
-def equiv_continuous_map_of_compact [compact_space α] : (α →ᵇ β) ≃ C(α, β) :=
-⟨forget_boundedness α β, mk_of_compact, λ f, by { ext, refl, }, λ f, by { ext, refl, }⟩
-
 end
 
 /-- The uniform distance between two bounded continuous functions -/
@@ -179,24 +170,7 @@ instance : metric_space (α →ᵇ β) :=
     (dist_le (add_nonneg dist_nonneg' dist_nonneg')).2 $ λ x,
       le_trans (dist_triangle _ _ _) (add_le_add (dist_coe_le_dist _) (dist_coe_le_dist _)) }
 
-instance [compact_space α] : metric_space C(α,β) :=
-metric_space.induced
-  (equiv_continuous_map_of_compact α β).symm
-  (equiv_continuous_map_of_compact α β).symm.injective
-  (by apply_instance)
-
-variables (α β)
-/--
-When `α` is compact, and `β` is a metric space, the bounded continuous maps `α →ᵇ β` are
-isometric to `C(α, β)`.
--/
-@[simps]
-def isometric_continuous_map_of_compact [compact_space α] :
-  (α →ᵇ β) ≃ᵢ C(α, β) :=
-{ isometry_to_fun := λ x y, rfl,
-  to_equiv := equiv_continuous_map_of_compact α β }
-
-variable {β}
+variables (α) {β}
 
 /-- Constant as a continuous bounded function. -/
 def const (b : β) : α →ᵇ β := ⟨continuous_map.const b, 0, by simp [le_refl]⟩
@@ -610,46 +584,6 @@ def forget_boundedness_add_hom : (α →ᵇ β) →+ C(α, β) :=
   map_zero' := by { ext, simp, },
   map_add' := by { intros, ext, simp, }, }
 
-section compact_space
-variables [compact_space α]
-
-section
-
-/--
-When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
-additively equivalent to `C(α, 𝕜)`.
--/
-@[simps]
-def add_equiv_continuous_map_of_compact : (α →ᵇ β) ≃+ C(α, β) :=
-{ ..forget_boundedness_add_hom α β,
-  ..equiv_continuous_map_of_compact α β, }
-
-@[simp]
-lemma add_equiv_continuous_map_of_compact_to_equiv :
-  (add_equiv_continuous_map_of_compact α β).to_equiv = equiv_continuous_map_of_compact α β :=
-rfl
-
-end
-
--- TODO at some point we will need lemmas characterising this norm!
--- At the moment the only way to reason about it is to transfer `f : C(α,β)` back to `α →ᵇ β`.
-instance : has_norm C(α,β) :=
-{ norm := λ x, dist x 0 }
-
-instance : normed_group C(α,β) :=
-{ dist_eq := λ x y,
-  begin
-    change dist x y = dist (x-y) 0,
-     -- it would be nice if `equiv_rw` could rewrite in multiple places at once
-    equiv_rw (equiv_continuous_map_of_compact α β).symm at x,
-    equiv_rw (equiv_continuous_map_of_compact α β).symm at y,
-    have p : dist x y = dist (x-y) 0, { rw dist_eq_norm, rw dist_zero_right, },
-    convert p,
-    exact ((add_equiv_continuous_map_of_compact α β).map_sub _ _).symm,
-  end, }
-
-end compact_space
-
 end normed_group
 
 section normed_space
@@ -683,13 +617,6 @@ semimodule.of_core $
 instance : normed_space 𝕜 (α →ᵇ β) := ⟨λ c f, norm_of_normed_group_le _
   (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _⟩
 
-instance [compact_space α] : normed_space 𝕜 C(α,β) :=
-{ norm_smul_le := λ c f,
-  begin
-    equiv_rw (equiv_continuous_map_of_compact α β).symm at f,
-    exact le_of_eq (norm_smul c f),
-  end }
-
 end normed_space
 
 section normed_ring
@@ -721,15 +648,6 @@ instance : normed_ring (α →ᵇ R) :=
 { norm_mul := λ f g, norm_of_normed_group_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _,
   .. bounded_continuous_function.normed_group }
 
-instance [compact_space α] : normed_ring C(α,R) :=
-{ norm_mul := λ f g,
-  begin
-    equiv_rw (equiv_continuous_map_of_compact α R).symm at f,
-    equiv_rw (equiv_continuous_map_of_compact α R).symm at g,
-    exact norm_mul_le f g,
-  end,
-  ..(infer_instance : normed_group C(α,R)) }
-
 end normed_ring
 
 section normed_comm_ring
@@ -816,37 +734,6 @@ norm_of_normed_group_le _ (mul_nonneg (norm_nonneg _) (norm_nonneg _)) _
 show that the space of bounded continuous functions from `α` to `β` is naturally a normed
 module over the algebra of bounded continuous functions from `α` to `𝕜`. -/
 
-variables (α 𝕜)
-
-/--
-When `α` is compact and `𝕜` is a normed field,
-the `𝕜`-algebra of bounded continuous maps `α →ᵇ 𝕜` is
-`𝕜`-linearly isometric to `C(α, 𝕜)`.
--/
-def linear_isometry_continuous_map_of_compact [compact_space α] :
-  (α →ᵇ 𝕜) ≃ₗᵢ[𝕜] C(α, 𝕜) :=
-{ map_smul' := λ c f, by { ext, simp, },
-  norm_map' := λ f, rfl,
-  ..add_equiv_continuous_map_of_compact α 𝕜 }
-
-@[simp]
-lemma isometric_continuous_map_of_compact_to_isometric [compact_space α] :
-  (linear_isometry_continuous_map_of_compact α 𝕜).to_isometric =
-    isometric_continuous_map_of_compact α 𝕜 :=
-rfl
-
-@[simp]
-lemma linear_isometry_continuous_map_of_compact_to_add_equiv [compact_space α] :
-  (linear_isometry_continuous_map_of_compact α 𝕜).to_linear_equiv.to_add_equiv =
-    add_equiv_continuous_map_of_compact α 𝕜 :=
-rfl
-
-@[simp]
-lemma linear_isometry_continuous_map_of_compact_to_equiv [compact_space α] :
-  (linear_isometry_continuous_map_of_compact α 𝕜).to_linear_equiv.to_equiv =
-    equiv_continuous_map_of_compact α 𝕜 :=
-rfl
-
 end normed_algebra
 
 end bounded_continuous_function

src/topology/continuous_function/compact.lean

@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import topology.continuous_function.bounded
+import analysis.normed_space.linear_isometry
+import tactic.equiv_rw
+
+/-!
+# Continuous functions on a compact space
+
+Continuous functions `C(α, β)` from a compact space `α` to a metric space `β`
+are automatically bounded, and so acquire various structures inherited from `α →ᵇ β`.
+
+This file transfers these structures, and restates some lemmas
+characterising these structures.
+
+If you need a lemma which is proved about `α →ᵇ β` but not for `C(α, β)` when `α` is compact,
+you should restate it here. You can also use
+`bounded_continuous_function.equiv_continuous_map_of_compact` to functions back and forth.
+
+-/
+
+noncomputable theory
+open_locale topological_space classical nnreal bounded_continuous_function
+
+open set filter metric
+
+variables (α : Type*) (β : Type*) [topological_space α] [compact_space α] [normed_group β]
+
+open bounded_continuous_function
+
+namespace continuous_map
+
+/--
+When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
+equivalent to `C(α, 𝕜)`.
+-/
+@[simps]
+def equiv_bounded_of_compact : C(α, β) ≃ (α →ᵇ β) :=
+⟨mk_of_compact, forget_boundedness α β, λ f, by { ext, refl, }, λ f, by { ext, refl, }⟩
+
+/--
+When `α` is compact, the bounded continuous maps `α →ᵇ 𝕜` are
+additively equivalent to `C(α, 𝕜)`.
+-/
+@[simps]
+def add_equiv_bounded_of_compact : C(α, β) ≃+ (α →ᵇ β) :=
+({ ..forget_boundedness_add_hom α β,
+  ..(equiv_bounded_of_compact α β).symm, } : (α →ᵇ β) ≃+ C(α, β)).symm
+
+-- It would be nice if `@[simps]` produced this directly,
+-- instead of the unhelpful `add_equiv_bounded_of_compact_apply_to_continuous_map`.
+@[simp]
+lemma add_equiv_bounded_of_compact_apply_apply (f : C(α, β)) (a : α) :
+  add_equiv_bounded_of_compact α β f a = f a :=
+rfl
+
+@[simp]
+lemma add_equiv_bounded_of_compact_to_equiv :
+  (add_equiv_bounded_of_compact α β).to_equiv = equiv_bounded_of_compact α β :=
+rfl
+
+instance : metric_space C(α,β) :=
+metric_space.induced
+  (equiv_bounded_of_compact α β)
+  (equiv_bounded_of_compact α β).injective
+  (by apply_instance)
+
+variables (α β)
+
+/--
+When `α` is compact, and `β` is a metric space, the bounded continuous maps `α →ᵇ β` are
+isometric to `C(α, β)`.
+-/
+@[simps]
+def isometric_bounded_of_compact :
+  C(α, β) ≃ᵢ (α →ᵇ β) :=
+{ isometry_to_fun := λ x y, rfl,
+  to_equiv := equiv_bounded_of_compact α β }
+
+-- TODO at some point we will need lemmas characterising this norm!
+-- At the moment the only way to reason about it is to transfer `f : C(α,β)` back to `α →ᵇ β`.
+instance : has_norm C(α,β) :=
+{ norm := λ x, dist x 0 }
+
+instance : normed_group C(α,β) :=
+{ dist_eq := λ x y,
+  begin
+    change dist x y = dist (x-y) 0,
+     -- it would be nice if `equiv_rw` could rewrite in multiple places at once
+    equiv_rw (equiv_bounded_of_compact α β) at x,
+    equiv_rw (equiv_bounded_of_compact α β) at y,
+    have p : dist x y = dist (x-y) 0, { rw dist_eq_norm, rw dist_zero_right, },
+    convert p,
+    exact ((add_equiv_bounded_of_compact α β).symm.map_sub _ _).symm,
+  end, }
+
+section
+variables {R : Type*} [normed_ring R]
+
+instance : normed_ring C(α,R) :=
+{ norm_mul := λ f g,
+  begin
+    equiv_rw (equiv_bounded_of_compact α R) at f,
+    equiv_rw (equiv_bounded_of_compact α R) at g,
+    exact norm_mul_le f g,
+  end,
+  ..(infer_instance : normed_group C(α,R)) }
+
+end
+
+section
+variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 β]
+
+instance : normed_space 𝕜 C(α,β) :=
+{ norm_smul_le := λ c f,
+  begin
+    equiv_rw (equiv_bounded_of_compact α β) at f,
+    exact le_of_eq (norm_smul c f),
+  end }
+
+variables (α 𝕜)
+
+/--
+When `α` is compact and `𝕜` is a normed field,
+the `𝕜`-algebra of bounded continuous maps `α →ᵇ 𝕜` is
+`𝕜`-linearly isometric to `C(α, 𝕜)`.
+-/
+def linear_isometry_bounded_of_compact :
+  C(α, 𝕜) ≃ₗᵢ[𝕜] (α →ᵇ 𝕜) :=
+{ map_smul' := λ c f, by { ext, simp, },
+  norm_map' := λ f, rfl,
+  ..add_equiv_bounded_of_compact α 𝕜 }
+
+@[simp]
+lemma linear_isometry_bounded_of_compact_to_isometric :
+  (linear_isometry_bounded_of_compact α 𝕜).to_isometric =
+    isometric_bounded_of_compact α 𝕜 :=
+rfl
+
+@[simp]
+lemma linear_isometry_bounded_of_compact_to_add_equiv :
+  (linear_isometry_bounded_of_compact α 𝕜).to_linear_equiv.to_add_equiv =
+    add_equiv_bounded_of_compact α 𝕜 :=
+rfl
+
+@[simp]
+lemma linear_isometry_bounded_of_compact_of_compact_to_equiv :
+  (linear_isometry_bounded_of_compact α 𝕜).to_linear_equiv.to_equiv =
+    equiv_bounded_of_compact α 𝕜 :=
+rfl
+
+end
+
+end continuous_map

src/topology/instances/real.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 import topology.metric_space.basic
 import topology.algebra.uniform_group
 import topology.algebra.ring
-import topology.algebra.continuous_functions
+import topology.continuous_function.algebra
 import ring_theory.subring
 import group_theory.archimedean
 /-!

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -8,7 +8,7 @@ their Hausdorff distance. This construction is instrumental to study the Gromov-
 distance between nonempty compact metric spaces -/
 import topology.metric_space.gluing
 import topology.metric_space.hausdorff_distance
-import topology.bounded_continuous_function
+import topology.continuous_function.bounded
 
 noncomputable theory
 open_locale classical topological_space nnreal