Perfect groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-16.
Last modified on 2023-11-09.

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.

Recent changes