refactor(GroupTheory/Nilpotent): add junk value to Group.nilpotencyClass (#35824)

This PR adds a junk value to `Group.nilpotencyClass` (similar to `nilpotencyClass` for rings). Can't hurt, since it only makes things more general, and occasionally allows for simpler statements.

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

Author: tb65536

Mathlib/GroupTheory/Nilpotent.lean

@@ -362,24 +362,37 @@ theorem nilpotent_iff_lowerCentralSeries : IsNilpotent G ↔ ∃ n, lowerCentral
 
 section Classical
 
-variable [hG : IsNilpotent G]
-
 variable (G) in
 open scoped Classical in
 /-- The nilpotency class of a nilpotent group is the smallest natural `n` such that
-the `n`-th term of the upper central series is `G`. -/
-noncomputable def Group.nilpotencyClass : ℕ := Nat.find (IsNilpotent.nilpotent G)
+the `n`-th term of the upper central series is `G`. If `G` is not nilpotent then the nilpotency
+class takes the junk value 0. -/
+noncomputable def Group.nilpotencyClass : ℕ :=
+  if hG : IsNilpotent G then Nat.find hG.nilpotent else 0
+
+theorem Group.nilpotencyClass_of_not_nilpotent (hG : ¬ IsNilpotent G) :
+    Group.nilpotencyClass G = 0 :=
+  dif_neg hG
+
+variable [hG : IsNilpotent G]
 
 open scoped Classical in
+theorem Group.nilpotencyClass_def :
+    Group.nilpotencyClass G = Nat.find (IsNilpotent.nilpotent G) :=
+  dif_pos hG
+
 @[simp]
-theorem upperCentralSeries_nilpotencyClass : upperCentralSeries G (Group.nilpotencyClass G) = ⊤ :=
-  Nat.find_spec (IsNilpotent.nilpotent G)
+theorem upperCentralSeries_nilpotencyClass :
+    upperCentralSeries G (Group.nilpotencyClass G) = ⊤ := by
+  classical
+  rw [nilpotencyClass_def, Nat.find_spec (IsNilpotent.nilpotent G)]
 
 theorem upperCentralSeries_eq_top_iff_nilpotencyClass_le {n : ℕ} :
     upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n := by
   classical
   constructor
   · intro h
+    rw [nilpotencyClass_def]
     exact Nat.find_le h
   · intro h
     rw [eq_top_iff, ← upperCentralSeries_nilpotencyClass]
@@ -391,6 +404,7 @@ central series reaches `G` in its `n`-th term. -/
 theorem least_ascending_central_series_length_eq_nilpotencyClass :
     Nat.find ((nilpotent_iff_finite_ascending_central_series G).mp hG) =
     Group.nilpotencyClass G := by
+  rw [nilpotencyClass_def]
   refine le_antisymm (Nat.find_mono ?_) (Nat.find_mono ?_)
   · intro n hn
     exact ⟨upperCentralSeries G, upperCentralSeries_isAscendingCentralSeries G, hn⟩
@@ -513,18 +527,17 @@ theorem lowerCentralSeries_succ_eq_bot {n : ℕ} (h : lowerCentralSeries G n ≤
 /-- The preimage of a nilpotent group is nilpotent if the kernel of the homomorphism is contained
 in the center -/
 theorem isNilpotent_of_ker_le_center {H : Type*} [Group H] (f : G →* H) (hf1 : f.ker ≤ center G)
-    (hH : IsNilpotent H) : IsNilpotent G := by
-  rw [nilpotent_iff_lowerCentralSeries] at *
-  rcases hH with ⟨n, hn⟩
+    [IsNilpotent H] : IsNilpotent G := by
+  rw [nilpotent_iff_lowerCentralSeries]
+  rcases nilpotent_iff_lowerCentralSeries.mp ‹_› with ⟨n, hn⟩
   use n + 1
   refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
   exact eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)
 
 theorem nilpotencyClass_le_of_ker_le_center {H : Type*} [Group H] (f : G →* H)
-    (hf1 : f.ker ≤ center G) (hH : IsNilpotent H) :
-    Group.nilpotencyClass (hG := isNilpotent_of_ker_le_center f hf1 hH) ≤
-      Group.nilpotencyClass H + 1 := by
-  haveI : IsNilpotent G := isNilpotent_of_ker_le_center f hf1 hH
+    (hf1 : f.ker ≤ center G) [IsNilpotent H] :
+    Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1 := by
+  have : IsNilpotent G := isNilpotent_of_ker_le_center f hf1
   rw [← lowerCentralSeries_length_eq_nilpotencyClass]
   classical apply Nat.find_min'
   refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
@@ -548,7 +561,9 @@ theorem nilpotent_of_surjective {G' : Type*} [Group G'] [h : IsNilpotent G] (f :
 nilpotent group is less or equal the nilpotency class of the domain -/
 theorem nilpotencyClass_le_of_surjective {G' : Type*} [Group G'] (f : G →* G')
     (hf : Function.Surjective f) [h : IsNilpotent G] :
-    Group.nilpotencyClass (hG := nilpotent_of_surjective _ hf) ≤ Group.nilpotencyClass G := by
+    Group.nilpotencyClass G' ≤ Group.nilpotencyClass G := by
+  have := nilpotent_of_surjective _ hf
+  rw [nilpotencyClass_def, nilpotencyClass_def]
   classical apply Nat.find_mono
   intro n hn
   rw [eq_top_iff]
@@ -599,12 +614,21 @@ theorem comap_upperCentralSeries_quotient_center (n : ℕ) :
 theorem nilpotencyClass_zero_iff_subsingleton [IsNilpotent G] :
     Group.nilpotencyClass G = 0 ↔ Subsingleton G := by
   classical
-  rw [Group.nilpotencyClass, Nat.find_eq_zero, upperCentralSeries_zero,
+  rw [Group.nilpotencyClass_def, Nat.find_eq_zero, upperCentralSeries_zero,
     subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]
 
+/-- If the quotient by `center G` is nilpotent, then so is G. -/
+theorem of_quotient_center_nilpotent (h : IsNilpotent (G ⧸ center G)) : IsNilpotent G := by
+  obtain ⟨n, hn⟩ := h.nilpotent
+  use n.succ
+  simp [← comap_upperCentralSeries_quotient_center, hn]
+
 /-- Quotienting the `center G` reduces the nilpotency class by 1 -/
-theorem nilpotencyClass_quotient_center [hH : IsNilpotent G] :
+theorem nilpotencyClass_quotient_center :
     Group.nilpotencyClass (G ⧸ center G) = Group.nilpotencyClass G - 1 := by
+  by_cases hH : IsNilpotent G; swap
+  · rw [nilpotencyClass_of_not_nilpotent hH, zero_tsub, nilpotencyClass_of_not_nilpotent]
+    exact mt of_quotient_center_nilpotent hH
   generalize hn : Group.nilpotencyClass G = n
   rcases n with (rfl | n)
   · simp only [nilpotencyClass_zero_iff_subsingleton, zero_tsub] at *
@@ -619,7 +643,7 @@ theorem nilpotencyClass_quotient_center [hH : IsNilpotent G] :
       calc
         n + 1 = Group.nilpotencyClass G := hn.symm
         _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 :=
-          nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _)) _
+          nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _))
 
 /-- The nilpotency class of a non-trivial group is one more than its quotient by the center -/
 theorem nilpotencyClass_eq_quotient_center_plus_one [hH : IsNilpotent G] [Nontrivial G] :
@@ -631,12 +655,6 @@ theorem nilpotencyClass_eq_quotient_center_plus_one [hH : IsNilpotent G] [Nontri
     apply false_of_nontrivial_of_subsingleton G
   · simp
 
-/-- If the quotient by `center G` is nilpotent, then so is G. -/
-theorem of_quotient_center_nilpotent (h : IsNilpotent (G ⧸ center G)) : IsNilpotent G := by
-  obtain ⟨n, hn⟩ := h.nilpotent
-  use n.succ
-  simp [← comap_upperCentralSeries_quotient_center, hn]
-
 /-- A custom induction principle for nilpotent groups. The base case is a trivial group
 (`subsingleton G`), and in the induction step, one can assume the hypothesis for
 the group quotiented by its center. -/