feat(GroupTheory/Commutator/Basic): ⁅H₁, H₂⁆ is a normal subgroup of H₁ ⊔ H₂ (leanprover-community#39227)

Shows `⁅H₁, H₂⁆ ≤ H₁ ⊔ H₂` and `(⁅H₁, H₂⁆.subgroupOf <| H₁ ⊔ H₂).Normal`, and adds `_ ≤ normalizer _ ↔` lemmas to help.

Author: SnirBroshi

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -337,26 +337,30 @@ theorem mem_normalizer_iff_conj_image_eq {s : Set G} {g : G} :
   refine forall_congr' fun h ↦ ?_
   simp_rw [mul_inv_eq_iff_eq_mul, ← eq_inv_mul_iff_mul_eq, ← mul_assoc, exists_eq_right, iff_comm]
 
-theorem _root_.AddSubgroup.mem_normalizer_iff_conj_image_eq {G : Type*} [AddGroup G] {s : Set G}
+theorem _root_.AddSubgroup.mem_normalizer_iff_addConj_image_eq {G : Type*} [AddGroup G] {s : Set G}
     {g : G} : g ∈ AddSubgroup.normalizer s ↔ AddAut.conj g '' s = s := by
   simp_rw [AddSubgroup.mem_set_normalizer_iff'', Set.ext_iff, Set.mem_image, AddAut.conj_apply]
   refine forall_congr' fun h ↦ ?_
   simp_rw [add_neg_eq_iff_eq_add, ← eq_neg_add_iff_add_eq, ← add_assoc, exists_eq_right, iff_comm]
 
+@[deprecated (since := "2026-05-12")]
+alias _root_.AddSubgroup.mem_normalizer_iff_conj_image_eq :=
+  AddSubgroup.mem_normalizer_iff_addConj_image_eq
+
 theorem normalizer_le_normalizer_closure (s : Set G) : normalizer s ≤ normalizer (closure s) := by
   intro g hg
   have : MulAut.conj g '' (closure s) = closure (MulAut.conj g '' s) :=
-    congr(SetLike.coe $(MulAut.conj g |>.toMonoidHom.map_closure s))
+    congr($(MulAut.conj g |>.toMonoidHom.map_closure s))
   rw [mem_normalizer_iff_conj_image_eq.mp hg] at this
   rwa [mem_normalizer_iff_conj_image_eq]
 
 theorem _root_.AddSubgroup.normalizer_le_normalizer_closure {G : Type*} [AddGroup G] (s : Set G) :
     AddSubgroup.normalizer s ≤ AddSubgroup.normalizer (AddSubgroup.closure s) := by
   intro g hg
   have : AddAut.conj g '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj g '' s) :=
-    congr(SetLike.coe $(AddAut.conj g |>.toAddMonoidHom.map_closure s))
-  rw [AddSubgroup.mem_normalizer_iff_conj_image_eq.mp hg] at this
-  rwa [AddSubgroup.mem_normalizer_iff_conj_image_eq]
+    congr($(AddAut.conj g |>.toAddMonoidHom.map_closure s))
+  rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq.mp hg] at this
+  rwa [AddSubgroup.mem_normalizer_iff_addConj_image_eq]
 
 variable {H}
 
@@ -371,6 +375,39 @@ variable (H) in
 theorem normalizer_eq_top [h : H.Normal] : normalizer (H : Set G) = ⊤ :=
   normalizer_eq_top_iff.mpr h
 
+@[to_additive]
+theorem le_set_normalizer_iff {s : Set G} :
+    H ≤ normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ s := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
+  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk
+
+@[to_additive]
+theorem le_normalizer_iff : H ≤ normalizer K ↔ ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp hg, fun hH h hh k ↦ ⟨fun hk ↦ hH h hh k hk, fun hk ↦ ?_⟩⟩
+  simpa [mul_assoc] using hH h⁻¹ (inv_mem hh) _ hk
+
+theorem le_normalizer_closure_iff {s : Set G} :
+    H ≤ normalizer (closure s) ↔ ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
+  have : MulAut.conj h '' (closure s) = closure (MulAut.conj h '' s) :=
+    congr($(MulAut.conj h |>.toMonoidHom.map_closure s))
+  rw [mem_normalizer_iff_conj_image_eq, this]
+  apply subset_antisymm <| by simpa using hH h hh
+  rw [SetLike.coe_subset_coe, closure_le, ← this]
+  exact fun g hg ↦ ⟨_, hH _ (inv_mem hh) g hg, by simp [mul_assoc]⟩
+
+theorem _root_.AddSubgroup.le_normalizer_closure_iff {G : Type*} [AddGroup G] {H : AddSubgroup G}
+    {s : Set G} :
+    H ≤ AddSubgroup.normalizer (AddSubgroup.closure s) ↔
+      ∀ h ∈ H, ∀ g ∈ s, h + g + -h ∈ AddSubgroup.closure s := by
+  refine ⟨fun hH h hh g hg ↦ hH hh g |>.mp <| AddSubgroup.mem_closure_of_mem hg, fun hH h hh ↦ ?_⟩
+  have : AddAut.conj h '' (AddSubgroup.closure s) = AddSubgroup.closure (AddAut.conj h '' s) :=
+    congr($(AddAut.conj h |>.toAddMonoidHom.map_closure s))
+  rw [AddSubgroup.mem_normalizer_iff_addConj_image_eq, this]
+  apply subset_antisymm <| by simpa using hH h hh
+  rw [SetLike.coe_subset_coe, AddSubgroup.closure_le, ← this]
+  exact fun g hg ↦ ⟨_, hH _ (neg_mem hh) g hg, by simp [add_assoc]⟩
+
 variable {N : Type*} [Group N]
 
 /-- The preimage of the normalizer is contained in the normalizer of the preimage. -/

