Characteristic subgroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-19.

module group-theory.characteristic-subgroups where

Imports
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.images-of-group-homomorphisms
open import group-theory.isomorphisms-groups
open import group-theory.subgroups


Idea

A characteristic subgroup of a group G is a subgroup H of G such that f H ⊆ H for every isomorphism f : G ≅ G. The seemingly stronger condition, which asserts that f H ＝ H for every isomorphism f : G ≅ G is equivalent.

Note that any characteristic subgroup is normal, since the condition of being characteristic implies that conjugation x H ＝ H.

We also note that every subgroup which is defined for all groups, such as the commutator subgroup, is automatically characteristic as a consequence of the univalence axiom, and therefore also normal.

Definition

The predicate of being a characteristic subgroup

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

is-characteristic-prop-Subgroup : Prop (l1 ⊔ l2)
is-characteristic-prop-Subgroup =
Π-Prop
( iso-Group G G)
( λ f →
leq-prop-Subgroup G
( im-hom-Subgroup G G (hom-iso-Group G G f) H)
( H))


The stronger predicate of being a characteristic subgroup

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

is-characteristic-prop-Subgroup' : Prop (l1 ⊔ l2)
is-characteristic-prop-Subgroup' =
Π-Prop
( iso-Group G G)
( λ f →
has-same-elements-prop-Subgroup G
( im-hom-Subgroup G G (hom-iso-Group G G f) H)
( H))