feat(topology/algebra): actions on the opposite type are continuous (#…

…13671)

This also adds the missing `t2_space` instance.

src/topology/algebra/const_mul_action.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Alex Kontorovich, Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Kontorovich, Heather Macbeth
 -/
+import topology.algebra.constructions
 import topology.homeomorph
 import group_theory.group_action.basic
 /-!
@@ -99,6 +100,10 @@ instance has_continuous_const_smul.op [has_scalar Mᵐᵒᵖ α] [is_central_sca
   has_continuous_const_smul Mᵐᵒᵖ α :=
 ⟨ mul_opposite.rec $ λ c, by simpa only [op_smul_eq_smul] using continuous_const_smul c ⟩
 
+@[to_additive] instance mul_opposite.has_continuous_const_smul :
+  has_continuous_const_smul M αᵐᵒᵖ :=
+⟨λ c, mul_opposite.continuous_op.comp $ mul_opposite.continuous_unop.const_smul c⟩
+
 @[to_additive]
 instance [has_scalar M β] [has_continuous_const_smul M β] :
   has_continuous_const_smul M (α × β) :=

src/topology/algebra/constructions.lean

@@ -36,6 +36,9 @@ continuous_induced_dom
 @[continuity, to_additive] lemma continuous_op : continuous (op : M → Mᵐᵒᵖ) :=
 continuous_induced_rng continuous_id
 
+@[to_additive] instance [t2_space M] : t2_space Mᵐᵒᵖ :=
+⟨λ x y h, separated_by_continuous mul_opposite.continuous_unop $ unop_injective.ne h⟩
+
 /-- `mul_opposite.op` as a homeomorphism. -/
 @[to_additive "`add_opposite.op` as a homeomorphism."]
 def op_homeomorph : M ≃ₜ Mᵐᵒᵖ :=

src/topology/algebra/mul_action.lean

@@ -110,6 +110,10 @@ instance has_continuous_smul.op [has_scalar Mᵐᵒᵖ X] [is_central_scalar M X
   from this.comp (mul_opposite.continuous_unop.prod_map continuous_id),
   by simpa only [op_smul_eq_smul] using (continuous_smul : continuous (λ p : M × X, _)) ⟩
 
+@[to_additive] instance mul_opposite.has_continuous_smul : has_continuous_smul M Xᵐᵒᵖ :=
+⟨mul_opposite.continuous_op.comp $ continuous_smul.comp $
+  continuous_id.prod_map mul_opposite.continuous_unop⟩
+
 end has_scalar
 
 section monoid

src/topology/algebra/uniform_mul_action.lean

@@ -42,7 +42,9 @@ instance has_uniform_continuous_const_smul.to_has_continuous_const_smul
   [has_uniform_continuous_const_smul M X] : has_continuous_const_smul M X :=
 ⟨λ c, (uniform_continuous_const_smul c).continuous⟩
 
-lemma uniform_continuous.const_smul [has_uniform_continuous_const_smul M X]
+variables {M X Y}
+
+@[to_additive] lemma uniform_continuous.const_smul [has_uniform_continuous_const_smul M X]
   {f : Y → X} (hf : uniform_continuous f) (c : M) :
   uniform_continuous (c • f) :=
 (uniform_continuous_const_smul c).comp hf
@@ -57,6 +59,10 @@ instance has_uniform_continuous_const_smul.op [has_scalar Mᵐᵒᵖ X] [is_cent
   exact uniform_continuous_const_smul c,
 end⟩
 
+@[to_additive] instance mul_opposite.has_uniform_continuous_const_smul
+  [has_uniform_continuous_const_smul M X] : has_uniform_continuous_const_smul M Xᵐᵒᵖ :=
+⟨λ c, mul_opposite.uniform_continuous_op.comp $ mul_opposite.uniform_continuous_unop.const_smul c⟩
+
 end has_scalar
 
 @[to_additive] instance uniform_group.to_has_uniform_continuous_const_smul