Normal closures of subgroups

Content created by Egbert Rijke, Fredrik Bakke and Gregor Perčič.

Created on 2023-08-07.
Last modified on 2024-04-11.

module group-theory.normal-closures-subgroups where
Imports 
open import foundation.dependent-pair-types
open import foundation.existential-quantification
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.conjugation
open import group-theory.groups
open import group-theory.normal-subgroups
open import group-theory.subgroups
open import group-theory.subgroups-generated-by-subsets-groups
open import group-theory.subsets-groups

open import order-theory.galois-connections-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders

Idea

Consider a subgroup H of a group G. The normal closure jH of G is the least normal subgroup of G that contains H. The normal closure of H is the subgroup generated by all the conjugates of elements of H.

In other words, the normal closure operation is the lower adjoint in a Galois connection between the large poset of normal subgroups of G and subgroups of G. The upper adjoint of this Galois connection is the inclusion function from normal subgroups to subgroups of G.

Note: The normal closure should not be confused with the normalizer of a subgroup, or with the normal core of a subgroup.

Definitions

The universal property of the normal closure

module _
  {l1 l2 l3 : Level} (G : Group l1) (H : Subgroup l2 G)
  (N : Normal-Subgroup l3 G)
  where

  is-normal-closure-Subgroup : UUω
  is-normal-closure-Subgroup =
    {l : Level} (M : Normal-Subgroup l G) →
    leq-Normal-Subgroup G N M ↔ leq-Subgroup G H (subgroup-Normal-Subgroup G M)

The construction of the normal closure

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

  generating-subset-normal-closure-Subgroup : subset-Group (l1 ⊔ l2) G
  generating-subset-normal-closure-Subgroup x =
    exists-structure-Prop
      ( type-Group G)
      ( λ y → fiber (conjugation-Group G y ∘ inclusion-Subgroup G H) x)

  contains-subgroup-generating-subset-normal-closure-Subgroup :
    subset-Subgroup G H ⊆ generating-subset-normal-closure-Subgroup
  contains-subgroup-generating-subset-normal-closure-Subgroup x h =
    unit-trunc-Prop
      ( unit-Group G , (x , h) , compute-conjugation-unit-Group G x)

  abstract
    is-closed-under-conjugation-generating-subset-normal-closure-Subgroup :
      is-closed-under-conjugation-subset-Group G
        generating-subset-normal-closure-Subgroup
    is-closed-under-conjugation-generating-subset-normal-closure-Subgroup
      x y s =
      apply-universal-property-trunc-Prop s
        ( generating-subset-normal-closure-Subgroup (conjugation-Group G x y))
        ( λ where
          ( z , h , refl) →
            unit-trunc-Prop
              ( mul-Group G x z ,
                h ,
                compute-conjugation-mul-Group G x z (pr1 h)))

  subgroup-normal-closure-Subgroup : Subgroup (l1 ⊔ l2) G
  subgroup-normal-closure-Subgroup =
    subgroup-subset-Group G generating-subset-normal-closure-Subgroup

  subset-normal-closure-Subgroup : subset-Group (l1 ⊔ l2) G
  subset-normal-closure-Subgroup =
    subset-Subgroup G subgroup-normal-closure-Subgroup

  is-in-normal-closure-Subgroup : type-Group G → UU (l1 ⊔ l2)
  is-in-normal-closure-Subgroup =
    is-in-Subgroup G subgroup-normal-closure-Subgroup

  is-closed-under-eq-normal-closure-Subgroup :
    {x y : type-Group G} → is-in-normal-closure-Subgroup x → x ＝ y →
    is-in-normal-closure-Subgroup y
  is-closed-under-eq-normal-closure-Subgroup =
    is-closed-under-eq-Subgroup G subgroup-normal-closure-Subgroup

  is-closed-under-eq-normal-closure-Subgroup' :
    {x y : type-Group G} → is-in-normal-closure-Subgroup y → x ＝ y →
    is-in-normal-closure-Subgroup x
  is-closed-under-eq-normal-closure-Subgroup' =
    is-closed-under-eq-Subgroup' G subgroup-normal-closure-Subgroup

  contains-unit-normal-closure-Subgroup :
    contains-unit-subset-Group G subset-normal-closure-Subgroup
  contains-unit-normal-closure-Subgroup =
    contains-unit-Subgroup G subgroup-normal-closure-Subgroup

  is-closed-under-multiplication-normal-closure-Subgroup :
    is-closed-under-multiplication-subset-Group G subset-normal-closure-Subgroup
  is-closed-under-multiplication-normal-closure-Subgroup =
    is-closed-under-multiplication-Subgroup G subgroup-normal-closure-Subgroup

  is-closed-under-inverses-normal-closure-Subgroup :
    is-closed-under-inverses-subset-Group G subset-normal-closure-Subgroup
  is-closed-under-inverses-normal-closure-Subgroup =
    is-closed-under-inverses-Subgroup G subgroup-normal-closure-Subgroup

  contains-generating-subset-normal-closure-Subgroup :
    generating-subset-normal-closure-Subgroup ⊆ subset-normal-closure-Subgroup
  contains-generating-subset-normal-closure-Subgroup =
    contains-subset-subgroup-subset-Group G
      generating-subset-normal-closure-Subgroup

  is-subgroup-generated-by-generating-subset-normal-closure-Subgroup :
    is-subgroup-generated-by-subset-Group G
      generating-subset-normal-closure-Subgroup
      subgroup-normal-closure-Subgroup
  is-subgroup-generated-by-generating-subset-normal-closure-Subgroup =
    is-subgroup-generated-by-subset-subgroup-subset-Group G
      generating-subset-normal-closure-Subgroup

  is-normal-subgroup-normal-closure-Subgroup :
    is-normal-Subgroup G subgroup-normal-closure-Subgroup
  is-normal-subgroup-normal-closure-Subgroup =
    is-normal-is-closed-under-conjugation-subgroup-subset-Group G
      generating-subset-normal-closure-Subgroup
      is-closed-under-conjugation-generating-subset-normal-closure-Subgroup

  normal-closure-Subgroup : Normal-Subgroup (l1 ⊔ l2) G
  pr1 normal-closure-Subgroup = subgroup-normal-closure-Subgroup
  pr2 normal-closure-Subgroup = is-normal-subgroup-normal-closure-Subgroup

  contains-subgroup-normal-closure-Subgroup :
    leq-Subgroup G H subgroup-normal-closure-Subgroup
  contains-subgroup-normal-closure-Subgroup =
    transitive-leq-subtype
      ( subset-Subgroup G H)
      ( generating-subset-normal-closure-Subgroup)
      ( subset-normal-closure-Subgroup)
      ( contains-subset-subgroup-subset-Group G
        generating-subset-normal-closure-Subgroup)
      ( contains-subgroup-generating-subset-normal-closure-Subgroup)

  forward-implication-is-normal-closure-normal-closure-Subgroup :
    {l : Level} (N : Normal-Subgroup l G) →
    leq-Normal-Subgroup G normal-closure-Subgroup N →
    leq-Subgroup G H (subgroup-Normal-Subgroup G N)
  forward-implication-is-normal-closure-normal-closure-Subgroup N u =
    transitive-leq-subtype
      ( subset-Subgroup G H)
      ( subset-normal-closure-Subgroup)
      ( subset-Normal-Subgroup G N)
      ( u)
      ( contains-subgroup-normal-closure-Subgroup)

  abstract
    contains-generating-subset-normal-closure-Normal-Subgroup :
      {l : Level} (N : Normal-Subgroup l G) →
      leq-Subgroup G H (subgroup-Normal-Subgroup G N) →
      generating-subset-normal-closure-Subgroup ⊆ subset-Normal-Subgroup G N
    contains-generating-subset-normal-closure-Normal-Subgroup N u x g =
      apply-universal-property-trunc-Prop g
        ( subset-Normal-Subgroup G N x)
        ( λ where
          ( z , (y , h) , refl) → is-normal-Normal-Subgroup G N z y (u y h))

  backward-implication-is-normal-closure-normal-closure-Subgroup :
    {l : Level} (N : Normal-Subgroup l G) →
    leq-Subgroup G H (subgroup-Normal-Subgroup G N) →
    leq-Normal-Subgroup G normal-closure-Subgroup N
  backward-implication-is-normal-closure-normal-closure-Subgroup N u =
    backward-implication
      ( is-subgroup-generated-by-generating-subset-normal-closure-Subgroup
        ( subgroup-Normal-Subgroup G N))
      ( contains-generating-subset-normal-closure-Normal-Subgroup N u)

  is-normal-closure-normal-closure-Subgroup :
    is-normal-closure-Subgroup G H normal-closure-Subgroup
  pr1 (is-normal-closure-normal-closure-Subgroup N) =
    forward-implication-is-normal-closure-normal-closure-Subgroup N
  pr2 (is-normal-closure-normal-closure-Subgroup N) =
    backward-implication-is-normal-closure-normal-closure-Subgroup N

