Perfect cores

Content created by Egbert Rijke and Fredrik Bakke.

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

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.

Recent changes