# Normal subgroups of concrete groups

Content created by Jonathan Prieto-Cubides, Egbert Rijke and Fredrik Bakke.

Created on 2022-07-10.

module group-theory.normal-subgroups-concrete-groups where

Imports
open import foundation.universe-levels

open import group-theory.concrete-group-actions
open import group-theory.concrete-groups
open import group-theory.subgroups-concrete-groups
open import group-theory.transitive-concrete-group-actions


## Idea

A normal subgroup is a fixed point of the conjugation action on the (large) set of all subgroups

## Definition

normal-subgroup-Concrete-Group :
{l1 : Level} (l2 : Level) (G : Concrete-Group l1) → UU (l1 ⊔ lsuc l2)
normal-subgroup-Concrete-Group l2 G =
(u : classifying-type-Concrete-Group G) →
subgroup-action-Concrete-Group l2 G u

module _
{l1 l2 : Level} (G : Concrete-Group l1)
(H : normal-subgroup-Concrete-Group l2 G)
where

subgroup-normal-subgroup-Concrete-Group : subgroup-Concrete-Group l2 G
subgroup-normal-subgroup-Concrete-Group = H (shape-Concrete-Group G)

action-normal-subgroup-Concrete-Group : action-Concrete-Group l2 G
action-normal-subgroup-Concrete-Group =
action-subgroup-Concrete-Group G subgroup-normal-subgroup-Concrete-Group

transitive-action-normal-subgroup-Concrete-Group :
transitive-action-Concrete-Group l2 G
transitive-action-normal-subgroup-Concrete-Group =
transitive-action-subgroup-Concrete-Group G
( subgroup-normal-subgroup-Concrete-Group)