ProCGroups.NormalSubgroups.Framework

3 Definition

This module proves the universal-property part of the construction. It packages finite-stage data into completed maps and shows the required extension and uniqueness statements.

Open this file on GitHub

import

ProCGroups.FreeProC.Basic

Imported by

Definition ProCGroups.IsNoncommutativeGroup GitHub

def IsNoncommutativeGroup (G : Type u) [Group G] : Prop :=
  commutator G ≠ ⊥

A group is noncommutative when its abstract commutator subgroup is nontrivial.

Definition ProCGroups.NormalSubgroups.IsClosedNormalClosure GitHub

def IsClosedNormalClosure {G : Type u} [Group G] [TopologicalSpace G]
    (S : Set G) (N : Subgroup G) : Prop :=
  N.Normal ∧ IsClosed (N : Set G) ∧ S ⊆ N ∧
    ∀ M : Subgroup G, M.Normal → IsClosed (M : Set G) → S ⊆ M → N ≤ M

The closed normal closure of a subset as a universal closed normal subgroup.

Definition ProCGroups.NormalSubgroups.IsPerfectSubgroup GitHub

def IsPerfectSubgroup {G : Type u} [Group G] (K : Subgroup G) : Prop :=
  ⁅K, K⁆ = K

A subgroup is perfect when it is equal to its abstract commutator subgroup.

ProCGroups.NormalSubgroups.Framework

Declarations