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 cores

module group-theory.perfect-cores where
Imports 
open import foundation.logical-equivalences
open import foundation.universe-levels

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

Idea

The perfect core of a group G is the largest perfect subgroup of G. That is, the subgroup perfect-core G satisfies the following universal property:

  (H : Subgroup G) → is-perfect-Subgroup G H ↔ H ⊆ perfect-core G

Definitions

The predicate of being a perfect core

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

  is-perfect-core-Subgroup : UUω
  is-perfect-core-Subgroup =
    {l : Level} (K : Subgroup l G) →
    is-perfect-Subgroup G K ↔ leq-Subgroup G K H

A wikidata identifier was not available for this concept.