feat(topology/algebra/group): add lemmas about units (#15921)

* add `simps` attribute here and there;
* add `continuous_prod_mk`, `units.continuous_iff`, `units.continuous_inv`, and `continuous.map_units`;
* golf `homeomorph.prod_units`, add additive version;
* drop unused section variables, golf `topological_group_Inf`.

src/algebra/group/prod.lean

@@ -495,7 +495,7 @@ 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 α`."]
+Used mainly to define the natural topology of `add_units α`.", simps]
 def embed_product (α : Type*) [monoid α] : αˣ →* α × αᵐᵒᵖ :=
 { to_fun := λ x, ⟨x, op ↑x⁻¹⟩,
   map_one' := by simp only [inv_one, eq_self_iff_true, units.coe_one, op_one, prod.mk_eq_one,

src/topology/algebra/constructions.lean

@@ -36,16 +36,16 @@ continuous_induced_dom
 @[continuity, to_additive] lemma continuous_op : continuous (op : M → Mᵐᵒᵖ) :=
 continuous_induced_rng.2 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."]
+@[to_additive "`add_opposite.op` as a homeomorphism.", simps]
 def op_homeomorph : M ≃ₜ Mᵐᵒᵖ :=
 { to_equiv := op_equiv,
   continuous_to_fun := continuous_op,
   continuous_inv_fun := continuous_unop }
 
+@[to_additive] instance [t2_space M] : t2_space Mᵐᵒᵖ :=
+op_homeomorph.symm.embedding.t2_space
+
 @[simp, to_additive] lemma map_op_nhds (x : M) : map (op : M → Mᵐᵒᵖ) (𝓝 x) = 𝓝 (op x) :=
 op_homeomorph.map_nhds_eq x
 
@@ -64,7 +64,7 @@ namespace units
 
 open mul_opposite
 
-variables [topological_space M] [monoid M]
+variables [topological_space M] [monoid M] [topological_space X]
 
 /-- The units of a monoid are equipped with a topology, via the embedding into `M × M`. -/
 @[to_additive] instance : topological_space Mˣ :=
@@ -81,4 +81,12 @@ continuous_induced_dom
 @[to_additive] lemma continuous_coe : continuous (coe : Mˣ → M) :=
 (@continuous_embed_product M _ _).fst
 
+@[to_additive] protected lemma continuous_iff {f : X → Mˣ} :
+  continuous f ↔ continuous (coe ∘ f : X → M) ∧ continuous (λ x, ↑(f x)⁻¹ : X → M) :=
+by simp only [inducing_embed_product.continuous_iff, embed_product_apply, (∘), continuous_prod_mk,
+  op_homeomorph.symm.inducing.continuous_iff, op_homeomorph_symm_apply, unop_op]
+
+@[to_additive] lemma continuous_coe_inv : continuous (λ u, ↑u⁻¹ : Mˣ → M) :=
+(units.continuous_iff.1 continuous_id).2
+
 end units

src/topology/algebra/group.lean

@@ -1177,69 +1177,45 @@ namespace units
 
 open mul_opposite (continuous_op continuous_unop)
 
-variables [monoid α] [topological_space α] [has_continuous_mul α] [monoid β] [topological_space β]
-  [has_continuous_mul β]
+variables [monoid α] [topological_space α] [monoid β] [topological_space β]
 
-@[to_additive] instance : topological_group αˣ :=
-{ continuous_inv := continuous_induced_rng.2 ((continuous_unop.comp
-    (@continuous_embed_product α _ _).snd).prod_mk (continuous_op.comp continuous_coe)) }
+@[to_additive] instance [has_continuous_mul α] : topological_group αˣ :=
+{ continuous_inv := units.continuous_iff.2 $ ⟨continuous_coe_inv, continuous_coe⟩ }
 
 /-- The topological group isomorphism between the units of a product of two monoids, and the product
-    of the units of each monoid. -/
-def homeomorph.prod_units : homeomorph (α × β)ˣ (αˣ × βˣ) :=
-{ continuous_to_fun  :=
-  begin
-    show continuous (λ i : (α × β)ˣ, (map (monoid_hom.fst α β) i, map (monoid_hom.snd α β) i)),
-    refine continuous.prod_mk _ _,
-    { refine continuous_induced_rng.2 ((continuous_fst.comp units.continuous_coe).prod_mk _),
-      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.2 ((continuous_snd.comp units.continuous_coe).prod_mk _),
-      simp_rw units.coe_map_inv,
-      exact continuous_op.comp (continuous_snd.comp (units.continuous_coe.comp continuous_inv)), }
-  end,
-  continuous_inv_fun :=
-  begin
-    refine continuous_induced_rng.2 (continuous.prod_mk _ _),
-    { exact (units.continuous_coe.comp continuous_fst).prod_mk
-        (units.continuous_coe.comp continuous_snd), },
-    { refine continuous_op.comp
-        (units.continuous_coe.comp $ continuous_induced_rng.2 $ continuous.prod_mk _ _),
-      { exact (units.continuous_coe.comp (continuous_inv.comp continuous_fst)).prod_mk
-          (units.continuous_coe.comp (continuous_inv.comp continuous_snd)) },
-      { exact continuous_op.comp ((units.continuous_coe.comp continuous_fst).prod_mk
-            (units.continuous_coe.comp continuous_snd)) }}
-  end,
-  ..mul_equiv.prod_units }
+of the units of each monoid. -/
+@[to_additive "The topological group isomorphism between the additive units of a product of two
+additive monoids, and the product of the additive units of each additive monoid."]
+def homeomorph.prod_units : (α × β)ˣ ≃ₜ (αˣ × βˣ) :=
+{ continuous_to_fun  := (continuous_fst.units_map (monoid_hom.fst α β)).prod_mk
+    (continuous_snd.units_map (monoid_hom.snd α β)),
+  continuous_inv_fun := units.continuous_iff.2 ⟨continuous_coe.fst'.prod_mk continuous_coe.snd',
+    continuous_coe_inv.fst'.prod_mk continuous_coe_inv.snd'⟩,
+  to_equiv := mul_equiv.prod_units.to_equiv }
 
 end units
 
 section lattice_ops
 
-variables {ι : Sort*} [group G] [group H]
-  {t : topological_space H} [topological_group H] {F : Type*}
-  [monoid_hom_class F G H] (f : F)
+variables {ι : Sort*} [group G]
 
 @[to_additive] lemma topological_group_Inf {ts : set (topological_space G)}
   (h : ∀ t ∈ ts, @topological_group G t _) :
   @topological_group G (Inf ts) _ :=
-{ continuous_inv := @has_continuous_inv.continuous_inv G (Inf ts) _
-    (@has_continuous_inv_Inf _ _ _
-      (λ t ht, @topological_group.to_has_continuous_inv G t _ (h t ht))),
-  continuous_mul := @has_continuous_mul.continuous_mul G (Inf ts) _
-    (@has_continuous_mul_Inf _ _ _
-      (λ t ht, @topological_group.to_has_continuous_mul G t _ (h t ht))) }
+{ to_has_continuous_inv := @has_continuous_inv_Inf _ _ _ $
+    λ t ht, @topological_group.to_has_continuous_inv G t _ $ h t ht,
+  to_has_continuous_mul := @has_continuous_mul_Inf _ _ _ $
+    λ t ht, @topological_group.to_has_continuous_mul G t _ $ h t ht }
 
 @[to_additive] lemma topological_group_infi {ts' : ι → topological_space G}
   (h' : ∀ i, @topological_group G (ts' i) _) :
   @topological_group G (⨅ i, ts' i) _ :=
-by {rw ← Inf_range, exact topological_group_Inf (set.forall_range_iff.mpr h')}
+by { rw ← Inf_range, exact topological_group_Inf (set.forall_range_iff.mpr h') }
 
 @[to_additive] lemma topological_group_inf {t₁ t₂ : topological_space G}
   (h₁ : @topological_group G t₁ _) (h₂ : @topological_group G t₂ _) :
   @topological_group G (t₁ ⊓ t₂) _ :=
-by {rw inf_eq_infi, refine topological_group_infi (λ b, _), cases b; assumption}
+by { rw inf_eq_infi, refine topological_group_infi (λ b, _), cases b; assumption }
 
 end lattice_ops
 

src/topology/algebra/monoid.lean

@@ -479,6 +479,10 @@ instance : has_continuous_mul αˣ := inducing_embed_product.has_continuous_mul
 
 end units
 
+@[to_additive] lemma continuous.units_map [monoid M] [monoid N] [topological_space M]
+  [topological_space N] (f : M →* N) (hf : continuous f) : continuous (units.map f) :=
+units.continuous_iff.2 ⟨hf.comp units.continuous_coe, hf.comp units.continuous_coe_inv⟩
+
 section
 
 variables [topological_space M] [comm_monoid M]

src/topology/constructions.lean

@@ -303,6 +303,10 @@ hf.comp continuous_at_snd
   (hf : continuous f) (hg : continuous g) : continuous (λx, (f x, g x)) :=
 continuous_inf_rng.2 ⟨continuous_induced_rng.2 hf, continuous_induced_rng.2 hg⟩
 
+@[simp] lemma continuous_prod_mk {f : α → β} {g : α → γ} :
+  continuous (λ x, (f x, g x)) ↔ continuous f ∧ continuous g :=
+⟨λ h, ⟨h.fst, h.snd⟩, λ h, h.1.prod_mk h.2⟩
+
 @[continuity] lemma continuous.prod.mk (a : α) : continuous (λ b : β, (a, b)) :=
 continuous_const.prod_mk continuous_id'