feat(GroupTheory/Torsion): the torsion subgroup is preserved by isomorphisms (leanprover-community#38721)

This PR proves that the torsion subgroup is preserved by isomorphisms.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/GroupTheory/Torsion.lean

@@ -313,6 +313,8 @@ subgroup as a submonoid. -/]
 theorem torsion_eq_torsion_submonoid : CommMonoid.torsion G = (torsion G).toSubmonoid :=
   rfl
 
+variable {G}
+
 @[to_additive]
 theorem mem_torsion (g : G) : g ∈ torsion G ↔ IsOfFinOrder g := Iff.rfl
 
@@ -325,10 +327,26 @@ lemma isMulTorsionFree_iff_torsion_eq_bot : IsMulTorsionFree G ↔ CommGroup.tor
   rw [isMulTorsionFree_iff_not_isOfFinOrder, eq_bot_iff, SetLike.le_def]
   simp [not_imp_not, CommGroup.mem_torsion]
 
+@[to_additive]
+lemma comap_torsion_of_injective {f : G →* H} (hf : Function.Injective f) :
+    (torsion H).comap f = torsion G := by
+  ext x
+  exact hf.isOfFinOrder_iff
+
+@[to_additive]
+lemma _root_.MulEquiv.comap_torsion (e : G ≃* H) : (torsion H).comap e = torsion G :=
+  comap_torsion_of_injective e.injective
+
+@[to_additive]
+lemma _root_.MulEquiv.map_torsion (e : G ≃* H) : (torsion G).map e = torsion H := by
+  rw [Subgroup.map_equiv_eq_comap_symm, e.symm.comap_torsion]
+
 @[to_additive]
 lemma torsion_prod : torsion (G × H) = (torsion G).prod (torsion H) := by
   simp [Subgroup.ext_iff, Subgroup.mem_prod, mem_torsion, IsOfFinOrder.prod_iff]
 
+variable (G)
+
 @[to_additive]
 lemma isTorsion_quotient_range_powMonoidHom {n : ℕ} (hn : n ≠ 0) :
     Monoid.IsTorsion (G ⧸ (powMonoidHom (α := G) n).range) := by

Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

@@ -906,7 +906,7 @@ theorem NumberField.Units.dvd_torsionOrder_of_isPrimitiveRoot [NeZero n] [Number
   convert! orderOf_dvd_natCard (⟨(hζ.isUnit (NeZero.ne n)).unit, ?_⟩ : torsion K)
   · rw [Subgroup.orderOf_mk]
     exact hζ.eq_orderOf
-  · refine (CommGroup.mem_torsion _ _).mpr ⟨n, NeZero.pos n, ?_⟩
+  · refine (CommGroup.mem_torsion _).mpr ⟨n, NeZero.pos n, ?_⟩
     rw [isPeriodicPt_mul_iff_pow_eq_one]
     exact hζ.pow_eq_one
 

Mathlib/NumberTheory/NumberField/Cyclotomic/Three.lean

@@ -62,7 +62,7 @@ theorem Units.mem [NumberField K] [IsCyclotomicExtension {3} ℚ K] :
     congr
     rw [Finset.univ_eq_empty_iff, hrank]
     infer_instance
-  obtain ⟨n, hnpos, hn⟩ := isOfFinOrder_iff_pow_eq_one.1 <| (CommGroup.mem_torsion _ _).1 x.2
+  obtain ⟨n, hnpos, hn⟩ := isOfFinOrder_iff_pow_eq_one.1 <| (CommGroup.mem_torsion _).1 x.2
   replace hn : (↑u : K) ^ ((⟨n, hnpos⟩ : ℕ+) : ℕ) = 1 := by
     rw [← map_pow]
     convert! map_one (algebraMap (𝓞 K) K)

Mathlib/NumberTheory/NumberField/Units/Basic.lean

@@ -238,7 +238,7 @@ theorem torsion_eq_one_or_neg_one_of_odd_finrank
     linarith [IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt hc (IsPrimitiveRoot.orderOf (x.1 : K)),
         NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank h]
   · interval_cases hi : orderOf (x : (𝓞 K)ˣ)
-    · linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion _ x.1).1 x.2)]
+    · linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion x.1).1 x.2)]
     · exact Or.intro_left _ (orderOf_eq_one_iff.1 hi)
     · rw [← orderOf_units, CharP.orderOf_eq_two_iff 0 (by decide)] at hi
       simp [← Units.val_inj, ← Units.val_inj, Units.val_neg, Units.val_one, hi]