From 7231172eaa3b3436657ad3b58f6cf0af606b20d2 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 25 Apr 2022 11:19:22 +0000
Subject: [PATCH] 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   | 5 +++++
 src/topology/algebra/constructions.lean      | 3 +++
 src/topology/algebra/mul_action.lean         | 4 ++++
 src/topology/algebra/uniform_mul_action.lean | 8 +++++++-
 4 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/topology/algebra/const_mul_action.lean b/src/topology/algebra/const_mul_action.lean
index ce5ad16bd580a..04fb4e45d85d8 100644
--- a/src/topology/algebra/const_mul_action.lean
+++ b/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 (α × β) :=
diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
index 5492a346352d1..d41da27532151 100644
--- a/src/topology/algebra/constructions.lean
+++ b/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ᵐᵒᵖ :=
diff --git a/src/topology/algebra/mul_action.lean b/src/topology/algebra/mul_action.lean
index abbcdb4eca379..4f250aa67ba1a 100644
--- a/src/topology/algebra/mul_action.lean
+++ b/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
diff --git a/src/topology/algebra/uniform_mul_action.lean b/src/topology/algebra/uniform_mul_action.lean
index 3079e25a568a8..6ea1087b57641 100644
--- a/src/topology/algebra/uniform_mul_action.lean
+++ b/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