This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Perfect groups

module group-theory.perfect-groups where
Imports 
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.commutator-subgroups
open import group-theory.full-subgroups
open import group-theory.groups

Idea

A group G is said to be perfect if its commutator subgroup is a full subgroup.

Definitions

The predicate of being a perfect group

module _
  {l1 : Level} (G : Group l1)
  where

  is-perfect-prop-Group : Prop l1
  is-perfect-prop-Group = is-full-prop-Subgroup G (commutator-subgroup-Group G)

  is-perfect-Group : UU l1
  is-perfect-Group = type-Prop is-perfect-prop-Group

  is-prop-is-perfect-Group : is-prop is-perfect-Group
  is-prop-is-perfect-Group = is-prop-type-Prop is-perfect-prop-Group

A wikidata identifier was not available for this concept.