refactor(GroupTheory/Torsion): make primaryComponent total (#39484)

Change `primaryComponent` to the `IsPGroup`-style `{g | ∃ k, g ^ p ^ k = 1}`, making the definitions total over `p : ℕ` without requiring `[Fact p.Prime]`.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: rosborn

Mathlib/GroupTheory/Torsion.lean

@@ -56,22 +56,22 @@ def IsTorsion :=
   ∀ g : G, IsOfFinOrder g
 
 /-- A monoid is not a torsion monoid if it has an element of infinite order. -/
-@[to_additive (attr := simp) /-- An additive monoid is not a torsion monoid if it
-  has an element of infinite order. -/]
-theorem not_isTorsion_iff : ¬IsTorsion G ↔ ∃ g : G, ¬IsOfFinOrder g := by
-  rw [IsTorsion, not_forall]
+@[to_additive (attr := simp)
+/-- An additive monoid is not a torsion monoid if it has an element of infinite order. -/]
+theorem not_isTorsion_iff : ¬IsTorsion G ↔ ∃ g : G, ¬IsOfFinOrder g :=
+  not_forall
 
 end Monoid
 
 open Monoid
 
 /-- Torsion monoids are really groups. -/
 @[to_additive (attr := implicit_reducible)
-  /-- Torsion additive monoids are really additive groups -/]
+/-- Torsion additive monoids are really additive groups -/]
 noncomputable def IsTorsion.group [Monoid G] (tG : IsTorsion G) : Group G :=
   { ‹Monoid G› with
-    inv := fun g => g ^ (orderOf g - 1)
-    inv_mul_cancel := fun g => by
+    inv g := g ^ (orderOf g - 1)
+    inv_mul_cancel g := by
       rw [← pow_succ, tsub_add_cancel_of_le, pow_orderOf_eq_one]
       exact (tG g).orderOf_pos }
 
@@ -81,51 +81,50 @@ variable [Group G] {N : Subgroup G} [Group H]
 
 /-- Subgroups of torsion groups are torsion groups. -/
 @[to_additive /-- Subgroups of additive torsion groups are additive torsion groups. -/]
-theorem IsTorsion.subgroup (tG : IsTorsion G) (H : Subgroup G) : IsTorsion H := fun h =>
+theorem IsTorsion.subgroup (tG : IsTorsion G) (H : Subgroup G) : IsTorsion H := fun h ↦
   Submonoid.isOfFinOrder_coe.1 <| tG h
 
 /-- The image of a surjective torsion group homomorphism is torsion. -/
 @[to_additive AddIsTorsion.of_surjective
-      /-- The image of a surjective additive torsion group homomorphism is torsion. -/]
+/-- The image of a surjective additive torsion group homomorphism is torsion. -/]
 theorem IsTorsion.of_surjective {f : G →* H} (hf : Function.Surjective f) (tG : IsTorsion G) :
-    IsTorsion H := fun h => by
-  obtain ⟨g, hg⟩ := hf h
-  rw [← hg]
+    IsTorsion H := fun h ↦ by
+  obtain ⟨g, rfl⟩ := hf h
   exact f.isOfFinOrder (tG g)
 
 /-- Torsion groups are closed under extensions. -/
 @[to_additive AddIsTorsion.extension_closed
 /-- Additive torsion groups are closed under extensions. -/]
 theorem IsTorsion.extension_closed {f : G →* H} (hN : N = f.ker) (tH : IsTorsion H)
-    (tN : IsTorsion N) : IsTorsion G := fun g => by
+    (tN : IsTorsion N) : IsTorsion G := fun g ↦ by
   obtain ⟨ngn, ngnpos, hngn⟩ := (tH <| f g).exists_pow_eq_one
   have hmem := MonoidHom.mem_ker.mpr ((f.map_pow g ngn).trans hngn)
   lift g ^ ngn to N using hN.symm ▸ hmem with gn h
   obtain ⟨nn, nnpos, hnn⟩ := (tN gn).exists_pow_eq_one
   exact isOfFinOrder_iff_pow_eq_one.mpr <| ⟨ngn * nn, mul_pos ngnpos nnpos, by
-      rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩
+    rw [pow_mul, ← h, ← Subgroup.coe_pow, hnn, Subgroup.coe_one]⟩
 
 /-- The image of a quotient is torsion iff the group is torsion. -/
 @[to_additive AddIsTorsion.quotient_iff
-      /-- The image of a quotient is additively torsion iff the group is torsion. -/]
+/-- The image of a quotient is additively torsion iff the group is torsion. -/]
 theorem IsTorsion.quotient_iff {f : G →* H} (hf : Function.Surjective f) (hN : N = f.ker)
     (tN : IsTorsion N) : IsTorsion H ↔ IsTorsion G :=
