feat(topology/continuous_function/algebra): generalize algebra instan…

…ces (#12055)

This adds:
* some missing instances in the algebra hierarchy (`comm_semigroup`, `mul_one_class`, `mul_zero_class`, `monoid_with_zero`, `comm_monoid_with_zero`, `comm_semiring`).
* finer-grained scalar action instances, notably none of which require `topological_space R` any more, as they only need `has_continuous_const_smul R M` instead of `has_continuous_smul R M`.
* continuity lemmas about `zpow` on groups and `zsmul` on additive groups (copied directly from the lemmas about `pow` on monoids), which are used to avoid diamonds in the int-action. In order to make room for these, the lemmas about `zpow` on groups with zero have been renamed to `zpow₀`, which is consistent with how the similar clash with `inv` is solved.
* a few lemmas about `mk_of_compact` since an existing proof was broken by `refl` closing the goal earlier than before.

src/analysis/fourier.lean

@@ -85,7 +85,7 @@ section monomials
 continuous maps from `circle` to `ℂ`. -/
 @[simps] def fourier (n : ℤ) : C(circle, ℂ) :=
 { to_fun := λ z, z ^ n,
-  continuous_to_fun := continuous_subtype_coe.zpow n $ λ z, or.inl (ne_zero_of_mem_circle z) }
+  continuous_to_fun := continuous_subtype_coe.zpow₀ n $ λ z, or.inl (ne_zero_of_mem_circle z) }
 
 @[simp] lemma fourier_zero {z : circle} : fourier 0 z = 1 := rfl
 

src/analysis/special_functions/integrals.lean

@@ -46,7 +46,7 @@ lemma interval_integrable_pow : interval_integrable (λ x, x^n) μ a b :=
 
 lemma interval_integrable_zpow {n : ℤ} (h : 0 ≤ n ∨ (0 : ℝ) ∉ [a, b]) :
   interval_integrable (λ x, x ^ n) μ a b :=
