fix(topology/algebra/group_completion): add lemmas about nsmul and zs…

…mul and fix diamonds (#14846)

This prevents a diamond forming between `uniform_space.completion.has_scalar` and the default `add_monoid.nsmul` and `sub_neg_monoid.zsmul` fields; by manually defining the latter to match the former.

To do this, we add two new instances of `has_uniform_continuous_smul` for nat- and int- actions.

To use the existing scalar actions, we had to shuffle the imports around a bit.

src/analysis/normed_space/completion.lean

@@ -32,7 +32,7 @@ instance : normed_space 𝕜 (completion E) :=
   norm_smul_le := λ c x, induction_on x
     (is_closed_le (continuous_const_smul _).norm (continuous_const.mul continuous_norm)) $
     λ y, by simp only [← coe_smul, norm_coe, norm_smul],
-  .. completion.module 𝕜 E }
+  .. completion.module }
 
 variables {𝕜 E}
 

src/topology/algebra/group_completion.lean

@@ -5,6 +5,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 import algebra.hom.group_instances
 import topology.algebra.uniform_group
+import topology.algebra.uniform_mul_action
 import topology.uniform_space.completion
 
 /-!
@@ -30,11 +31,11 @@ the main constructions deal with continuous group morphisms.
 
 noncomputable theory
 
-universes u v
+variables {M R α β : Type*}
 
 section group
 open uniform_space Cauchy filter set
-variables {α : Type u} [uniform_space α]
+variables [uniform_space α]
 
 instance [has_zero α] : has_zero (completion α) := ⟨(0 : α)⟩
 instance [has_neg α] : has_neg (completion α) := ⟨completion.map (λa, -a : α → α)⟩
@@ -46,9 +47,23 @@ lemma uniform_space.completion.coe_zero [has_zero α] : ((0 : α) : completion 
 end group
 
 namespace uniform_space.completion
+open uniform_space
+
+section has_zero
+
+instance [uniform_space α] [monoid_with_zero M] [has_zero α] [mul_action_with_zero M α]
+  [has_uniform_continuous_const_smul M α] :
+  mul_action_with_zero M (completion α) :=
+{ smul := (•),
+  smul_zero := λ r, by rw [← coe_zero, ← coe_smul, mul_action_with_zero.smul_zero r],
+  zero_smul := ext' (continuous_const_smul _) continuous_const $ λ a,
+    by rw [← coe_smul, zero_smul, coe_zero],
+  .. completion.mul_action M α }
+
+end has_zero
+
 section uniform_add_group
-open uniform_space uniform_space.completion
-variables {α : Type*} [uniform_space α] [add_group α] [uniform_add_group α]
+variables [uniform_space α] [add_group α] [uniform_add_group α]
 
 @[norm_cast]
 lemma coe_neg (a : α) : ((- a : α) : completion α) = - a :=
@@ -80,13 +95,30 @@ instance : add_monoid (completion α) :=
           (continuous_snd.comp continuous_snd))))
     (assume a b c, show (a : completion α) + b + c = a + (b + c),
       by repeat { rw_mod_cast add_assoc }),