-  ⟨fun tH => IsTorsion.extension_closed hN tH tN, fun tG => IsTorsion.of_surjective hf tG⟩
+  ⟨fun tH ↦ IsTorsion.extension_closed hN tH tN, fun tG ↦ IsTorsion.of_surjective hf tG⟩
 
 /-- If a group exponent exists, the group is torsion. -/
 @[to_additive ExponentExists.is_add_torsion
-      /-- If a group exponent exists, the group is additively torsion. -/]
-theorem ExponentExists.isTorsion (h : ExponentExists G) : IsTorsion G := fun g => by
+/-- If a group exponent exists, the group is additively torsion. -/]
+theorem ExponentExists.isTorsion (h : ExponentExists G) : IsTorsion G := fun g ↦ by
   obtain ⟨n, npos, hn⟩ := h
   exact isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, hn g⟩
 
 /-- The group exponent exists for any bounded torsion group. -/
 @[to_additive IsAddTorsion.exponentExists
-      /-- The group exponent exists for any bounded additive torsion group. -/]
+/-- The group exponent exists for any bounded additive torsion group. -/]
 theorem IsTorsion.exponentExists (tG : IsTorsion G)
-    (bounded : (Set.range fun g : G => orderOf g).Finite) : ExponentExists G :=
+    (bounded : (Set.range fun g : G ↦ orderOf g).Finite) : ExponentExists G :=
   exponent_ne_zero.mp <|
-    (exponent_ne_zero_iff_range_orderOf_finite fun g => (tG g).orderOf_pos).mpr bounded
+    (exponent_ne_zero_iff_range_orderOf_finite fun g ↦ (tG g).orderOf_pos).mpr bounded
 
 /-- Finite groups are torsion groups. -/
 @[to_additive is_add_torsion_of_finite /-- Finite additive groups are additive torsion groups. -/]
@@ -158,8 +157,7 @@ namespace AddMonoid
 
 /-- A module whose scalars are additively torsion is additively torsion. -/
 theorem IsTorsion.module_of_torsion [Semiring R] [Module R M] (tR : IsTorsion R) : IsTorsion M :=
-  fun f =>
-  isOfFinAddOrder_iff_nsmul_eq_zero.mpr <| by
+  fun f ↦ isOfFinAddOrder_iff_nsmul_eq_zero.mpr <| by
     obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero
     exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩
 
@@ -198,7 +196,7 @@ variable {G}
 
 /-- Torsion submonoids are torsion. -/
 @[to_additive /-- Additive torsion submonoids are additively torsion. -/]
-theorem torsion.isTorsion : IsTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ =>
+theorem torsion.isTorsion : IsTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ ↦
   ⟨n, npos,
     Subtype.ext <| by
       dsimp
@@ -207,44 +205,56 @@ theorem torsion.isTorsion : IsTorsion <| torsion G := fun ⟨x, n, npos, hn⟩ =
       rw [_root_.mul_one, SubmonoidClass.coe_pow, Subtype.coe_mk,
         (isPeriodicPt_mul_iff_pow_eq_one _).mp hn]⟩
 
-variable (G) (p : ℕ) [hp : Fact p.Prime]
+variable (G) (p : ℕ)
 
-/-- The `p`-primary component is the submonoid of elements with order prime-power of `p`. -/
-@[to_additive (attr := simps)
-      /-- The `p`-primary component is the submonoid of elements with additive
-      order prime-power of `p`. -/]
+/-- The `p`-primary component is the submonoid of elements `g` such that `g ^ p ^ k = 1`
+for some `k`. For prime `p`, these are exactly the elements of `p`-power order. -/
+@[to_additive
+/-- The additive `p`-primary component is the submonoid of elements `g` such that
+`p ^ k • g = 0` for some `k`. For prime `p`, these are exactly the elements of additive
+`p`-power order. -/]
 def primaryComponent : Submonoid G where
