Perfect subgroups

Content created by Fredrik Bakke and Ulrik Buchholtz.

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

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.

Recent changes