-  .. completion.has_zero, .. completion.has_neg, ..completion.has_add, .. completion.has_sub }
+  nsmul := (•),
+  nsmul_zero' := λ a, completion.induction_on a (is_closed_eq continuous_map continuous_const)
+    (λ a, by rw [←coe_smul, ←coe_zero, zero_smul]),
+  nsmul_succ' := λ n a, completion.induction_on a
+    (is_closed_eq continuous_map $ continuous_map₂ continuous_id continuous_map)
+    (λ a, by rw_mod_cast succ_nsmul ),
+  .. completion.has_zero, ..completion.has_add, }
 
 instance : sub_neg_monoid (completion α) :=
 { sub_eq_add_neg := λ a b, completion.induction_on₂ a b
     (is_closed_eq (continuous_map₂ continuous_fst continuous_snd)
       (continuous_map₂ continuous_fst (completion.continuous_map.comp continuous_snd)))
    (λ a b, by exact_mod_cast congr_arg coe (sub_eq_add_neg a b)),
+  zsmul := (•),
+  zsmul_zero' := λ a, completion.induction_on a (is_closed_eq continuous_map continuous_const)
+    (λ a, by { rw_mod_cast zero_smul, refl} ),
+  zsmul_succ' := λ n a, completion.induction_on a
+    (is_closed_eq continuous_map $ continuous_map₂ continuous_id continuous_map)
+    (λ a, by rw_mod_cast (show int.of_nat n.succ • a = a + int.of_nat n • a,
+                          from sub_neg_monoid.zsmul_succ' n a) ),
+  zsmul_neg' := λ n a, completion.induction_on a
+    (is_closed_eq continuous_map $ completion.continuous_map.comp continuous_map)
+    (λ a, by rw [←coe_smul, ←coe_smul, ←coe_neg, show -[1+ n] • a = -((n.succ : ℤ) • a),
+                                                 from sub_neg_monoid.zsmul_neg' n a]),
   .. completion.add_monoid, .. completion.has_neg, .. completion.has_sub }
 
 instance : add_group (completion α) :=
@@ -98,6 +130,16 @@ instance : add_group (completion α) :=
 instance : uniform_add_group (completion α) :=
 ⟨uniform_continuous_map₂ has_sub.sub⟩
 
+instance {M} [monoid M] [distrib_mul_action M α] [has_uniform_continuous_const_smul M α] :
+  distrib_mul_action M (completion α) :=
+{ smul := (•),
+  smul_add := λ r x y, induction_on₂ x y
+    (is_closed_eq ((continuous_fst.add continuous_snd).const_smul _)
+      ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
+    (λ a b, by simp only [← coe_add, ← coe_smul, smul_add]),
+  smul_zero := λ r, by rw [← coe_zero, ← coe_smul, smul_zero r],
+  .. completion.mul_action M α }
+
 /-- The map from a group to its completion as a group hom. -/
 @[simps] def to_compl : α →+ completion α :=
 { to_fun := coe,
@@ -107,23 +149,32 @@ instance : uniform_add_group (completion α) :=
 lemma continuous_to_compl : continuous (to_compl : α → completion α) :=
 continuous_coe α
 
-variables {β : Type v} [uniform_space β] [add_group β] [uniform_add_group β]
+end uniform_add_group
+
+section uniform_add_comm_group
+variables [uniform_space α] [add_comm_group α] [uniform_add_group α]
 
-instance {α : Type u} [uniform_space α] [add_comm_group α] [uniform_add_group α] :
-  add_comm_group (completion α) :=
+instance : add_comm_group (completion α) :=
 { add_comm  := assume a b, completion.induction_on₂ a b
     (is_closed_eq (continuous_map₂ continuous_fst continuous_snd)
       (continuous_map₂ continuous_snd continuous_fst))
     (assume x y, by { change ↑x + ↑y = ↑y + ↑x, rw [← coe_add, ← coe_add, add_comm]}),
   .. completion.add_group }
 
-end uniform_add_group
+instance [semiring R] [module R α] [has_uniform_continuous_const_smul R α] :
+  module R (completion α) :=
+{ smul := (•),
+  add_smul := λ a b, ext' (continuous_const_smul _)
+    ((continuous_const_smul _).add (continuous_const_smul _)) $ λ x, by { norm_cast, rw add_smul },
+  .. completion.distrib_mul_action, .. completion.mul_action_with_zero }
+
+end uniform_add_comm_group
 
 end uniform_space.completion
 
 section add_monoid_hom
-variables {α β : Type*} [uniform_space α] [add_group α] [uniform_add_group α]
-                        [uniform_space β] [add_group β] [uniform_add_group β]
+variables [uniform_space α] [add_group α] [uniform_add_group α]
+          [uniform_space β] [add_group β] [uniform_add_group β]
 
 open uniform_space uniform_space.completion
 

src/topology/algebra/uniform_group.lean

@@ -79,6 +79,26 @@ by simp * at *
 @[to_additive] lemma uniform_continuous_mul : uniform_continuous (λp:α×α, p.1 * p.2) :=
 uniform_continuous_fst.mul uniform_continuous_snd
 
+@[to_additive uniform_continuous.const_nsmul]
+lemma uniform_continuous.pow_const [uniform_space β] {f : β → α}
+  (hf : uniform_continuous f) : ∀ n : ℕ, uniform_continuous (λ x, f x ^ n)
+| 0 := by { simp_rw pow_zero, exact uniform_continuous_const }
+| (n + 1) := by { simp_rw pow_succ, exact hf.mul (uniform_continuous.pow_const n) }
+
+@[to_additive uniform_continuous_const_nsmul] lemma uniform_continuous_pow_const (n : ℕ) :
+  uniform_continuous (λx:α, x ^ n) :=
+uniform_continuous_id.pow_const n
+
+@[to_additive uniform_continuous.const_zsmul]
+lemma uniform_continuous.zpow_const [uniform_space β] {f : β → α}
+  (hf : uniform_continuous f) : ∀ n : ℤ, uniform_continuous (λ x, f x ^ n)
+| (n : ℕ) := by { simp_rw zpow_coe_nat, exact hf.pow_const _, }
+| -[1+ n] := by { simp_rw zpow_neg_succ_of_nat, exact (hf.pow_const _).inv }
+
+@[to_additive uniform_continuous_const_zsmul] lemma uniform_continuous_zpow_const (n : ℤ) :
+  uniform_continuous (λx:α, x ^ n) :=
+uniform_continuous_id.zpow_const n
+
 @[priority 10, to_additive]
 instance uniform_group.to_topological_group : topological_group α :=
 { continuous_mul := uniform_continuous_mul.continuous,

src/topology/algebra/uniform_mul_action.lean

@@ -3,15 +3,21 @@ Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
-import topology.algebra.group_completion
+import algebra.hom.group_instances
+import topology.algebra.uniform_group
+import topology.uniform_space.completion
 
 /-!
 # Multiplicative action on the completion of a uniform space
 
 In this file we define typeclasses `has_uniform_continuous_const_vadd` and
 `has_uniform_continuous_const_smul` and prove that a multiplicative action on `X` with uniformly
-continuous `(•) c` can be extended to a multiplicative action on `uniform_space.completion X`. We
-also provide similar instances `distrib_mul_action`, `mul_action_with_zero`, and `module`.
+continuous `(•) c` can be extended to a multiplicative action on `uniform_space.completion X`.
+
+In later files once the additive group structure is set up, we provide
+* `uniform_space.completion.distrib_mul_action`
+* `uniform_space.completion.mul_action_with_zero`
+* `uniform_space.completion.module`
 -/
 
 universes u v w x y z
@@ -33,6 +39,14 @@ class has_uniform_continuous_const_smul [uniform_space X] [has_scalar M X] : Pro
 export has_uniform_continuous_const_vadd (uniform_continuous_const_vadd)
   has_uniform_continuous_const_smul (uniform_continuous_const_smul)
 
+instance add_monoid.has_uniform_continuous_const_smul_nat [add_group X] [uniform_add_group X] :
+  has_uniform_continuous_const_smul ℕ X :=
+⟨uniform_continuous_const_nsmul⟩
+
+instance add_group.has_uniform_continuous_const_smul_int [add_group X] [uniform_add_group X] :
+  has_uniform_continuous_const_smul ℤ X :=
+⟨uniform_continuous_const_zsmul⟩
+
 section has_scalar
 
 variable [has_scalar M X]
@@ -102,33 +116,6 @@ end has_scalar
   mul_smul := λ x y, ext' (continuous_const_smul _) ((continuous_const_smul _).const_smul _) $
     λ a, by simp only [← coe_smul, mul_smul] }
 
-instance [monoid_with_zero M] [has_zero X] [mul_action_with_zero M X]
-  [has_uniform_continuous_const_smul M X] :
-  mul_action_with_zero M (completion X) :=
-{ smul := (•),
-  smul_zero := λ r, by rw [← coe_zero, ← coe_smul, mul_action_with_zero.smul_zero r],
-  zero_smul := ext' (continuous_const_smul _) continuous_const $ λ a,
-    by rw [← coe_smul, zero_smul, coe_zero],
-  .. completion.mul_action M X }
-
-instance [monoid M] [add_group N] [distrib_mul_action M N] [uniform_space N]
-  [uniform_add_group N] [has_uniform_continuous_const_smul M N] :
-  distrib_mul_action M (completion N) :=
-{ smul := (•),
-  smul_add := λ r x y, induction_on₂ x y
-    (is_closed_eq ((continuous_fst.add continuous_snd).const_smul _)
-      ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
-    (λ a b, by simp only [← coe_add, ← coe_smul, smul_add]),
-  smul_zero := λ r, by rw [← coe_zero, ← coe_smul, smul_zero r],
-  .. completion.mul_action M N }
-
-instance [semiring R] [add_comm_group M] [module R M] [uniform_space M] [uniform_add_group M]
-  [has_uniform_continuous_const_smul R M] : module R (completion M) :=
-{ smul := (•),
-  add_smul := λ a b, ext' (continuous_const_smul _)
-    ((continuous_const_smul _).add (continuous_const_smul _)) $ λ x, by { norm_cast, rw add_smul },
-  .. completion.distrib_mul_action R M, .. completion.mul_action_with_zero R M }
-
 end completion
 
 end uniform_space