-  carrier := { g | ∃ n : ℕ, orderOf g = p ^ n }
-  one_mem' := ⟨0, by rw [pow_zero, orderOf_one]⟩
-  mul_mem' hg₁ hg₂ :=
-    exists_orderOf_eq_prime_pow_iff.mpr <| by
-      obtain ⟨m, hm⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₁
-      obtain ⟨n, hn⟩ := exists_orderOf_eq_prime_pow_iff.mp hg₂
-      exact
-        ⟨m + n, by
-          rw [mul_pow, pow_add, pow_mul, hm, one_pow, Monoid.one_mul, mul_comm, pow_mul, hn,
-            one_pow]⟩
+  carrier := { g | ∃ k : ℕ, g ^ p ^ k = 1 }
+  one_mem' := ⟨0, by simp⟩
+  mul_mem' := fun {a b} ⟨m, hm⟩ ⟨n, hn⟩ ↦ ⟨m + n, by
+    rw [mul_pow, pow_add, pow_mul, hm, one_pow, one_mul, mul_comm, pow_mul, hn, one_pow]⟩
 
 variable {G} {p}
 
+/-- `g` lies in the `p`-primary component iff `g ^ p ^ k = 1` for some `k`. -/
+@[to_additive (attr := simp)
+/-- `g` lies in the additive `p`-primary component iff `p ^ k • g = 0` for some `k`. -/]
+theorem mem_primaryComponent {g : G} : g ∈ primaryComponent G p ↔ ∃ k : ℕ, g ^ p ^ k = 1 :=
+  .rfl
+
+/-- For prime `p`, `g` lies in the `p`-primary component iff its order is a power of `p`. -/
+@[to_additive
+/-- For prime `p`, `g` lies in the additive `p`-primary component iff its additive
+order is a power of `p`. -/]
+theorem mem_primaryComponent_iff_orderOf [Fact p.Prime] {g : G} :
+    g ∈ primaryComponent G p ↔ ∃ n : ℕ, orderOf g = p ^ n :=
+  exists_orderOf_eq_prime_pow_iff.symm
+
+variable [hp : Fact p.Prime]
+
 /-- Elements of the `p`-primary component have order `p^n` for some `n`. -/
 @[to_additive primaryComponent.exists_orderOf_eq_prime_nsmul
-  /-- Elements of the `p`-primary component have additive order `p^n` for some `n` -/]
+/-- Elements of the `p`-primary component have additive order `p^n` for some `n`. -/]
 theorem primaryComponent.exists_orderOf_eq_prime_pow (g : CommMonoid.primaryComponent G p) :
     ∃ n : ℕ, orderOf g = p ^ n := by
-      obtain ⟨_, hn⟩ := g.property
-      rw [orderOf_submonoid g] at hn
-      exact ⟨_, hn⟩
+  rw [← orderOf_submonoid, ← mem_primaryComponent_iff_orderOf]
+  exact g.property
 
 /-- The `p`- and `q`-primary components are disjoint for `p ≠ q`. -/
 @[to_additive /-- The `p`- and `q`-primary components are disjoint for `p ≠ q`. -/]
 theorem primaryComponent.disjoint {p' : ℕ} [hp' : Fact p'.Prime] (hne : p ≠ p') :
     Disjoint (CommMonoid.primaryComponent G p) (CommMonoid.primaryComponent G p') :=
-  Submonoid.disjoint_def.mpr <| by
-    rintro g ⟨_ | n, hn⟩ ⟨n', hn'⟩
+  Submonoid.disjoint_def.mpr fun {g} hg hg' ↦ by
+    rw [mem_primaryComponent_iff_orderOf] at hg hg'
+    obtain ⟨_ | n, hn⟩ := hg
     · rwa [pow_zero, orderOf_eq_one_iff] at hn
-    · exact
-        absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn.symm.trans hn')) hne
+    · obtain ⟨_, hn'⟩ := hg'
+      exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn ▸ hn')) hne
 
 end CommMonoid
 
@@ -278,8 +288,8 @@ end Monoid.IsTorsion
 
 /-- Torsion submonoids of a torsion submonoid are isomorphic to the submonoid. -/
 @[to_additive (attr := simp) AddCommMonoid.Torsion.ofTorsion
-      /-- Additive torsion submonoids of an additive torsion submonoid are
-      isomorphic to the submonoid. -/]
+/-- Additive torsion submonoids of an additive torsion submonoid are
+isomorphic to the submonoid. -/]
 def Torsion.ofTorsion : torsion (torsion G) ≃* torsion G :=
   Monoid.IsTorsion.torsionMulEquiv CommMonoid.torsion.isTorsion
 
@@ -294,12 +304,12 @@ namespace CommGroup
 /-- The torsion subgroup of an abelian group. -/
 @[to_additive /-- The torsion subgroup of an additive abelian group. -/]
 def torsion : Subgroup G :=