-(continuous_on_id.zpow n $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
+(continuous_on_id.zpow₀ n $ λ x hx, h.symm.imp (ne_of_mem_of_not_mem hx) id).interval_integrable
 
 lemma interval_integrable_rpow {r : ℝ} (h : 0 ≤ r ∨ (0 : ℝ) ∉ [a, b]) :
   interval_integrable (λ x, x ^ r) μ a b :=

src/analysis/specific_limits.lean

@@ -101,7 +101,7 @@ end
 @[simp] lemma continuous_at_zpow {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {m : ℤ} {x : 𝕜} :
   continuous_at (λ x, x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m :=
 begin
-  refine ⟨_, continuous_at_zpow _ _⟩,
+  refine ⟨_, continuous_at_zpow₀ _ _⟩,
   contrapose!, rintro ⟨rfl, hm⟩ hc,
   exact not_tendsto_at_top_of_tendsto_nhds (hc.tendsto.mono_left nhds_within_le_nhds).norm
       (tendsto_norm_zpow_nhds_within_0_at_top hm)

src/measure_theory/integral/circle_integral.lean

@@ -260,7 +260,7 @@ begin
     refine (zpow_strict_anti this.1 this.2).le_iff_le.2 (int.lt_add_one_iff.1 _), exact hn },
   { rintro (rfl|H),
     exacts [circle_integrable_zero_radius,
-      ((continuous_on_id.sub continuous_on_const).zpow _ $ λ z hz, H.symm.imp_left $
+      ((continuous_on_id.sub continuous_on_const).zpow₀ _ $ λ z hz, H.symm.imp_left $
         λ hw, sub_ne_zero.2 $ ne_of_mem_of_not_mem hz hw).circle_integrable'] },
 end
 

src/topology/algebra/group.lean

@@ -250,6 +250,48 @@ hf.inv
 lemma is_compact.inv {s : set G} (hs : is_compact s) : is_compact (s⁻¹) :=
 by { rw [← image_inv], exact hs.image continuous_inv }
 
+section zpow
+
+@[continuity, to_additive]
+lemma continuous_zpow : ∀ z : ℤ, continuous (λ a : G, a ^ z)
+| (int.of_nat n) := by simpa using continuous_pow n
+| -[1+n] := by simpa using (continuous_pow (n + 1)).inv
+
+@[continuity, to_additive]
+lemma continuous.zpow {f : α → G} (h : continuous f) (z : ℤ) :
+  continuous (λ b, (f b) ^ z) :=
+(continuous_zpow z).comp h
+
+@[to_additive]
+lemma continuous_on_zpow {s : set G} (z : ℤ) : continuous_on (λ x, x ^ z) s :=
+(continuous_zpow z).continuous_on
+
+@[to_additive]
+lemma continuous_at_zpow (x : G) (z : ℤ) : continuous_at (λ x, x ^ z) x :=
+(continuous_zpow z).continuous_at
+
+@[to_additive]
+lemma filter.tendsto.zpow {α} {l : filter α} {f : α → G} {x : G} (hf : tendsto f l (𝓝 x)) (z : ℤ) :
+  tendsto (λ x, f x ^ z) l (𝓝 (x ^ z)) :=
+(continuous_at_zpow _ _).tendsto.comp hf
+
+@[to_additive]
+lemma continuous_within_at.zpow {f : α → G} {x : α} {s : set α} (hf : continuous_within_at f s x)
+  (z : ℤ) : continuous_within_at (λ x, f x ^ z) s x :=
+hf.zpow z
+
+@[to_additive]
+lemma continuous_at.zpow {f : α → G} {x : α} (hf : continuous_at f x) (z : ℤ) :
+  continuous_at (λ x, f x ^ z) x :=
+hf.zpow z
+
+@[to_additive continuous_on.zsmul]
+lemma continuous_on.zpow {f : α → G} {s : set α} (hf : continuous_on f s) (z : ℤ) :
+  continuous_on (λ x, f x ^ z) s :=
+λ x hx, (hf x hx).zpow z
+
+end zpow
+
 section ordered_comm_group
 
 variables [topological_space H] [ordered_comm_group H] [topological_group H]

src/topology/algebra/group_with_zero.lean

@@ -235,7 +235,7 @@ section zpow
 variables [group_with_zero G₀] [topological_space G₀] [has_continuous_inv₀ G₀]
   [has_continuous_mul G₀]
 
-lemma continuous_at_zpow (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : continuous_at (λ x, x ^ m) x :=
+lemma continuous_at_zpow₀ (x : G₀) (m : ℤ) (h : x ≠ 0 ∨ 0 ≤ m) : continuous_at (λ x, x ^ m) x :=
 begin
   cases m,
   { simpa only [zpow_of_nat] using continuous_at_pow x m },
@@ -244,30 +244,30 @@ begin
     exact (continuous_at_pow x (m + 1)).inv₀ (pow_ne_zero _ hx) }
 end
 
-lemma continuous_on_zpow (m : ℤ) : continuous_on (λ x : G₀, x ^ m) {0}ᶜ :=
-λ x hx, (continuous_at_zpow _ _ (or.inl hx)).continuous_within_at
+lemma continuous_on_zpow₀ (m : ℤ) : continuous_on (λ x : G₀, x ^ m) {0}ᶜ :=
+λ x hx, (continuous_at_zpow₀ _ _ (or.inl hx)).continuous_within_at
 
-lemma filter.tendsto.zpow {f : α → G₀} {l : filter α} {a : G₀} (hf : tendsto f l (𝓝 a)) (m : ℤ)
+lemma filter.tendsto.zpow₀ {f : α → G₀} {l : filter α} {a : G₀} (hf : tendsto f l (𝓝 a)) (m : ℤ)
   (h : a ≠ 0 ∨ 0 ≤ m) :
   tendsto (λ x, (f x) ^ m) l (𝓝 (a ^ m)) :=
-(continuous_at_zpow _ m h).tendsto.comp hf
+(continuous_at_zpow₀ _ m h).tendsto.comp hf
 
 variables {X : Type*} [topological_space X] {a : X} {s : set X} {f : X → G₀}
 
-lemma continuous_at.zpow (hf : continuous_at f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
+lemma continuous_at.zpow₀ (hf : continuous_at f a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
   continuous_at (λ x, (f x) ^ m) a :=
-hf.zpow m h
+hf.zpow₀ m h
 
-lemma continuous_within_at.zpow (hf : continuous_within_at f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
+lemma continuous_within_at.zpow₀ (hf : continuous_within_at f s a) (m : ℤ) (h : f a ≠ 0 ∨ 0 ≤ m) :
   continuous_within_at (λ x, f x ^ m) s a :=
-hf.zpow m h
+hf.zpow₀ m h
 
-lemma continuous_on.zpow (hf : continuous_on f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) :
+lemma continuous_on.zpow₀ (hf : continuous_on f s) (m : ℤ) (h : ∀ a ∈ s, f a ≠ 0 ∨ 0 ≤ m) :
   continuous_on (λ x, f x ^ m) s :=
-λ a ha, (hf a ha).zpow m (h a ha)
+λ a ha, (hf a ha).zpow₀ m (h a ha)
 
-@[continuity] lemma continuous.zpow (hf : continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) :
+@[continuity] lemma continuous.zpow₀ (hf : continuous f) (m : ℤ) (h0 : ∀ a, f a ≠ 0 ∨ 0 ≤ m) :
   continuous (λ x, (f x) ^ m) :=
-continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).zpow m (h0 x)
+continuous_iff_continuous_at.2 $ λ x, (hf.tendsto x).zpow₀ m (h0 x)
 
 end zpow

src/topology/category/Top/basic.lean

@@ -26,7 +26,7 @@ def Top : Type (u+1) := bundled topological_space
 namespace Top
 
 instance bundled_hom : bundled_hom @continuous_map :=
-⟨@continuous_map.to_fun, @continuous_map.id, @continuous_map.comp, @continuous_map.coe_inj⟩
+⟨@continuous_map.to_fun, @continuous_map.id, @continuous_map.comp, @continuous_map.coe_injective⟩
 
 attribute [derive [large_category, concrete_category]] Top
 

src/topology/category/Top/limits.lean

@@ -56,8 +56,8 @@ def limit_cone_infi (F : J ⥤ Top.{u}) : cone F :=
   π :=
   { app := λ j, ⟨(types.limit_cone (F ⋙ forget)).π.app j,
                  continuous_iff_le_induced.mpr (infi_le _ _)⟩,
-    naturality' := λ j j' f,
-                   continuous_map.coe_inj ((types.limit_cone (F ⋙ forget)).π.naturality f) } }
+    naturality' := λ j j' f, continuous_map.coe_injective
+      ((types.limit_cone (F ⋙ forget)).π.naturality f) } }
 
 /--
 The chosen cone `Top.limit_cone F` for a functor `F : J ⥤ Top` is a limit cone.
@@ -100,8 +100,8 @@ def colimit_cocone (F : J ⥤ Top.{u}) : cocone F :=
   ι :=
   { app := λ j, ⟨(types.colimit_cocone (F ⋙ forget)).ι.app j,
                  continuous_iff_coinduced_le.mpr (le_supr _ j)⟩,
-    naturality' := λ j j' f,
-                   continuous_map.coe_inj ((types.colimit_cocone (F ⋙ forget)).ι.naturality f) } }
+    naturality' := λ j j' f, continuous_map.coe_injective
+      ((types.colimit_cocone (F ⋙ forget)).ι.naturality f) } }
 
 /--
 The chosen cocone `Top.colimit_cocone F` for a functor `F : J ⥤ Top` is a colimit cocone.