Classical.Structures.Group.Centralizer¶
Centralizers¶
This is the Classical.Structures.Group.Centralizer module of the Agda Universal Algebra Library.
The centralizer C_G(N) of a subset N of a group G is the set of elements
that commute with every member of N. It is a subgroup, it is antitone in N,
and it is normal whenever N is.1
This module also proves the small commutator fact that drives subdirect irreducibility: two normal subgroups that meet trivially centralize each other.
For m ∈ M and n ∈ N the commutator n m n⁻¹ m⁻¹ lies in M (read it as
(n m n⁻¹) m⁻¹, and use normality of M) and in N (similarly, read n (m n⁻¹ m⁻¹)),
hence is trivial, which is exactly n m = m n.
The centralizer of a subset¶
module Centralizer {α ρ : Level} (𝒢 : Group α ρ) where private 𝑮 : Algebra {𝑆 = Sig-Group} α ρ 𝑮 = proj₁ 𝒢 open Setoid 𝔻[ 𝑮 ] using ( _≈_ ) renaming ( Carrier to G ; refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) open SetoidReasoning 𝔻[ 𝑮 ] open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; assoc-law ; idˡ-law ; idʳ-law ; invˡ-law ; invʳ-law ) open Conjugate 𝒢 using ( IsNormal ; conj-cong ; conj-∙-hom ; conj-conj⁻¹ ; conj-syntax) -- The centralizer of N: the elements commuting with every member of N. C[_] : Pred G ℓ → Pred G (α ⊔ ρ ⊔ ℓ) C[ N ] g = ∀ x → x ∈ N → g ∙ x ≈ x ∙ g -- Larger subsets have smaller centralizers. C-isAntitone : {M : Pred G ℓ} {N : Pred G ℓ'} → M ⊆ N → C[ N ] ⊆ C[ M ] C-isAntitone M⊆N g∈C x x∈M = g∈C x (M⊆N x∈M)
The centralizer is a subgroup. Closure under inversion is the only step with any
content: from g x = x g one gets g⁻¹ x = x g⁻¹ by applying g⁻¹ on the left
and right of both sides.
C-isSubgroup : (N : Pred G ℓ) → IsSubgroup 𝒢 C[ N ] C-isSubgroup N = mkIsSubgroup 𝒢 resp ∙-c ε-c ⁻¹-c where resp : C[ N ] Respects _≈_ resp {g} {g'} g≈g' g∈C x x∈N = begin g' ∙ x ≈˘⟨ ∙-cong g≈g' ≈refl ⟩ g ∙ x ≈⟨ g∈C x x∈N ⟩ x ∙ g ≈⟨ ∙-cong ≈refl g≈g' ⟩ x ∙ g' ∎ ε-c : ε ∈ C[ N ] ε-c x _ = ≈trans (idˡ-law x) (≈sym (idʳ-law x)) ∙-c : ∀ {g h} → g ∈ C[ N ] → h ∈ C[ N ] → g ∙ h ∈ C[ N ] ∙-c {g} {h} g∈C h∈C x x∈N = begin g ∙ h ∙ x ≈⟨ assoc-law g h x ⟩ g ∙ (h ∙ x) ≈⟨ ∙-cong ≈refl (h∈C x x∈N) ⟩ g ∙ (x ∙ h) ≈˘⟨ assoc-law g x h ⟩ g ∙ x ∙ h ≈⟨ ∙-cong (g∈C x x∈N) ≈refl ⟩ x ∙ g ∙ h ≈⟨ assoc-law x g h ⟩ x ∙ (g ∙ h) ∎ ⁻¹-c : ∀ {g} → g ∈ C[ N ] → g ⁻¹ ∈ C[ N ] ⁻¹-c {g} g∈C x x∈N = begin g ⁻¹ ∙ x ≈˘⟨ ∙-cong ≈refl (idʳ-law x) ⟩ g ⁻¹ ∙ (x ∙ ε) ≈˘⟨ ∙-cong ≈refl (∙-cong ≈refl (invʳ-law g)) ⟩ g ⁻¹ ∙ (x ∙ (g ∙ g ⁻¹)) ≈˘⟨ ∙-cong ≈refl (assoc-law x g (g ⁻¹)) ⟩ g ⁻¹ ∙ (x ∙ g ∙ g ⁻¹) ≈˘⟨ ∙-cong ≈refl (∙-cong (g∈C x x∈N) ≈refl) ⟩ g ⁻¹ ∙ (x ^ g) ≈⟨ ∙-cong ≈refl (assoc-law g x (g ⁻¹)) ⟩ g ⁻¹ ∙ (g ∙ (x ∙ g ⁻¹)) ≈˘⟨ assoc-law (g ⁻¹) g (x ∙ g ⁻¹) ⟩ (g ⁻¹ ∙ g) ∙ (x ∙ g ⁻¹) ≈⟨ ∙-cong (invˡ-law g) ≈refl ⟩ ε ∙ (x ∙ g ⁻¹) ≈⟨ idˡ-law (x ∙ g ⁻¹) ⟩ x ∙ g ⁻¹ ∎
The centralizer of a normal subgroup is normal: conjugating a centralizing element
by k still centralizes, because k⁻¹ x k is again in N, so g commutes with it,
and conjugating that equation by k gives what is wanted.
C-isNormal : {N : Pred G ℓ} → IsNormal N → IsNormal C[ N ] C-isNormal N-normal k {g} g∈C x x∈N = begin g ^ k ∙ x ≈˘⟨ ∙-cong ≈refl (conj-conj⁻¹ k x) ⟩ g ^ k ∙ (x ^ (k ⁻¹))^ k ≈˘⟨ conj-∙-hom k g (x ^ (k ⁻¹)) ⟩ (g ∙ x ^ (k ⁻¹))^ k ≈⟨ conj-cong k (g∈C (x ^ (k ⁻¹)) (N-normal (k ⁻¹) x∈N)) ⟩ (x ^ (k ⁻¹) ∙ g)^ k ≈⟨ conj-∙-hom k (x ^ (k ⁻¹)) g ⟩ (x ^ (k ⁻¹))^ k ∙ g ^ k ≈⟨ ∙-cong (conj-conj⁻¹ k x) ≈refl ⟩ x ∙ g ^ k ∎
Normal subgroups meeting trivially centralize each other¶
Two normal subgroups with trivial intersection commute elementwise: if M and N
are normal and meet at (ε), then every element of N centralizes M.
We formalize this standard fact in normals-centralize;
the proof is the classical commutator argument. Given n ∈ N and m ∈ M, the
commutator (n m n⁻¹) m⁻¹ lies in M by normality of M and in N by normality
of N, so the trivial-intersection hypothesis forces it to be ε, which is exactly
n m ≈ m n.
normals-centralize : {M : Pred G ℓ} {N : Pred G ℓ'} → IsSubgroup 𝒢 M → IsSubgroup 𝒢 N → IsNormal M → IsNormal N → (∀ {w} → w ∈ M → w ∈ N → w ≈ ε) -- M and N meet trivially → N ⊆ C[ M ] normals-centralize {M = M} {N} M-sg N-sg M-nrm N-nrm meet {n} n∈N m m∈M = commute where open IsSubgroup M-sg using () renaming ( ∙-closed to M∙ ; ⁻¹-closed to M⁻¹ ) open IsSubgroup N-sg using () renaming ( ∙-closed to N∙ ; ⁻¹-closed to N⁻¹ ; respects to N-resp ) -- The commutator, read as (n m n⁻¹) m⁻¹ ... w : G w = n ∙ m ∙ n ⁻¹ ∙ m ⁻¹ w∈M : w ∈ M w∈M = M∙ (M-nrm n m∈M) (M⁻¹ m∈M) -- ... and as n (m n⁻¹ m⁻¹). w≈ : w ≈ n ∙ (n ⁻¹) ^ m w≈ = begin n ∙ m ∙ n ⁻¹ ∙ m ⁻¹ ≈⟨ ∙-cong (assoc-law n m (n ⁻¹)) ≈refl ⟩ n ∙ (m ∙ n ⁻¹) ∙ m ⁻¹ ≈⟨ assoc-law n (m ∙ n ⁻¹) (m ⁻¹) ⟩ n ∙ (n ⁻¹) ^ m ∎ w∈N : w ∈ N w∈N = N-resp (≈sym w≈) (N∙ n∈N (N-nrm m (N⁻¹ n∈N))) w≈ε : w ≈ ε w≈ε = meet w∈M w∈N -- Cancelling m⁻¹ and then n⁻¹ from n m n⁻¹ m⁻¹ ≈ ε. step : n ∙ m ∙ n ⁻¹ ≈ m step = begin m ^ n ≈˘⟨ idʳ-law _ ⟩ m ^ n ∙ ε ≈˘⟨ ∙-cong ≈refl (invˡ-law m) ⟩ m ^ n ∙ (m ⁻¹ ∙ m) ≈˘⟨ assoc-law (m ^ n) (m ⁻¹) m ⟩ m ^ n ∙ m ⁻¹ ∙ m ≈⟨ ∙-cong w≈ε ≈refl ⟩ ε ∙ m ≈⟨ idˡ-law m ⟩ m ∎ commute : n ∙ m ≈ m ∙ n commute = begin n ∙ m ≈˘⟨ idʳ-law (n ∙ m) ⟩ n ∙ m ∙ ε ≈˘⟨ ∙-cong ≈refl (invˡ-law n) ⟩ n ∙ m ∙ (n ⁻¹ ∙ n) ≈˘⟨ assoc-law (n ∙ m) (n ⁻¹) n ⟩ m ^ n ∙ n ≈⟨ ∙-cong step ≈refl ⟩ m ∙ n ∎
-
Normality of centralizers is what Lemma 3.7 of the note Interval enforceable properties of finite groups (arXiv:1205.1927v4) uses: in a core-free parachute representation the centralizer of every nontrivial normal subgroup is trivial, whence the group is subdirectly irreducible with a nonabelian monolith. ↩