refactor(topology/*): Hom classes for continuous maps/homs (#11909)

Add
* `continuous_map_class`
* `bounded_continuous_map_class`
* `continuous_monoid_hom_class`
* `continuous_add_monoid_hom_class`
* `continuous_map.homotopy_class`

to follow the `fun_like` design. Deprecate lemmas accordingly.

Also rename a few fields to match the convention in the rest of the library.

Author: YaelDillies

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -502,7 +502,7 @@ variables (f : R →+* S)
   (comap f y).as_ideal = ideal.comap f y.as_ideal :=
 rfl
 
-@[simp] lemma comap_id : comap (ring_hom.id R) = continuous_map.id := by { ext, refl }
+@[simp] lemma comap_id : comap (ring_hom.id R) = continuous_map.id _ := by { ext, refl }
 
 @[simp] lemma comap_comp (f : R →+* S) (g : S →+* S') :
   comap (g.comp f) = (comap f).comp (comap g) :=

src/topology/algebra/continuous_monoid_hom.lean

@@ -14,54 +14,96 @@ This file defines the space of continuous homomorphisms between two topological
 ## Main definitions
 
 * `continuous_monoid_hom A B`: The continuous homomorphisms `A →* B`.
-
+* `continuous_add_monoid_hom α β`: The continuous additive homomorphisms `α →+ β`.
 -/
 
-variables (A B C D E : Type*)
+open function
+
+variables {F α β : Type*} (A B C D E : Type*)
   [monoid A] [monoid B] [monoid C] [monoid D] [comm_group E]
   [topological_space A] [topological_space B] [topological_space C] [topological_space D]
   [topological_space E] [topological_group E]
 
-set_option old_structure_cmd true
+/-- The type of continuous additive monoid homomorphisms from `α` to `β`.
 
-/-- Continuous homomorphisms between two topological groups. -/
-structure continuous_monoid_hom extends A →* B, continuous_map A B
+When possible, instead of parametrizing results over `(f : continuous_add_monoid_hom α β)`,
+you should parametrize over `(F : Type*) [continuous_add_monoid_hom_class F α β] (f : F)`.
 
-/-- Continuous homomorphisms between two topological groups. -/
+When you extend this structure, make sure to extend `continuous_add_monoid_hom_class`. -/
 structure continuous_add_monoid_hom (A B : Type*) [add_monoid A] [add_monoid B]
-  [topological_space A] [topological_space B] extends A →+ B, continuous_map A B
+  [topological_space A] [topological_space B] extends A →+ B :=
+(continuous_to_fun : continuous to_fun)
+
+/-- The type of continuous monoid homomorphisms from `α` to `β`.
+
+When possible, instead of parametrizing results over `(f : continuous_monoid_hom α β)`,
+you should parametrize over `(F : Type*) [continuous_monoid_hom_class F α β] (f : F)`.
 
-attribute [to_additive] continuous_monoid_hom
-attribute [to_additive] continuous_monoid_hom.to_monoid_hom
+When you extend this structure, make sure to extend `continuous_add_monoid_hom_class`. -/
+@[to_additive]
+structure continuous_monoid_hom extends A →* B :=
+(continuous_to_fun : continuous to_fun)
 
-initialize_simps_projections continuous_monoid_hom (to_fun → apply)
+/-- `continuous_add_monoid_hom_class F α β` states that `F` is a type of continuous additive monoid
+homomorphisms.
+
+You should also extend this typeclass when you extend `continuous_add_monoid_hom`. -/
+class continuous_add_monoid_hom_class (F α β : Type*) [add_monoid α] [add_monoid β]
+  [topological_space α] [topological_space β] extends add_monoid_hom_class F α β :=
+(map_continuous (f : F) : continuous f)
+
+/-- `continuous_monoid_hom_class F α β` states that `F` is a type of continuous additive monoid
+homomorphisms.
+
+You should also extend this typeclass when you extend `continuous_monoid_hom`. -/
+@[to_additive]
+class continuous_monoid_hom_class (F α β : Type*) [monoid α] [monoid β]
+  [topological_space α] [topological_space β] extends monoid_hom_class F α β :=
+(map_continuous (f : F) : continuous f)
 
 /-- Reinterpret a `continuous_monoid_hom` as a `monoid_hom`. -/
 add_decl_doc continuous_monoid_hom.to_monoid_hom
 
-/-- Reinterpret a `continuous_monoid_hom` as a `continuous_map`. -/
-add_decl_doc continuous_monoid_hom.to_continuous_map
-
 /-- Reinterpret a `continuous_add_monoid_hom` as an `add_monoid_hom`. -/
 add_decl_doc continuous_add_monoid_hom.to_add_monoid_hom
 
-/-- Reinterpret a `continuous_add_monoid_hom` as a `continuous_map`. -/
-add_decl_doc continuous_add_monoid_hom.to_continuous_map
+@[priority 100, to_additive] -- See note [lower instance priority]
+instance continuous_monoid_hom_class.to_continuous_map_class [monoid α] [monoid β]
+  [topological_space α] [topological_space β] [continuous_monoid_hom_class F α β] :
+  continuous_map_class F α β :=
+{ .. ‹continuous_monoid_hom_class F α β› }
 
 namespace continuous_monoid_hom
-
-variables {A B C D E}
-
+variables {A B C D E} [monoid α] [monoid β] [topological_space α] [topological_space β]
+
+@[to_additive]
+instance : continuous_monoid_hom_class (continuous_monoid_hom α β) α β :=
+{ coe := λ f, f.to_fun,
+  coe_injective' := λ f g h, by { obtain ⟨⟨_, _⟩, _⟩ := f, obtain ⟨⟨_, _⟩, _⟩ := g, congr' },
+  map_mul := λ f, f.map_mul',
+  map_one := λ f, f.map_one',
+  map_continuous := λ f, f.continuous_to_fun }
+
+/-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
+directly. -/
 @[to_additive] instance : has_coe_to_fun (continuous_monoid_hom A B) (λ _, A → B) :=
-⟨continuous_monoid_hom.to_fun⟩
+fun_like.has_coe_to_fun
 
 @[to_additive] lemma ext {f g : continuous_monoid_hom A B} (h : ∀ x, f x = g x) : f = g :=
-by cases f; cases g; congr; exact funext h
+fun_like.ext _ _ h
+
+/-- Reinterpret a `continuous_monoid_hom` as a `continuous_map`. -/
+@[to_additive "Reinterpret a `continuous_add_monoid_hom` as a `continuous_map`."]
+def to_continuous_map (f : continuous_monoid_hom α β) : C(α, β) := { .. f}
+
+@[to_additive] lemma to_continuous_map_injective : injective (to_continuous_map : _ → C(α, β)) :=
+λ f g h, ext $ by convert fun_like.ext_iff.1 h
 
 /-- Construct a `continuous_monoid_hom` from a `continuous` `monoid_hom`. -/
 @[to_additive "Construct a `continuous_add_monoid_hom` from a `continuous` `add_monoid_hom`.",
   simps]
-def mk' (f : A →* B) (hf : continuous f) : continuous_monoid_hom A B := { .. f }
+def mk' (f : A →* B) (hf : continuous f) : continuous_monoid_hom A B :=
+{ continuous_to_fun := hf, .. f }
 
 /-- Composition of two continuous homomorphisms. -/
 @[to_additive "Composition of two continuous homomorphisms.", simps]
@@ -153,7 +195,7 @@ variables (A B C D E)
 lemma is_inducing : inducing (to_continuous_map : continuous_monoid_hom A B → C(A, B)) := ⟨rfl⟩
 
 lemma is_embedding : embedding (to_continuous_map : continuous_monoid_hom A B → C(A, B)) :=
-⟨is_inducing A B, λ _ _, ext ∘ continuous_map.ext_iff.mp⟩
+⟨is_inducing A B, to_continuous_map_injective⟩
 
 variables {A B C D E}
 

src/topology/category/CompHaus/default.lean

@@ -11,7 +11,6 @@ import category_theory.monad.limits
 import topology.urysohns_lemma
 
 /-!
-
 # The category of Compact Hausdorff Spaces
 
 We construct the category of compact Hausdorff spaces.
@@ -134,7 +133,7 @@ noncomputable def stone_cech_equivalence (X : Top.{u}) (Y : CompHaus.{u}) :
   begin
     rintro ⟨f : (X : Type*) ⟶ Y, hf : continuous f⟩,
     ext,
-    exact congr_fun (stone_cech_extend_extends hf) x,
+    exact congr_fun (stone_cech_extend_extends hf) _,
   end }
 
 /--

src/topology/compact_open.lean

@@ -277,7 +277,7 @@ lemma curry_apply (f : C(α × β, γ)) (a : α) (b : β) : f.curry a b = f (a,
 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
+hf ▸ continuous.comp continuous_ev $ continuous.prod_map f.2 continuous_id
 
 /-- 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
@@ -291,16 +291,16 @@ lemma continuous_uncurry [locally_compact_space α] [locally_compact_space β] :
 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 continuous.comp continuous_ev (continuous.prod_map continuous_ev continuous_id);
   apply_instance
 end
 
 /-- The family of constant maps: `β → C(α, β)` as a continuous map. -/
 def const' : C(β, C(α, β)) := curry ⟨prod.fst, continuous_fst⟩
 
-@[simp] lemma coe_const' : (const' : β → C(α, β)) = const := rfl
+@[simp] lemma coe_const' : (const' : β → C(α, β)) = const α := rfl
 
-lemma continuous_const' : continuous (const : β → C(α, β)) := const'.continuous
+lemma continuous_const' : continuous (const α : β → C(α, β)) := const'.continuous
 
 end curry
 
@@ -323,7 +323,7 @@ def continuous_map_of_unique [unique α] : β ≃ₜ C(α, β) :=
 { to_fun := continuous_map.comp ⟨_, continuous_fst⟩ ∘ coev α β,
   inv_fun := ev α β ∘ (λ f, (f, default)),
   left_inv := λ a, rfl,
-  right_inv := λ f, by { ext, rw unique.eq_default x, refl },
+  right_inv := λ f, by { ext, rw unique.eq_default a, refl },
   continuous_to_fun := continuous.comp (continuous_comp _) continuous_coev,
   continuous_inv_fun :=
     continuous.comp continuous_ev (continuous.prod_mk continuous_id continuous_const) }

src/topology/continuous_function/algebra.lean

@@ -46,23 +46,21 @@ instance has_mul [has_mul β] [has_continuous_mul β] : has_mul C(α, β) :=
 ⟨λ f g, ⟨f * g, continuous_mul.comp (f.continuous.prod_mk g.continuous : _)⟩⟩
 
 @[simp, norm_cast, to_additive]
-lemma coe_mul [has_mul β] [has_continuous_mul β] (f g : C(α, β)) :
-  ((f * g : C(α, β)) : α → β) = (f : α → β) * (g : α → β) := rfl
+lemma coe_mul [has_mul β] [has_continuous_mul β] (f g : C(α, β)) : ⇑(f * g) = f * g := rfl
 
 @[simp, to_additive] lemma mul_comp [has_mul γ] [has_continuous_mul γ]
   (f₁ f₂ : C(β, γ)) (g : C(α, β)) :
   (f₁ * f₂).comp g = f₁.comp g * f₂.comp g :=
 rfl
 
 @[to_additive]
-instance [has_one β] : has_one C(α, β) := ⟨const (1 : β)⟩
+instance [has_one β] : has_one C(α, β) := ⟨const α 1⟩
 
 @[simp, norm_cast, to_additive]
-lemma coe_one [has_one β] : ((1 : C(α, β)) : α → β) = (1 : α → β) := rfl
+lemma coe_one [has_one β]  : ⇑(1 : C(α, β)) = 1 := rfl
+
+@[simp, to_additive] lemma one_comp [has_one γ] (g : C(α, β)) : (1 : C(β, γ)).comp g = 1 := rfl
 
-@[simp, to_additive] lemma one_comp [has_one γ] (g : C(α, β)) :
-  (1 : C(β, γ)).comp g = 1 :=
-rfl
 instance has_nsmul [add_monoid β] [has_continuous_add β] : has_scalar ℕ C(α, β) :=
 ⟨λ n f, ⟨n • f, f.continuous.nsmul n⟩⟩