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

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₂`. -/
@@ -179,6 +189,22 @@ 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]
+instance normal_subgroupOf_commutator_sup : (⁅H₁, H₂⁆.subgroupOf <| H₁ ⊔ H₂).Normal := by
+  refine normal_subgroupOf_of_le_normalizer <| sup_le ?_ ?_ <;>
+    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₂
+  · apply (mul_mem_cancel_left <| commutator_mem_commutator hg₁ hg).mp
+    rw [← mul_assoc, ← mul_assoc, ← commutatorElement_mul_right_eq_mul_conj]
+    exact commutator_mem_commutator hg₁ <| mul_mem hg hg₂
+
 @[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]