Module

Framework.lean

Nyll.ProCGroups.NormalSubgroups.Framework

3 declarations indexed from sourceView source ↗

Module documentation

This module defines noncommutative groups, the universal property of a closed normal closure, and perfect subgroups.

Imports1

Imported by3

def

ProCGroups.IsNoncommutativeGroup

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups
universe u

Lean source · statement

def IsNoncommutativeGroup (G : Type u) [Group G] : Prop

def

ProCGroups.NormalSubgroups.IsClosedNormalClosure

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups
universe u
namespace NormalSubgroups

Lean source · statement

def IsClosedNormalClosure {G : Type u} [Group G] [TopologicalSpace G]
    (S : Set G) (N : Subgroup G) : Prop

def

ProCGroups.NormalSubgroups.IsPerfectSubgroup

Documentation

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

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace ProCGroups
universe u
namespace NormalSubgroups

Lean source · statement

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