feat(topology/algebra): add @[to_additive] to some lemmas (#12018)

* rename `embed_product` to `units.embed_product`, add `add_units.embed_product`;
* add additive versions to lemmas about topology on `units M`;
* add `add_opposite.topological_space` and `add_opposite.has_continuous_add`;
* move `continuous_op` and `continuous_unop` to the `mul_opposite` namespace, add additive versions.

src/algebra/group/prod.lean

@@ -345,12 +345,14 @@ end
 
 end mul_equiv
 
-section units
+namespace units
 
 open mul_opposite
 
 /-- Canonical homomorphism of monoids from `αˣ` into `α × αᵐᵒᵖ`.
 Used mainly to define the natural topology of `αˣ`. -/
+@[to_additive "Canonical homomorphism of additive monoids from `add_units α` into `α × αᵃᵒᵖ`.
+Used mainly to define the natural topology of `add_units α`."]
 def embed_product (α : Type*) [monoid α] : αˣ →* α × αᵐᵒᵖ :=
 { to_fun := λ x, ⟨x, op ↑x⁻¹⟩,
   map_one' := by simp only [one_inv, eq_self_iff_true, units.coe_one, op_one, prod.mk_eq_one,

src/topology/algebra/group.lean

@@ -827,12 +827,14 @@ end quotient
 
 namespace units
 
+open mul_opposite (continuous_op continuous_unop)
+
 variables [monoid α] [topological_space α] [has_continuous_mul α] [monoid β] [topological_space β]
   [has_continuous_mul β]
 
-instance : topological_group αˣ :=
-{ continuous_inv := continuous_induced_rng ((continuous_unop.comp (continuous_snd.comp
-    (@continuous_embed_product α _ _))).prod_mk (continuous_op.comp continuous_coe)) }
+@[to_additive] instance : topological_group αˣ :=
+{ continuous_inv := continuous_induced_rng ((continuous_unop.comp
+    (@continuous_embed_product α _ _).snd).prod_mk (continuous_op.comp continuous_coe)) }
 
 /-- The topological group isomorphism between the units of a product of two monoids, and the product
     of the units of each monoid. -/
@@ -842,7 +844,7 @@ def homeomorph.prod_units : homeomorph (α × β)ˣ (αˣ × βˣ) :=
     show continuous (λ i : (α × β)ˣ, (map (monoid_hom.fst α β) i, map (monoid_hom.snd α β) i)),
     refine continuous.prod_mk _ _,
     { refine continuous_induced_rng ((continuous_fst.comp units.continuous_coe).prod_mk _),
-      refine continuous_op.comp (continuous_fst.comp _),
+      refine mul_opposite.continuous_op.comp (continuous_fst.comp _),
       simp_rw units.inv_eq_coe_inv,
       exact units.continuous_coe.comp continuous_inv, },
     { refine continuous_induced_rng ((continuous_snd.comp units.continuous_coe).prod_mk _),

src/topology/algebra/monoid.lean

@@ -379,28 +379,27 @@ lemma continuous_on.pow {f : X → M} {s : set X} (hf : continuous_on f s) (n :
 
 end has_continuous_mul
 
-section op
-
-open mul_opposite
+namespace mul_opposite
 
 /-- Put the same topological space structure on the opposite monoid as on the original space. -/
-instance [_i : topological_space α] : topological_space αᵐᵒᵖ :=
+@[to_additive] instance [_i : topological_space α] : topological_space αᵐᵒᵖ :=
 topological_space.induced (unop : αᵐᵒᵖ → α) _i
 
 variables [topological_space α]
 
-lemma continuous_unop : continuous (unop : αᵐᵒᵖ → α) := continuous_induced_dom
-lemma continuous_op : continuous (op : α → αᵐᵒᵖ) := continuous_induced_rng continuous_id
+@[to_additive] lemma continuous_unop : continuous (unop : αᵐᵒᵖ → α) := continuous_induced_dom
+@[to_additive] lemma continuous_op : continuous (op : α → αᵐᵒᵖ) :=
+continuous_induced_rng continuous_id
 
 variables [monoid α] [has_continuous_mul α]
 
 /-- If multiplication is continuous in the monoid `α`, then it also is in the monoid `αᵐᵒᵖ`. -/
-instance : has_continuous_mul αᵐᵒᵖ :=
+@[to_additive] instance : has_continuous_mul αᵐᵒᵖ :=
 ⟨ let h₁ := @continuous_mul α _ _ _ in
   let h₂ : continuous (λ p : α × α, _) := continuous_snd.prod_mk continuous_fst in
   continuous_induced_rng $ (h₁.comp h₂).comp (continuous_unop.prod_map continuous_unop) ⟩
 
-end op
+end mul_opposite
 
 namespace units
 
@@ -409,13 +408,13 @@ open mul_opposite
 variables [topological_space α] [monoid α]
 
 /-- The units of a monoid are equipped with a topology, via the embedding into `α × α`. -/
-instance : topological_space αˣ :=
+@[to_additive] instance : topological_space αˣ :=
 topological_space.induced (embed_product α) (by apply_instance)
 
-lemma continuous_embed_product : continuous (embed_product α) :=
+@[to_additive] lemma continuous_embed_product : continuous (embed_product α) :=
 continuous_induced_dom
 
-lemma continuous_coe : continuous (coe : αˣ → α) :=
+@[to_additive] lemma continuous_coe : continuous (coe : αˣ → α) :=
 by convert continuous_fst.comp continuous_induced_dom
 
 variables [has_continuous_mul α]
@@ -425,7 +424,7 @@ with respect to the induced topology, is continuous.
 
 Inversion is also continuous, but we register this in a later file, `topology.algebra.group`,
 because the predicate `has_continuous_inv` has not yet been defined. -/
-instance : has_continuous_mul αˣ :=
+@[to_additive] instance : has_continuous_mul αˣ :=
 ⟨ let h := @continuous_mul (α × αᵐᵒᵖ) _ _ _ in
   continuous_induced_rng $ h.comp $ continuous_embed_product.prod_map continuous_embed_product ⟩
 

src/topology/algebra/mul_action.lean

@@ -132,7 +132,7 @@ continuous_smul.comp (continuous_const.prod_mk hg)
 instance has_continuous_smul.op [has_scalar Mᵐᵒᵖ α] [is_central_scalar M α] :
   has_continuous_smul Mᵐᵒᵖ α :=
 ⟨ suffices continuous (λ p : M × α, mul_opposite.op p.fst • p.snd),
-  from this.comp (continuous_unop.prod_map continuous_id),
+  from this.comp (mul_opposite.continuous_unop.prod_map continuous_id),
   by simpa only [op_smul_eq_smul] using (continuous_smul : continuous (λ p : M × α, _)) ⟩
 
 end has_scalar
@@ -141,7 +141,7 @@ section monoid
 
 variables [monoid M] [mul_action M α] [has_continuous_smul M α]
 
-instance units.has_continuous_smul : has_continuous_smul Mˣ α :=
+@[to_additive] instance units.has_continuous_smul : has_continuous_smul Mˣ α :=
 { continuous_smul :=
     show continuous ((λ p : M × α, p.fst • p.snd) ∘ (λ p : Mˣ × α, (p.1, p.2))),
     from continuous_smul.comp ((units.continuous_coe.comp continuous_fst).prod_mk continuous_snd) }