feat(group_theory/general_commutator): subgroup.pi commutes with the general_commutator (#11825)

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

Author: nomeata

src/group_theory/general_commutator.lean

@@ -137,3 +137,32 @@ begin
       simp [le_prod_iff, map_map, monoid_hom.fst_comp_inl, monoid_hom.snd_comp_inl,
         monoid_hom.fst_comp_inr, monoid_hom.snd_comp_inr ], }, }
 end
+
+/-- The commutator of direct product is contained in the direct product of the commutators.
+
+See `general_commutator_pi_pi_of_fintype` for equality given `fintype η`.
+-/
+lemma general_commutator_pi_pi_le {η : Type*} {Gs : η → Type*} [∀ i, group (Gs i)]
+  (H K : Π i, subgroup (Gs i)) :
+  ⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ ≤ subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=
+(general_commutator_le _ _ _).mpr $
+  λ p hp q hq i hi, general_commutator_containment _ _ (hp i hi) (hq i hi)
+
+/-- The commutator of a finite direct product is contained in the direct product of the commutators.
+-/
+lemma general_commutator_pi_pi_of_fintype {η : Type*} [fintype η] {Gs : η → Type*}
+  [∀ i, group (Gs i)] (H K : Π i, subgroup (Gs i)) :
+  ⁅subgroup.pi set.univ H, subgroup.pi set.univ K⁆ = subgroup.pi set.univ (λ i, ⁅H i, K i⁆) :=
+begin
+  classical,
+  apply le_antisymm (general_commutator_pi_pi_le H K),
+  { rw pi_le_iff, intros i hi,
+    rw map_general_commutator,
+    apply general_commutator_mono;
+    { rw le_pi_iff,
+      intros j hj,
+      rintros _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩,
+      by_cases h : j = i,
+      { subst h, simpa using hx, },
+      { simp [h, one_mem] }, }, },
+end

src/group_theory/subgroup/basic.lean

@@ -1154,6 +1154,81 @@ ext $ λ x, by simp [mem_pi]
 (eq_bot_iff_forall _).mpr $ λ p hp,
 by { simp only [mem_pi, mem_bot] at *, ext j, exact hp j trivial, }
 
+@[to_additive]
+lemma le_pi_iff {I : set η} {H : Π i, subgroup (f i)} {J : subgroup (Π i, f i)} :
+  J ≤ pi I H ↔ (∀ i : η , i ∈ I → map (pi.eval_monoid_hom f i) J ≤ H i) :=
+begin
+  split,
+  { intros h i hi, rintros _ ⟨x, hx, rfl⟩, exact (h hx) _ hi, },
+  { intros h x hx i hi, refine h i hi ⟨_, hx, rfl⟩, }
+end
+
+@[simp]
+lemma single_mem_pi [decidable_eq η] {I : set η} {H : Π i, subgroup (f i)}
+  (i : η) (x : f i) :
+  monoid_hom.single f i x ∈ pi I H ↔ (i ∈ I → x ∈ H i) :=
+begin
+  split,
+  { intros h hi, simpa using h i hi, },
+  { intros h j hj,
+    by_cases heq : j = i,
+    { subst heq, simpa using h hj, },
+    { simp [heq, one_mem], }, }
+end
+
+lemma pi_mem_of_single_mem_aux [decidable_eq η] (I : finset η) {H : subgroup (Π i, f i) }
+  (x : Π i, f i) (h1 : ∀ i, i ∉ I → x i = 1) (h2 : ∀ i, i ∈ I → pi.mul_single i (x i) ∈ H ) :
+  x ∈ H :=
+begin
+  induction I using finset.induction_on with i I hnmem ih generalizing x,
+  { have : x = 1,
+    { ext i, refine (h1 i (not_mem_empty i)), },
+    simp [this, one_mem], },
+  { have : x = function.update x i 1 * pi.mul_single i (x i),
+    { ext j,
+      by_cases heq : j = i,
+      { subst heq, simp, },
+      { simp [heq], }, },
+    rw this, clear this,
+    apply mul_mem,
+    { apply ih; clear ih,
+      { intros j hj,
+        by_cases heq : j = i,
+        { subst heq, simp, },
+        { simp [heq], apply h1 j, simpa [heq] using hj, } },
+      { intros j hj,
+        have : j ≠ i, by { rintro rfl, contradiction },
+        simp [this],
+        exact h2 _ (finset.mem_insert_of_mem hj), }, },
+    { apply h2, simp, } }
+end
+
+lemma pi_mem_of_single_mem [fintype η] [decidable_eq η] {H : subgroup (Π i, f i) } (x : Π i, f i)
+  (h : ∀ i, pi.mul_single i (x i) ∈ H) : x ∈ H :=
+pi_mem_of_single_mem_aux finset.univ x (by simp) (λ i _, h i)
+
+/-- For finite index types, the `subgroup.pi` is generated by the embeddings of the groups.  -/
+lemma pi_le_iff [decidable_eq η] [fintype η] {H : Π i, subgroup (f i)} {J : subgroup (Π i, f i)} :
+  pi univ H ≤ J ↔ (∀ i : η, map (monoid_hom.single f i) (H i) ≤ J) :=
+begin
+  split,
+  { rintros h i _ ⟨x, hx, rfl⟩, apply h, simpa using hx },
+  { exact λ h x hx, pi_mem_of_single_mem  x (λ i, h i (mem_map_of_mem _ (hx i trivial))), }
+end
+
+lemma pi_eq_bot_iff (H : Π i, subgroup (f i)) :
+  pi set.univ H = ⊥ ↔ ∀ i, H i = ⊥ :=
+begin
+  classical,
+  simp only [eq_bot_iff_forall],
+  split,
+  { intros h i x hx,
+    have : monoid_hom.single f i x = 1 :=
+    h (monoid_hom.single f i x) ((single_mem_pi i x).mpr (λ _, hx)),
+    simpa using congr_fun this i, },
+  { exact λ h x hx, funext (λ i, h _ _ (hx i trivial)), },
+end
+
 end pi
 
 /-- A subgroup is normal if whenever `n ∈ H`, then `g * n * g⁻¹ ∈ H` for every `g : G` -/