feat(group_theory/nilpotent): n-ary products of nilpotent group (#11829)

Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

src/group_theory/nilpotent.lean

@@ -55,7 +55,8 @@ subgroup `G` of `G`, and `⊥` denotes the trivial subgroup `{1}`.
   `least_descending_central_series_length_eq_nilpotency_class` and
   `lower_central_series_length_eq_nilpotency_class`.
 * If `G` is nilpotent, then so are its subgroups, images, quotients and preimages.
-  Binary products of nilpotent groups are nilpotent.
+  Binary and finite products of nilpotent groups are nilpotent.
+  Infinite products are nilpotent if their nilpotent class is bounded.
   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.
@@ -731,6 +732,87 @@ end
 
 end prod
 
+section bounded_pi
+
+-- First the case of infinite products with bounded nilpotency class
+
+variables {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
+
+lemma lower_central_series_pi_le (n : ℕ):
+  lower_central_series (Π i, Gs i) n ≤ subgroup.pi set.univ (λ i, lower_central_series (Gs i) n) :=
+begin
+  let pi := λ (f : Π i, subgroup (Gs i)), subgroup.pi set.univ f,
+  induction n with n ih,
+  { simp [pi_top] },
+  { calc lower_central_series (Π i, Gs i) n.succ
+        = ⁅lower_central_series (Π i, Gs i) n, ⊤⁆           : rfl
+    ... ≤ ⁅pi (λ i, (lower_central_series (Gs i) n)), ⊤⁆    : general_commutator_mono ih (le_refl _)
+    ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), pi (λ i, ⊤)⁆ : by simp [pi, pi_top]
+    ... ≤ pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)    : general_commutator_pi_pi_le _ _
+    ... = pi (λ i, lower_central_series (Gs i) n.succ)      : rfl }
+end
+
+/-- products of nilpotent groups are nilpotent if their nipotency class is bounded -/
+lemma is_nilpotent_pi_of_bounded_class [∀ i, is_nilpotent (Gs i)]
+  (n : ℕ) (h : ∀ i, group.nilpotency_class (Gs i) ≤ n) :
+  is_nilpotent (Π i, Gs i) :=
+begin
+  rw nilpotent_iff_lower_central_series,
+  refine ⟨n, _⟩,
+  rw eq_bot_iff,
+  apply le_trans (lower_central_series_pi_le _),
+  rw [← eq_bot_iff, pi_eq_bot_iff],
+  intros i,
+  apply lower_central_series_eq_bot_iff_nilpotency_class_le.mpr (h i),
+end
+
+end bounded_pi
+
+section finite_pi
+
+-- Now for finite products
+
+variables {η : Type*} [fintype η] {Gs : η → Type*} [∀ i, group (Gs i)]
+
+lemma lower_central_series_pi_of_fintype (n : ℕ):
+  lower_central_series (Π i, Gs i) n = subgroup.pi set.univ (λ i, lower_central_series (Gs i) n) :=
+begin
+  let pi := λ (f : Π i, subgroup (Gs i)), subgroup.pi set.univ f,
+  induction n with n ih,
+  { simp [pi_top] },
+  { calc lower_central_series (Π i, Gs i) n.succ
+        = ⁅lower_central_series (Π i, Gs i) n, ⊤⁆          : rfl
+    ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), ⊤⁆   : by rw ih
+    ... = ⁅pi (λ i, (lower_central_series (Gs i) n)), pi (λ i, ⊤)⁆ : by simp [pi, pi_top]
+    ... = pi (λ i, ⁅(lower_central_series (Gs i) n), ⊤⁆)   : general_commutator_pi_pi_of_fintype _ _
+    ... = pi (λ i, lower_central_series (Gs i) n.succ)     : rfl }
+end
+
+/-- n-ary products of nilpotent groups are nilpotent -/
+instance is_nilpotent_pi [∀ i, is_nilpotent (Gs i)] :
+  is_nilpotent (Π i, Gs i) :=
+begin
+  rw nilpotent_iff_lower_central_series,
+  refine ⟨finset.univ.sup (λ i, group.nilpotency_class (Gs i)), _⟩,
+  rw [lower_central_series_pi_of_fintype, pi_eq_bot_iff],
+  intros i,
+  apply lower_central_series_eq_bot_iff_nilpotency_class_le.mpr,
+  exact @finset.le_sup _ _ _ _ finset.univ (λ i, group.nilpotency_class (Gs i)) _
+    (finset.mem_univ i),
+end
+
+/-- The nilpotency class of an n-ary product is the sup of the nilpotency classes of the factors -/
+lemma nilpotency_class_pi [∀ i, is_nilpotent (Gs i)] :
+  group.nilpotency_class (Π i, Gs i) = finset.univ.sup (λ i, group.nilpotency_class (Gs i)) :=
+begin
+  apply eq_of_forall_ge_iff,
+  intros k,
+  simp only [finset.sup_le_iff, ← lower_central_series_eq_bot_iff_nilpotency_class_le,
+    lower_central_series_pi_of_fintype, pi_eq_bot_iff, finset.mem_univ, true_implies_iff ],
+end
+
+end finite_pi
+
 /-- A nilpotent subgroup is solvable -/
 @[priority 100]
 instance is_nilpotent.to_is_solvable [h : is_nilpotent G]: is_solvable G :=