Characteristic subgroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-19.
Last modified on 2023-10-22.

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))

See also

Recent changes