From f3a04edad2f7569b2ec277c64d41fca364441525 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Mon, 28 Feb 2022 02:34:22 +0000 Subject: [PATCH] feat(group_theory/subgroup/basic): Centralizer subgroup (#11946) This PR defines the centralizer subgroup, and provides a few basic lemmas. Co-authored-by: tb65536 --- src/group_theory/subgroup/basic.lean | 29 +++- src/group_theory/submonoid/centralizer.lean | 146 ++++++++++++++++++++ 2 files changed, 174 insertions(+), 1 deletion(-) create mode 100644 src/group_theory/submonoid/centralizer.lean diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean index 3fb589b2def9e..098a590c78ed2 100644 --- a/src/group_theory/subgroup/basic.lean +++ b/src/group_theory/subgroup/basic.lean @@ -5,7 +5,7 @@ Authors: Kexing Ying -/ import group_theory.submonoid.pointwise import group_theory.submonoid.membership -import group_theory.submonoid.center +import group_theory.submonoid.centralizer import algebra.group.conj import algebra.module.basic import order.atoms @@ -1383,6 +1383,9 @@ def _root_.group.comm_group_of_center_eq_top (h : center G = ⊤) : comm_group G .. (_ : group G) } variables {G} (H) + +section normalizer + /-- The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal. -/ @[to_additive "The `normalizer` of `H` is the largest subgroup of `G` inside which `H` is normal."] def normalizer : subgroup G := @@ -1495,6 +1498,30 @@ lemma normalizer_condition.normal_of_coatom (hnc : normalizer_condition G) (hmax : is_coatom H) : H.normal := normalizer_eq_top.mp (hmax.2 _ (hnc H (lt_top_iff_ne_top.mpr hmax.1))) +end normalizer + +section centralizer + +/-- The `centralizer` of `H` is the subgroup of `g : G` commuting with every `h : H`. -/ +@[to_additive "The `centralizer` of `H` is the additive subgroup of `g : G` commuting with +every `h : H`."] +def centralizer : subgroup G := +{ carrier := set.centralizer H, + inv_mem' := λ g, set.inv_mem_centralizer, + .. submonoid.centralizer ↑H } + +@[to_additive] lemma mem_centralizer_iff {g : G} : g ∈ H.centralizer ↔ ∀ h ∈ H, h * g = g * h := +iff.rfl + +@[to_additive] lemma mem_centralizer_iff_commutator_eq_one {g : G} : + g ∈ H.centralizer ↔ ∀ h ∈ H, h * g * h⁻¹ * g⁻¹ = 1 := +by simp only [mem_centralizer_iff, mul_inv_eq_iff_eq_mul, one_mul] + +@[to_additive] lemma centralizer_top : centralizer ⊤ = center G := +set_like.ext' (set.centralizer_univ G) + +end centralizer + /-- Commutivity of a subgroup -/ structure is_commutative : Prop := (is_comm : _root_.is_commutative H (*)) diff --git a/src/group_theory/submonoid/centralizer.lean b/src/group_theory/submonoid/centralizer.lean new file mode 100644 index 0000000000000..18db3994dffc1 --- /dev/null +++ b/src/group_theory/submonoid/centralizer.lean @@ -0,0 +1,146 @@ +/- +Copyright (c) 2021 Thomas Browning. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Browning +-/ +import group_theory.submonoid.center + +/-! +# Centralizers of magmas and monoids + +## Main definitions + +* `set.centralizer`: the center of a magma +* `submonoid.centralizer`: the center of a monoid +* `set.add_centralizer`: the center of an additive magma +* `add_submonoid.centralizer`: the center of an additive monoid + +We provide `subgroup.centralizer`, `add_subgroup.centralizer` in other files. +-/ + +variables {M : Type*} {S T : set M} + +namespace set + +variables (S) + +/-- The centralizer of a subset of a magma. -/ +@[to_additive add_centralizer /-" The centralizer of a subset of an additive magma. "-/] +def centralizer [has_mul M] : set M := {c | ∀ m ∈ S, m * c = c * m} + +variables {S} + +@[to_additive mem_add_centralizer] +lemma mem_centralizer_iff [has_mul M] {c : M} : c ∈ centralizer S ↔ ∀ m ∈ S, m * c = c * m := +iff.rfl + +@[to_additive decidable_mem_add_centralizer] +instance decidable_mem_centralizer [has_mul M] [decidable_eq M] [fintype M] + [decidable_pred (∈ S)] : decidable_pred (∈ centralizer S) := +λ _, decidable_of_iff' _ (mem_centralizer_iff) + +variables (S) + +@[simp, to_additive zero_mem_add_centralizer] +lemma one_mem_centralizer [mul_one_class M] : (1 : M) ∈ centralizer S := +by simp [mem_centralizer_iff] + +@[simp] +lemma zero_mem_centralizer [mul_zero_class M] : (0 : M) ∈ centralizer S := +by simp [mem_centralizer_iff] + +variables {S} {a b : M} + +@[simp, to_additive add_mem_add_centralizer] +lemma mul_mem_centralizer [semigroup M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : + a * b ∈ centralizer S := +λ g hg, by rw [mul_assoc, ←hb g hg, ← mul_assoc, ha g hg, mul_assoc] + +@[simp, to_additive neg_mem_add_centralizer] +lemma inv_mem_centralizer [group M] (ha : a ∈ centralizer S) : a⁻¹ ∈ centralizer S := +λ g hg, by rw [mul_inv_eq_iff_eq_mul, mul_assoc, eq_inv_mul_iff_mul_eq, ha g hg] + +@[simp] +lemma add_mem_centralizer [distrib M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : + a + b ∈ centralizer S := +λ c hc, by rw [add_mul, mul_add, ha c hc, hb c hc] + +@[simp] +lemma neg_mem_centralizer [has_mul M] [has_distrib_neg M] (ha : a ∈ centralizer S) : + -a ∈ centralizer S := +λ c hc, by rw [mul_neg, ha c hc, neg_mul] + +@[simp] +lemma inv_mem_centralizer₀ [group_with_zero M] (ha : a ∈ centralizer S) : a⁻¹ ∈ centralizer S := +(eq_or_ne a 0).elim (λ h, by { rw [h, inv_zero], exact zero_mem_centralizer S }) + (λ ha0 c hc, by rw [mul_inv_eq_iff_eq_mul₀ ha0, mul_assoc, eq_inv_mul_iff_mul_eq₀ ha0, ha c hc]) + +@[simp, to_additive sub_mem_add_centralizer] +lemma div_mem_centralizer [group M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : + a / b ∈ centralizer S := +begin + rw [div_eq_mul_inv], + exact mul_mem_centralizer ha (inv_mem_centralizer hb), +end + +@[simp] +lemma div_mem_centralizer₀ [group_with_zero M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) : + a / b ∈ centralizer S := +begin + rw div_eq_mul_inv, + exact mul_mem_centralizer ha (inv_mem_centralizer₀ hb), +end + +@[to_additive add_centralizer_subset] +lemma centralizer_subset [has_mul M] (h : S ⊆ T) : centralizer T ⊆ centralizer S := +λ t ht s hs, ht s (h hs) + +variables (M) + +@[simp, to_additive add_centralizer_univ] +lemma centralizer_univ [has_mul M] : centralizer univ = center M := +subset.antisymm (λ a ha b, ha b (set.mem_univ b)) (λ a ha b hb, ha b) + +variables {M} (S) + +@[simp, to_additive add_centralizer_eq_univ] +lemma centralizer_eq_univ [comm_semigroup M] : centralizer S = univ := +subset.antisymm (subset_univ _) $ λ x hx y hy, mul_comm y x + +end set + +namespace submonoid +section +variables {M} [monoid M] (S) + +/-- The centralizer of a subset of a monoid `M`. -/ +@[to_additive "The centralizer of a subset of an additive monoid."] +def centralizer : submonoid M := +{ carrier := S.centralizer, + one_mem' := S.one_mem_centralizer, + mul_mem' := λ a b, set.mul_mem_centralizer } + +@[to_additive] lemma coe_centralizer : ↑(centralizer S) = S.centralizer := rfl + +variables {S} + +@[to_additive] lemma mem_centralizer_iff {z : M} : z ∈ centralizer S ↔ ∀ g ∈ S, g * z = z * g := +iff.rfl + +@[to_additive] instance decidable_mem_centralizer [decidable_eq M] [fintype M] + [decidable_pred (∈ S)] : decidable_pred (∈ centralizer S) := +λ _, decidable_of_iff' _ mem_centralizer_iff + +@[to_additive] +lemma centralizer_subset (h : S ⊆ T) : centralizer T ≤ centralizer S := +set.centralizer_subset h + +variables (M) + +@[simp, to_additive] +lemma centralizer_univ : centralizer set.univ = center M := +set_like.ext' (set.centralizer_univ M) + +end + +end submonoid