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 an equality-respecting subgroup, it is
antitone in N, and it is normal whenever N is; these are the three facts the
structure theory of parachute representations needs.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⁻¹, using normality of M) and in N (read it as n (m n⁻¹ m⁻¹),
using normality of N), 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 ( conj ; IsNormal ; conj-cong ; conj-∙-hom ; conj-conj⁻¹ ) -- 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 an equality-respecting subgroup. Closure under inversion is the
only step with any content: from g x = x g one gets g⁻¹ x = x g⁻¹ by conjugating
the equation with g⁻¹ on 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 ⁻¹ ∙ (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 conj k g ∙ x ≈˘⟨ ∙-cong ≈refl (conj-conj⁻¹ k x) ⟩ conj k g ∙ conj k (conj (k ⁻¹) x) ≈˘⟨ conj-∙-hom k g (conj (k ⁻¹) x) ⟩ conj k (g ∙ conj (k ⁻¹) x) ≈⟨ conj-cong k (g∈C (conj (k ⁻¹) x) (N-normal (k ⁻¹) x∈N)) ⟩ conj k (conj (k ⁻¹) x ∙ g) ≈⟨ conj-∙-hom k (conj (k ⁻¹) x) g ⟩ conj k (conj (k ⁻¹) x) ∙ conj k g ≈⟨ ∙-cong (conj-conj⁻¹ k x) ≈refl ⟩ x ∙ conj k g ∎
Normal subgroups meeting trivially centralize each other¶
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 ∙ conj m (n ⁻¹) w≈ = begin n ∙ m ∙ n ⁻¹ ∙ m ⁻¹ ≈⟨ ∙-cong (assoc-law n m (n ⁻¹)) ≈refl ⟩ n ∙ (m ∙ n ⁻¹) ∙ m ⁻¹ ≈⟨ assoc-law n (m ∙ n ⁻¹) (m ⁻¹) ⟩ n ∙ (m ∙ 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 n ∙ m ∙ n ⁻¹ ≈˘⟨ idʳ-law _ ⟩ n ∙ m ∙ n ⁻¹ ∙ ε ≈˘⟨ ∙-cong ≈refl (invˡ-law m) ⟩ n ∙ m ∙ n ⁻¹ ∙ (m ⁻¹ ∙ m) ≈˘⟨ assoc-law (n ∙ m ∙ n ⁻¹) (m ⁻¹) m ⟩ n ∙ 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 ⟩ n ∙ m ∙ n ⁻¹ ∙ n ≈⟨ ∙-cong step ≈refl ⟩ m ∙ n ∎
-
The FLRP program's Lemma 3.7 (
docs/papers/flrp/ieprops/,lemma-wjd-5): 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. See FLRP.Parachute. ↩