The normal closure Galois connection

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

  preserves-order-normal-closure-Subgroup :
    {l2 l3 : Level} (H : Subgroup l2 G) (K : Subgroup l3 G) →
    leq-Subgroup G H K →
    leq-Normal-Subgroup G
      ( normal-closure-Subgroup G H)
      ( normal-closure-Subgroup G K)
  preserves-order-normal-closure-Subgroup H K u =
    backward-implication-is-normal-closure-normal-closure-Subgroup G H
      ( normal-closure-Subgroup G K)
      ( transitive-leq-subtype
        ( subset-Subgroup G H)
        ( subset-Subgroup G K)
        ( subset-normal-closure-Subgroup G K)
        ( contains-subgroup-normal-closure-Subgroup G K)
        ( u))

  normal-closure-subgroup-hom-Large-Poset :
    hom-Large-Poset
      ( λ l2 → l1 ⊔ l2)
      ( Subgroup-Large-Poset G)
      ( Normal-Subgroup-Large-Poset G)
  normal-closure-subgroup-hom-Large-Poset =
    make-hom-Large-Preorder
      ( normal-closure-Subgroup G)
      ( preserves-order-normal-closure-Subgroup)

  normal-closure-Galois-Connection :
    galois-connection-Large-Poset
      ( λ l2 → l1 ⊔ l2)
      ( λ l → l)
      ( Subgroup-Large-Poset G)
      ( Normal-Subgroup-Large-Poset G)
  normal-closure-Galois-Connection =
    make-galois-connection-Large-Poset
      ( normal-closure-subgroup-hom-Large-Poset)
      ( subgroup-normal-subgroup-hom-Large-Poset G)
      ( λ H N → is-normal-closure-normal-closure-Subgroup G H N)

See also

Recent changes