Source: ProCGroups.NormalSubgroups.Framework
1import ProCGroups.FreeProC.Basic
3/-!
4# Closed normal closures and perfect subgroups
6This module defines noncommutative groups, the universal property of a closed normal closure, and
7perfect subgroups.
8-/
10noncomputable section
12namespace ProCGroups
14universe u
16/-- A group is noncommutative when its abstract commutator subgroup is nontrivial. -/
17def IsNoncommutativeGroup (G : Type u) [Group G] : Prop :=
18 commutator G ≠ ⊥
20namespace NormalSubgroups
22/-- The closed normal closure of a subset as a universal closed normal subgroup. -/
23def IsClosedNormalClosure {G : Type u} [Group G] [TopologicalSpace G]
24 (S : Set G) (N : Subgroup G) : Prop :=
25 N.Normal ∧ IsClosed (N : Set G) ∧ S ⊆ N ∧
26 ∀ M : Subgroup G, M.Normal → IsClosed (M : Set G) → S ⊆ M → N ≤ M
28/-- A subgroup is perfect when it is equal to its abstract commutator subgroup. -/
29def IsPerfectSubgroup {G : Type u} [Group G] (K : Subgroup G) : Prop :=
30 ⁅K, K⁆ = K
32end NormalSubgroups
33end ProCGroups