diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean index 83b4cc4a47dc35..39a74b2cb5c5e0 100644 --- a/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean @@ -337,16 +337,20 @@ 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] @@ -354,9 +358,9 @@ theorem _root_.AddSubgroup.normalizer_le_normalizer_closure {G : Type*} [AddGrou 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. -/ diff --git a/Mathlib/GroupTheory/Commutator/Basic.lean b/Mathlib/GroupTheory/Commutator/Basic.lean index 7fcf19a1b0d8d9..43a7f4929a4fa8 100644 --- a/Mathlib/GroupTheory/Commutator/Basic.lean +++ b/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,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]