refactor(topology/instances/add_circle): redefine equiv_add_circle (#17881)

urkud · urkud · commit f178c0e25af3 · 2022-12-10T07:00:46.000Z
Use `quotient_add_group.congr`. Also define `add_aut.mul_left` and `add_aut.mul_right`.
diff --git a/src/algebra/ring/add_aut.lean b/src/algebra/ring/add_aut.lean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import group_theory.group_action.group
+import algebra.module.basic
+
+/-!
+# Multiplication on the left/right as additive automorphisms
+
+In this file we define `add_aut.mul_left` and `add_aut.mul_right`.
+
+See also `add_monoid_hom.mul_left`, `add_monoid_hom.mul_right`, `add_monoid.End.mul_left`, and
+`add_monoid.End.mul_right` for multiplication by `R` as an endomorphism instead of multiplication by
+`Rˣ` as an automorphism.
+-/
+
+namespace add_aut
+variables {R : Type*} [semiring R]
+
+/-- Left multiplication by a unit of a semiring as an additive automorphism. -/
+@[simps { simp_rhs := tt }]
+def mul_left : Rˣ →* add_aut R := distrib_mul_action.to_add_aut _ _
+
+/-- Right multiplication by a unit of a semiring as an additive automorphism. -/
+def mul_right (u : Rˣ) : add_aut R :=
+distrib_mul_action.to_add_aut Rᵐᵒᵖˣ R (units.op_equiv.symm $ mul_opposite.op u)
+
+@[simp] lemma mul_right_apply (u : Rˣ) (x : R) : mul_right u x = x * u := rfl
+@[simp] lemma mul_right_symm_apply (u : Rˣ) (x : R) : (mul_right u).symm x = x * ↑u⁻¹ := rfl
+
+end add_aut
+
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
@@ -2683,6 +2683,10 @@ end ring
 
 end add_subgroup
 
+@[simp, to_additive map_zmultiples] lemma monoid_hom.map_zpowers (f : G →* N) (x : G) :
+  (subgroup.zpowers x).map f = subgroup.zpowers (f x) :=
+by rw [subgroup.zpowers_eq_closure, subgroup.zpowers_eq_closure, f.map_closure, set.image_singleton]
+
 lemma int.mem_zmultiples_iff {a b : ℤ} :
   b ∈ add_subgroup.zmultiples a ↔ a ∣ b :=
 exists_congr (λ k, by rw [mul_comm, eq_comm, ← smul_eq_mul])
diff --git a/src/topology/instances/add_circle.lean b/src/topology/instances/add_circle.lean
@@ -3,6 +3,7 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import algebra.ring.add_aut
 import group_theory.divisible
 import group_theory.order_of_element
 import ring_theory.int.basic
@@ -110,19 +111,11 @@ end linear_ordered_add_comm_group
 section linear_ordered_field
 variables [linear_ordered_field 𝕜] [topological_space 𝕜] [order_topology 𝕜] (p q : 𝕜)
 
-/-- An auxiliary definition used only for constructing `add_circle.equiv_add_circle`. -/
-private def equiv_add_circle_aux (hp : p ≠ 0) : add_circle p →+ add_circle q :=
-quotient_add_group.lift _
-  ((quotient_add_group.mk' (zmultiples q)).comp $ add_monoid_hom.mul_right (p⁻¹ * q))
-  (λ x h, by obtain ⟨z, rfl⟩ := mem_zmultiples_iff.1 h; simp [hp, mul_assoc (z : 𝕜), ← mul_assoc p])
-
 /-- The rescaling equivalence between additive circles with different periods. -/
 def equiv_add_circle (hp : p ≠ 0) (hq : q ≠ 0) : add_circle p ≃+ add_circle q :=
-{ to_fun := equiv_add_circle_aux p q hp,
-  inv_fun := equiv_add_circle_aux q p hq,
-  left_inv := by { rintros ⟨x⟩, show quotient_add_group.mk _ = _, congr, field_simp [hp, hq], },
-  right_inv := by { rintros ⟨x⟩, show quotient_add_group.mk _ = _, congr, field_simp [hp, hq], },
-  .. equiv_add_circle_aux p q hp }
+quotient_add_group.congr _ _ (add_aut.mul_right $ (units.mk0 p hp)⁻¹ * units.mk0 q hq) $
+  by rw [add_monoid_hom.map_zmultiples, add_monoid_hom.coe_coe, add_aut.mul_right_apply,
+    units.coe_mul, units.coe_mk0, units.coe_inv, units.coe_mk0, mul_inv_cancel_left₀ hp]
 
 @[simp] lemma equiv_add_circle_apply_mk (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
   equiv_add_circle p q hp hq (x : 𝕜) = (x * (p⁻¹ * q) : 𝕜) :=
