feat(topology): the currying homeomorphism (#6319)

src/topology/compact_open.lean

@@ -7,8 +7,34 @@ Type of continuous maps and the compact-open topology on them.
 -/
 import topology.subset_properties
 import topology.continuous_map
+import topology.homeomorph
 import tactic.tidy
 
+/-!
+# The compact-open topology
+
+In this file, we define the compact-open topology on the set of continuous maps between two
+topological spaces.
+
+## Main definitions
+
+* `compact_open` is the compact-open topology on `C(α, β)`. It is declared as an instance.
+* `ev` is the evaluation map `C(α, β) × α → β`. It is continuous as long as `α` is locally compact.
+* `coev` is the coevaluation map `β → C(α, β × α)`. It is always continuous.
+* `continuous_map.curry` is the currying map `C(α × β, γ) → C(α, C(β, γ))`. This map always exists
+  and it is continuous as long as `α × β` is locally compact.
+* `continuous_map.uncurry` is the uncurrying map `C(α, C(β, γ)) → C(α × β, γ)`. For this map to
+  exist, we need `β` to be locally compact. If `α` is also locally compact, then this map is
+  continuous.
+* `homeomorph.curry` combines the currying and uncurrying operations into a homeomorphism
+  `C(α × β, γ) ≃ₜ C(α, C(β, γ))`. This homeomorphism exists if `α` and `β` are locally compact.
+
+
+## Tags
+
+compact-open, curry, function space
+-/
+
 open set
 open_locale topological_space
 
@@ -104,6 +130,75 @@ end
 
 end coev
 
+section curry
+
+/-- Auxiliary definition, see `continuous_map.curry` and `homeomorph.curry`. -/
+def curry' (f : C(α × β, γ)) (a : α) : C(β, γ) := ⟨function.curry f a⟩
+
+/-- If a map `α × β → γ` is continuous, then its curried form `α → C(β, γ)` is continuous. -/
+lemma continuous_curry' (f : C(α × β, γ)) : continuous (curry' f) :=
+have hf : curry' f = continuous_map.induced f.continuous_to_fun ∘ coev _ _, by { ext, refl },
+hf ▸ continuous.comp (continuous_induced f.continuous_to_fun) continuous_coev
+
+/-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form
+    `α × β → γ` is continuous. -/
+lemma continuous_of_continuous_uncurry (f : α → C(β, γ))
+  (h : continuous (function.uncurry (λ x y, f x y))) : continuous f :=
+by { convert continuous_curry' ⟨_, h⟩, ext, refl }
+
+/-- The curried form of a continuous map `α × β → γ` as a continuous map `α → C(β, γ)`.
+    If `a × β` is locally compact, this is continuous. If `α` and `β` are both locally
+    compact, then this is a homeomorphism, see `homeomorph.curry`. -/
+def curry (f : C(α × β, γ)) : C(α, C(β, γ)) :=
+⟨_, continuous_curry' f⟩
+
+/-- The currying process is a continuous map between function spaces. -/
+lemma continuous_curry [locally_compact_space (α × β)] :
+  continuous (curry : C(α × β, γ) → C(α, C(β, γ))) :=
+begin
+  apply continuous_of_continuous_uncurry,
+  apply continuous_of_continuous_uncurry,
+  rw ←homeomorph.comp_continuous_iff' (homeomorph.prod_assoc _ _ _).symm,
+  convert continuous_ev;
+  tidy
+end
+
+/-- The uncurried form of a continuous map `α → C(β, γ)` is a continuous map `α × β → γ`. -/
+lemma continuous_uncurry_of_continuous [locally_compact_space β] (f : C(α, C(β, γ))) :
+  continuous (function.uncurry (λ x y, f x y)) :=
+have hf : function.uncurry (λ x y, f x y) = ev β γ ∘ prod.map f id, by { ext, refl },
+hf ▸ continuous.comp continuous_ev $ continuous.prod_map f.2 id.2
+
+/-- The uncurried form of a continuous map `α → C(β, γ)` as a continuous map `α × β → γ` (if `β` is
+    locally compact). If `α` is also locally compact, then this is a homeomorphism between the two
+    function spaces, see `homeomorph.curry`. -/
+def uncurry [locally_compact_space β] (f : C(α, C(β, γ))) : C(α × β, γ) :=
+⟨_, continuous_uncurry_of_continuous f⟩
+
+/-- The uncurrying process is a continuous map between function spaces. -/
+lemma continuous_uncurry [locally_compact_space α] [locally_compact_space β] :
+  continuous (uncurry : C(α, C(β, γ)) → C(α × β, γ)) :=
+begin
+  apply continuous_of_continuous_uncurry,
+  rw ←homeomorph.comp_continuous_iff' (homeomorph.prod_assoc _ _ _),
+  apply continuous.comp continuous_ev (continuous.prod_map continuous_ev id.2);
+  apply_instance
+end
+
+end curry
+
 end compact_open
 
 end continuous_map
+
+open continuous_map
+
+namespace homeomorph
+variables {α : Type*} {β : Type*} {γ : Type*}
+variables [topological_space α] [topological_space β] [topological_space γ]
+
+/-- Currying as a homeomorphism between the function spaces `C(α × β, γ)` and `C(α, C(β, γ))`. -/
+def curry [locally_compact_space α] [locally_compact_space β] : C(α × β, γ) ≃ₜ C(α, C(β, γ)) :=
+⟨⟨curry, uncurry, by tidy, by tidy⟩, continuous_curry, continuous_uncurry⟩
+
+end homeomorph

src/topology/subset_properties.lean

@@ -635,6 +635,21 @@ compact-open topology. -/
 class locally_compact_space (α : Type*) [topological_space α] : Prop :=
 (local_compact_nhds : ∀ (x : α) (n ∈ 𝓝 x), ∃ s ∈ 𝓝 x, s ⊆ n ∧ is_compact s)
 
+instance locally_compact_space.prod (α : Type*) (β : Type*) [topological_space α]
+  [topological_space β] [locally_compact_space α] [locally_compact_space β] :
+  locally_compact_space (α × β) :=
+{ local_compact_nhds :=
+  begin
+    rintros ⟨x, y⟩ n hn,
+    obtain ⟨u, hu, v, hv, huv⟩ := mem_nhds_prod_iff.1 hn,
+    obtain ⟨a, ha₁, ha₂, ha₃⟩ := locally_compact_space.local_compact_nhds _ _ hu,
+    obtain ⟨b, hb₁, hb₂, hb₃⟩ := locally_compact_space.local_compact_nhds _ _ hv,
+    refine ⟨a.prod b, _, _, _⟩,
+    { exact mem_nhds_prod_iff.2 ⟨_, ha₁, _, hb₁, subset.rfl⟩ },
+    { exact subset.trans (prod_mono ha₂ hb₂) huv },
+    { exact is_compact.prod ha₃ hb₃ }
+  end }
+
 /-- A reformulation of the definition of locally compact space: In a locally compact space,
   every open set containing `x` has a compact subset containing `x` in its interior. -/
 lemma exists_compact_subset [locally_compact_space α] {x : α} {U : set α}