-  { CommMonoid.torsion G with inv_mem' := fun hx => IsOfFinOrder.inv hx }
+  { CommMonoid.torsion G with inv_mem' := fun hx ↦ IsOfFinOrder.inv hx }
 
 /-- The torsion submonoid of an abelian group equals the torsion subgroup as a submonoid. -/
 @[to_additive add_torsion_eq_add_torsion_submonoid
-      /-- The additive torsion submonoid of an abelian group equals the torsion
-      subgroup as a submonoid. -/]
+/-- The additive torsion submonoid of an abelian group equals the torsion
+subgroup as a submonoid. -/]
 theorem torsion_eq_torsion_submonoid : CommMonoid.torsion G = (torsion G).toSubmonoid :=
   rfl
 
@@ -327,22 +337,37 @@ lemma isTorsion_quotient_range_powMonoidHom {n : ℕ} (hn : n ≠ 0) :
   rw [← QuotientGroup.mk_pow, QuotientGroup.eq_one_iff]
   simp
 
-variable (p : ℕ) [hp : Fact p.Prime]
+variable (p : ℕ)
 
-/-- The `p`-primary component is the subgroup of elements with order prime-power of `p`. -/
-@[to_additive (attr := simps!)
-      /-- The `p`-primary component is the subgroup of elements with additive order
-      prime-power of `p`. -/]
+/-- The `p`-primary component is the subgroup of elements `g` such that `g ^ p ^ k = 1`
+for some `k`. For prime `p`, these are exactly the elements of `p`-power order. -/
+@[to_additive
+/-- The additive `p`-primary component is the subgroup of elements `g` such that
+`p ^ k • g = 0` for some `k`. For prime `p`, these are exactly the elements of additive
+`p`-power order. -/]
 def primaryComponent : Subgroup G :=
   { CommMonoid.primaryComponent G p with
-    inv_mem' := fun {g} ⟨n, hn⟩ => ⟨n, (orderOf_inv g).trans hn⟩ }
+    inv_mem' := fun {g} ⟨k, hk⟩ ↦ ⟨k, by rw [inv_pow, hk, inv_one]⟩ }
 
 variable {G} {p}
 
-/-- The `p`-primary component is a `p` group. -/
-theorem primaryComponent.isPGroup : IsPGroup p <| primaryComponent G p := fun g =>
-  (propext exists_orderOf_eq_prime_pow_iff.symm).mpr
-    (CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow g)
+/-- `g` lies in the `p`-primary component iff `g ^ p ^ k = 1` for some `k`. -/
+@[to_additive (attr := simp)
+/-- `g` lies in the additive `p`-primary component iff `p ^ k • g = 0` for some `k`. -/]
+theorem mem_primaryComponent {g : G} : g ∈ primaryComponent G p ↔ ∃ k : ℕ, g ^ p ^ k = 1 :=
+  .rfl
+
+/-- For prime `p`, `g` lies in the `p`-primary component iff its order is a power of `p`. -/
+@[to_additive
+/-- For prime `p`, `g` lies in the additive `p`-primary component iff its additive
+order is a power of `p`. -/]
+theorem mem_primaryComponent_iff_orderOf [Fact p.Prime] {g : G} :
+    g ∈ primaryComponent G p ↔ ∃ n : ℕ, orderOf g = p ^ n :=
+  exists_orderOf_eq_prime_pow_iff.symm
+
+/-- The `p`-primary component is a `p`-group. -/
+theorem primaryComponent.isPGroup : IsPGroup p (primaryComponent G p) := fun g ↦
+  g.property.imp fun _ hk ↦ Subtype.ext <| by simpa using hk
 
 end CommGroup
 
@@ -373,8 +398,8 @@ instance {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] :
   let e : (M ⧸ AddCommGroup.torsion M) ≃+ (M ⧸ S) := QuotientAddGroup.congr _ _ (.refl _)
     (by simp [S])
   -- So we can copy over scalar multiplication.
-  letI : SMul R (M ⧸ AddCommGroup.torsion M) := ⟨fun r m => e.symm (r • e m)⟩
-  Function.Injective.module R e.toAddMonoidHom e.injective (fun _ _ =>
+  letI : SMul R (M ⧸ AddCommGroup.torsion M) := ⟨fun r m ↦ e.symm (r • e m)⟩
+  Function.Injective.module R e.toAddMonoidHom e.injective (fun _ _ ↦
     e.symm.injective (e.symm_apply_apply _))
 
 end AddCommGroup