Mathlib/GroupTheory/Commutator/Basic.lean

@@ -70,6 +70,16 @@ theorem map_commutatorElement : (f ⁅g₁, g₂⁆ : G') = ⁅f g₁, f g₂⁆
 theorem conjugate_commutatorElement : g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆ := by
   simp [mul_assoc, commutatorElement_def]
 
+@[to_additive]
+theorem commutatorElement_mul_left_eq_conj_mul (a b c : G) :
+    ⁅a * b, c⁆ = a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆ := by
+  simp [mul_assoc, commutatorElement_def]
+
+@[to_additive]
+theorem commutatorElement_mul_right_eq_mul_conj (a b c : G) :
+    ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹ := by
+  simp [mul_assoc, commutatorElement_def]
+
 namespace Subgroup
 
 /-- The commutator of two subgroups `H₁` and `H₂`. -/
@@ -82,7 +92,7 @@ theorem commutator_def (H₁ H₂ : Subgroup G) :
     ⁅H₁, H₂⁆ = closure { g | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = g } :=
   rfl
 
-variable {g₁ g₂ g₃} {H H₁ H₂ H₃ K₁ K₂ : Subgroup G}
+variable {g₁ g₂ g₃} {H H₁ H₂ H₃ K K₁ K₂ : Subgroup G}
 
 @[to_additive]
 theorem commutator_mem_commutator (h₁ : g₁ ∈ H₁) (h₂ : g₂ ∈ H₂) : ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆ :=
@@ -165,6 +175,16 @@ theorem commutator_top_left_le_iff : ⁅(⊤ : Subgroup G), H⁆ ≤ H ↔ H.Nor
 theorem commutator_top_right_le_iff : ⁅H, ⊤⁆ ≤ H ↔ H.Normal :=
   commutator_comm H ⊤ ▸ commutator_top_left_le_iff
 
+@[to_additive]
+theorem le_normalizer_iff_commutator_le_right : H ≤ normalizer K ↔ ⁅H, K⁆ ≤ K := by
+  refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩
+  · exact commutator_le.mpr fun h hh k hk ↦ mul_mem (hH h hh k hk) (inv_mem hk)
+  · exact (mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk
+
+@[to_additive]
+theorem le_normalizer_iff_commutator_le_left : H ≤ normalizer K ↔ ⁅K, H⁆ ≤ K :=
+  commutator_comm H K ▸ le_normalizer_iff_commutator_le_right
+
 @[to_additive (attr := simp)]
 theorem commutator_bot_left : ⁅(⊥ : Subgroup G), H₁⁆ = ⊥ :=
   le_bot_iff.mp (commutator_le_left ⊥ H₁)
@@ -179,6 +199,28 @@ theorem commutator_le_inf [Normal H₁] [Normal H₂] : ⁅H₁, H₂⁆ ≤ H
 
 end Normal
 
+@[to_additive]
+theorem commutator_le_sup : ⁅H₁, H₂⁆ ≤ H₁ ⊔ H₂ :=
+  commutator_le.mpr <| by grind [mul_assoc, mul_mem, mul_mem_sup, inv_mem]
+
+@[to_additive]
+theorem normalizer_commutator_ge_left : H₁ ≤ normalizer (⁅H₁, H₂⁆ : Subgroup G) := by
+  apply le_normalizer_closure_iff.mpr
+  rintro g hg _ ⟨g₁, hg₁, g₂, hg₂, rfl⟩
+  apply (mul_mem_cancel_right <| commutator_mem_commutator hg hg₂).mp
+  rw [← commutatorElement_mul_left_eq_conj_mul g g₁ g₂]
+  exact commutator_mem_commutator (mul_mem hg hg₁) hg₂
+
+@[to_additive]
+theorem normalizer_commutator_ge_right : H₂ ≤ normalizer (⁅H₁, H₂⁆ : Subgroup G) := by
+  rw [commutator_comm]
+  apply normalizer_commutator_ge_left
+
+@[to_additive]
+instance normal_subgroupOf_commutator_sup : (⁅H₁, H₂⁆.subgroupOf <| H₁ ⊔ H₂).Normal :=
+  normal_subgroupOf_of_le_normalizer <| sup_le
+    (normalizer_commutator_ge_left H₁ H₂) (normalizer_commutator_ge_right H₁ H₂)
+
 @[to_additive]
 theorem map_commutator (f : G →* G') : map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆ := by
   simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]