ProCGroups/NormalSubgroups/Framework.lean
1import ProCGroups.FreeProC.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/NormalSubgroups/Framework.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Closed normal subgroups
14Develops the normal-subgroup predicates used by the later compactness and algebraic comparison
15arguments.
16-/
18noncomputable section
20namespace ProCGroups
22universe u
24/-- A group is noncommutative when its abstract commutator subgroup is nontrivial. -/
25def IsNoncommutativeGroup (G : Type u) [Group G] : Prop :=
26 commutator G ≠ ⊥
28namespace NormalSubgroups
30/-- The closed normal closure of a subset as a universal closed normal subgroup. -/
31def IsClosedNormalClosure {G : Type u} [Group G] [TopologicalSpace G]
32 (S : Set G) (N : Subgroup G) : Prop :=
33 N.Normal ∧ IsClosed (N : Set G) ∧ S ⊆ N ∧
34 ∀ M : Subgroup G, M.Normal → IsClosed (M : Set G) → S ⊆ M → N ≤ M
36/-- A subgroup is perfect when it is equal to its abstract commutator subgroup. -/
37def IsPerfectSubgroup {G : Type u} [Group G] (K : Subgroup G) : Prop :=
38 ⁅K, K⁆ = K
40end NormalSubgroups
41end ProCGroups