feat(group_theory/nilpotent): add lemmas about G / center G (#11592)

in particular its nilpotency class and an induction principle based on
that.

src/group_theory/nilpotent.lean

@@ -55,6 +55,8 @@ subgroup `G` of `G`, and `⊥` denotes the trivial subgroup `{1}`.
   `lower_central_series_length_eq_nilpotency_class`.
 * If `G` is nilpotent, then so are its subgroups, images, quotients and preimages.
   Corresponding lemmas about the `nilpotency_class` are provided.
+* The `nilpotency_class` of `G ⧸ center G` is given explicitly, and an induction principle
+  is derived from that.
 * `is_nilpotent.to_is_solvable`: If `G` is nilpotent, it is solvable.
 
 
@@ -574,6 +576,93 @@ instance nilpotent_quotient_of_nilpotent (H : subgroup G) [H.normal] [h : is_nil
 lemma nilpotency_class_quotient_le (H : subgroup G) [H.normal] [h : is_nilpotent G] :
   group.nilpotency_class (G ⧸ H) ≤ group.nilpotency_class G := nilpotency_class_le_of_surjective _ _
 
+-- This technical lemma helps with rewriting the subgroup, which occurs in indices
+private lemma comap_center_subst {H₁ H₂ : subgroup G} [normal H₁] [normal H₂] (h : H₁ = H₂) :
+  comap (mk' H₁) (center (G ⧸ H₁)) = comap (mk' H₂) (center (G ⧸ H₂)) :=
+by unfreezingI { subst h }
+
+lemma comap_upper_central_series_quotient_center (n : ℕ) :
+  comap (mk' (center G)) (upper_central_series (G ⧸ center G) n) = upper_central_series G n.succ :=
+begin
+  induction n with n ih,
+  { simp, },
+  { let Hn := upper_central_series (G ⧸ center G) n,
+    calc comap (mk' (center G)) (upper_central_series_step Hn)
+        = comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) :
+        by rw upper_central_series_step_eq_comap_center
+    ... = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ (comap (mk' (center G)) Hn))) :
+        quotient_group.comap_comap_center
+    ... = comap (mk' (upper_central_series G n.succ)) (center (G ⧸ upper_central_series G n.succ)) :
+        comap_center_subst ih
+    ... = upper_central_series_step (upper_central_series G n.succ) :
+        symm (upper_central_series_step_eq_comap_center _), }
+end
+
+lemma nilpotency_class_zero_iff_subsingleton [is_nilpotent G] :
+  group.nilpotency_class G = 0 ↔ subsingleton G :=
+by simp [group.nilpotency_class, nat.find_eq_zero, subsingleton_iff_bot_eq_top]
+
+section classical
+
+open_locale classical
+
+/-- Quotienting the `center G` reduces the nilpotency class by 1 -/
+lemma nilpotency_class_quotient_center [hH : is_nilpotent G] :
+  group.nilpotency_class (G ⧸ center G) = group.nilpotency_class G - 1 :=
+begin
+  generalize hn : group.nilpotency_class G = n,
+  rcases n with rfl | n,
+  { simp [nilpotency_class_zero_iff_subsingleton] at *,
+    haveI := hn,
+    apply_instance, },
+  { suffices : group.nilpotency_class (G ⧸ center G) = n, by simpa,
+    apply le_antisymm,
+    { apply upper_central_series_eq_top_iff_nilpotency_class_le.mp,
+      apply (@comap_injective G _ _ _ (mk' (center G)) (surjective_quot_mk _)),
+      rw [ comap_upper_central_series_quotient_center, comap_top, ← hn],
+      exact upper_central_series_nilpotency_class, },
+    { apply le_of_add_le_add_right,
+      calc n + 1 = n.succ : rfl
+        ... = group.nilpotency_class G : symm hn
+        ... ≤ group.nilpotency_class (G ⧸ center G) + 1
+            : nilpotency_class_le_of_ker_le_center _ (le_of_eq (ker_mk _)) _, } }
+end
+
+/-- Quotienting the `center G` reduces the nilpotency class by 1 -/
+lemma nilpotency_class_eq_quotient_center_plus_one [hH : is_nilpotent G] [nontrivial G] :
+  group.nilpotency_class G = group.nilpotency_class (G ⧸ center G) + 1 :=
+begin
+  rw nilpotency_class_quotient_center,
+  rcases h : group.nilpotency_class G,
+  { exfalso,
+    rw nilpotency_class_zero_iff_subsingleton at h, resetI,
+    apply (false_of_nontrivial_of_subsingleton G), },
+  { simp }
+end
+
+end classical
+
+/-- 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. -/
+@[elab_as_eliminator]
+lemma nilpotent_center_quotient_ind
+  {P : Π G [group G], by exactI ∀ [is_nilpotent G], Prop}
+  (G : Type*) [group G] [is_nilpotent G]
+  (hbase : ∀ G [group G] [subsingleton G], by exactI P G)
+  (hstep : ∀ G [group G], by exactI ∀ [is_nilpotent G], by exactI ∀ (ih : P (G ⧸ center G)), P G) :
+  P G :=
+begin
+  obtain ⟨n, h⟩ : ∃ n, group.nilpotency_class G = n := ⟨ _, rfl⟩,
+  unfreezingI { induction n with n ih generalizing G },
+  { haveI := nilpotency_class_zero_iff_subsingleton.mp h,
+    exact hbase _, },
+  { have hn : group.nilpotency_class (G ⧸ center G) = n :=
+      by simp [nilpotency_class_quotient_center, h],
+    exact hstep _ (ih _ hn), },
+end
+
+
 lemma derived_le_lower_central (n : ℕ) : derived_series G n ≤ lower_central_series G n :=
 by { induction n with i ih, { simp }, { apply general_commutator_mono ih, simp } }
 

src/group_theory/quotient_group.lean

@@ -405,4 +405,18 @@ top_unique $ λ x _,
 
 end trivial
 
+@[to_additive quotient_add_grup.comap_comap_center]
+lemma comap_comap_center {H₁ : subgroup G} [H₁.normal] {H₂ : subgroup (G ⧸ H₁)} [H₂.normal] :
+  (((subgroup.center ((G ⧸ H₁) ⧸ H₂))).comap (mk' H₂)).comap (mk' H₁) =
+  (subgroup.center (G ⧸ H₂.comap (mk' H₁))).comap (mk' (H₂.comap (mk' H₁))) :=
+begin
+  ext x,
+  simp only [mk'_apply, subgroup.mem_comap, subgroup.mem_center_iff, forall_coe],
+  apply forall_congr,
+  change ∀ (y : G), (↑↑(y * x) = ↑↑(x * y) ↔ ↑(y * x) = ↑(x * y)),
+  intro y,
+  repeat { rw [eq_iff_div_mem] },
+  simp,
+end
+
 end quotient_group