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 subgroups

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

open import group-theory.groups
open import group-theory.perfect-groups
open import group-theory.subgroups

Idea

A subgroup H of a group G is a perfect subgroup if it is a perfect group on its own.

Definitions

The predicate of being a perfect subgroup

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

  is-perfect-prop-Subgroup : Prop (l1 ⊔ l2)
  is-perfect-prop-Subgroup = is-perfect-prop-Group (group-Subgroup G H)

  is-perfect-Subgroup : UU (l1 ⊔ l2)
  is-perfect-Subgroup = type-Prop is-perfect-prop-Subgroup

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

A wikidata identifier was not available for this concept.