feat(group_theory/nilpotent): is_nilpotent_of_product_of_sylow_group (#11834)

Author: nomeata

src/group_theory/nilpotent.lean

@@ -8,6 +8,8 @@ import group_theory.general_commutator
 import group_theory.quotient_group
 import group_theory.solvable
 import group_theory.p_group
+import group_theory.sylow
+import data.nat.factorization
 
 /-!
 
@@ -77,6 +79,8 @@ are not central series if `G` is not nilpotent is a standard abuse of notation.
 
 open subgroup
 
+section with_group
+
 variables {G : Type*} [group G] (H : subgroup G) [normal H]
 
 /-- If `H` is a normal subgroup of `G`, then the set `{x : G | ∀ y : G, x*y*x⁻¹*y⁻¹ ∈ H}`
@@ -533,7 +537,7 @@ begin
   simp only [lower_central_series_nilpotency_class, le_bot_iff],
 end
 
-/-- The range of a surejctive homomorphism from a nilpotent group is nilpotent -/
+/-- The range of a surjective homomorphism from a nilpotent group is nilpotent -/
 lemma nilpotent_of_surjective {G' : Type*} [group G'] [h : is_nilpotent G]
   (f : G →* G') (hf : function.surjective f) :
   is_nilpotent G' :=
@@ -563,6 +567,11 @@ begin
     ... ≤ upper_central_series G' n : upper_central_series.map hf n,
 end
 
+/-- Nilpotency respects isomorphisms -/
+lemma nilpotent_of_mul_equiv {G' : Type*} [group G'] [h : is_nilpotent G] (f : G ≃* G') :
+  is_nilpotent G' :=
+nilpotent_of_surjective f.to_monoid_hom (mul_equiv.surjective f)
+
 /-- A quotient of a nilpotent group is nilpotent -/
 instance nilpotent_quotient_of_nilpotent (H : subgroup G) [H.normal] [h : is_nilpotent G] :
   is_nilpotent (G ⧸ H) :=
@@ -823,32 +832,6 @@ begin
   exact derived_le_lower_central n,
 end
 
-section classical
-
-open_locale classical -- to get the fintype instance for quotient groups
-
-/-- A p-group is nilpotent -/
-lemma is_p_group.is_nilpotent {G : Type*} [hG : group G] [hf : fintype G]
-  {p : ℕ} (hp : fact (nat.prime p)) (h : is_p_group p G) :
-  is_nilpotent G :=
-begin
-  unfreezingI
-  { revert hG,
-    induction hf using fintype.induction_subsingleton_or_nontrivial with G hG hS G hG hN ih },
-  { apply_instance, },
-  { introI _, intro h,
-    have hc : center G > ⊥ := gt_iff_lt.mp h.bot_lt_center,
-    have hcq : fintype.card (G ⧸ center G) < fintype.card G,
-    { rw card_eq_card_quotient_mul_card_subgroup (center G),
-      apply lt_mul_of_one_lt_right,
-      exact (fintype.card_pos_iff.mpr has_one.nonempty),
-      exact ((subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt hc)), },
-    have hnq : is_nilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G)),
-    exact (of_quotient_center_nilpotent hnq), }
-end
-
-end classical
-
 lemma normalizer_condition_of_is_nilpotent [h : is_nilpotent G] : normalizer_condition G :=
 begin
   -- roughly based on https://groupprops.subwiki.org/wiki/Nilpotent_implies_normalizer_condition
@@ -871,3 +854,47 @@ begin
     apply map_injective_of_ker_le (mk' (center G)) hkh le_top,
     exact (ih H' hH').trans (symm (map_top_of_surjective _ hsur)), },
 end
+
+end with_group
+
+section with_finite_group
+
+open group
+
+variables {G : Type*} [hG : group G] [hf : fintype G]
+include hG hf
+
+/-- A p-group is nilpotent -/
+lemma is_p_group.is_nilpotent {p : ℕ} [hp : fact (nat.prime p)] (h : is_p_group p G) :
+  is_nilpotent G :=
+begin
+  classical,
+  unfreezingI
+  { revert hG,
+    induction hf using fintype.induction_subsingleton_or_nontrivial with G hG hS G hG hN ih },
+  { apply_instance, },
+  { introI _, intro h,
+    have hcq : fintype.card (G ⧸ center G) < fintype.card G,
+    { rw card_eq_card_quotient_mul_card_subgroup (center G),
+      apply lt_mul_of_one_lt_right,
+      exact (fintype.card_pos_iff.mpr has_one.nonempty),
+      exact ((subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt h.bot_lt_center)), },
+    have hnq : is_nilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G)),
+    exact (of_quotient_center_nilpotent hnq), }
+end
+
+/-- If a finite group is the direct product of its Sylow groups, it is nilpotent -/
+theorem is_nilpotent_of_product_of_sylow_group
+  (e : (Π p : (fintype.card G).factorization.support, Π P : sylow p G, (↑P : subgroup G)) ≃* G) :
+  is_nilpotent G :=
+begin
+  classical,
+  let ps := (fintype.card G).factorization.support,
+  haveI : ∀ (p : ps) (P : sylow p G), is_nilpotent (↑P : subgroup G),
+  { intros p P,
+    haveI : fact (nat.prime ↑p) := fact.mk (nat.prime_of_mem_factorization (finset.coe_mem p)),
+    exact P.is_p_group'.is_nilpotent, },
+  exact nilpotent_of_mul_equiv e,
+end
+
+end with_finite_group