Normalizer subgroups

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

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

module group-theory.normalizer-subgroups where
Imports 
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.conjugation
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.subgroups
open import group-theory.subsets-groups

Idea

Consider a subgroup H of a group G. The normalizer subgroup Nᴳ(H) of G is the largest subgroup of G of which H is a normal subgroup. The normalizer subgroup consists of all elements g : G such that h ∈ H ⇔ (gh)g⁻¹ ∈ H for all h ∈ G. In other words, the normalizer subgroup consists of all elements g such that (gH)g⁻¹ ＝ H.

The weaker condition that (gH)g⁻¹ ⊆ H is not sufficient in the case of infinite groups. In this case, the group elements satisfying this weaker condition may not be closed under inverses.

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

Definitions

The universal property of the normalizer subgroup

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

  is-normalizer-Subgroup : UUω
  is-normalizer-Subgroup =
    {l : Level} (K : Subgroup l G) →
    ( {x y : type-Group G} →
      is-in-Subgroup G K x →
      is-in-Subgroup G H y →
      is-in-Subgroup G H (conjugation-Group G x y)) ↔
    leq-Subgroup G K N

The construction of the normalizer subgroup

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

  subset-normalizer-Subgroup : subset-Group (l1 ⊔ l2) G
  subset-normalizer-Subgroup x =
    implicit-Π-Prop
      ( type-Group G)
      ( λ y →
        iff-Prop
          ( subset-Subgroup G H y)
          ( subset-Subgroup G H (conjugation-Group G x y)))

  is-in-normalizer-Subgroup : type-Group G → UU (l1 ⊔ l2)
  is-in-normalizer-Subgroup =
    is-in-subtype subset-normalizer-Subgroup

  is-closed-under-eq-normalizer-Subgroup :
    {x y : type-Group G} →
    is-in-normalizer-Subgroup x → x ＝ y → is-in-normalizer-Subgroup y
  is-closed-under-eq-normalizer-Subgroup =
    is-closed-under-eq-subtype subset-normalizer-Subgroup

  restrict-conjugation-Subgroup :
    (x : type-Group G) → is-in-normalizer-Subgroup x →
    type-Subgroup G H → type-Subgroup G H
  pr1 (restrict-conjugation-Subgroup x u (y , h)) = conjugation-Group G x y
  pr2 (restrict-conjugation-Subgroup x u (y , h)) = forward-implication u h

  contains-unit-normalizer-Subgroup :
    contains-unit-subset-Group G subset-normalizer-Subgroup
  pr1 contains-unit-normalizer-Subgroup u =
    is-closed-under-eq-Subgroup' G H u (compute-conjugation-unit-Group G _)
  pr2 contains-unit-normalizer-Subgroup u =
    is-closed-under-eq-Subgroup G H u (compute-conjugation-unit-Group G _)

  is-closed-under-multiplication-normalizer-Subgroup :
    is-closed-under-multiplication-subset-Group G subset-normalizer-Subgroup
  pr1 (is-closed-under-multiplication-normalizer-Subgroup {x} {y} u v) w =
    is-closed-under-eq-Subgroup' G H
      ( forward-implication u (forward-implication v w))
      ( compute-conjugation-mul-Group G x y _)
  pr2 (is-closed-under-multiplication-normalizer-Subgroup {x} {y} u v) w =
    backward-implication v
      ( backward-implication u
        ( is-closed-under-eq-Subgroup G H w
          ( compute-conjugation-mul-Group G x y _)))

  is-closed-under-inverses-normalizer-Subgroup :
    is-closed-under-inverses-subset-Group G subset-normalizer-Subgroup
  pr1 (is-closed-under-inverses-normalizer-Subgroup {x} u {y}) h =
    backward-implication u
      ( is-closed-under-eq-Subgroup' G H h
        ( is-section-conjugation-inv-Group G x y))
  pr2 (is-closed-under-inverses-normalizer-Subgroup {x} u {y}) h =
    is-closed-under-eq-Subgroup G H
      ( forward-implication u h)
      ( is-section-conjugation-inv-Group G x y)

  normalizer-Subgroup : Subgroup (l1 ⊔ l2) G
  pr1 normalizer-Subgroup =
    subset-normalizer-Subgroup
  pr1 (pr2 normalizer-Subgroup) =
    contains-unit-normalizer-Subgroup
  pr1 (pr2 (pr2 normalizer-Subgroup)) =
    is-closed-under-multiplication-normalizer-Subgroup
  pr2 (pr2 (pr2 normalizer-Subgroup)) =
    is-closed-under-inverses-normalizer-Subgroup

  forward-implication-is-normalizer-normalizer-Subgroup :
    {l : Level} (K : Subgroup l G) →
    ( {x y : type-Group G} → is-in-Subgroup G K x →
      is-in-Subgroup G H y →
      is-in-Subgroup G H (conjugation-Group G x y)) →
    leq-Subgroup G K normalizer-Subgroup
  pr1 (forward-implication-is-normalizer-normalizer-Subgroup K u x k {y}) h =
    u k h
  pr2 (forward-implication-is-normalizer-normalizer-Subgroup K u x k {y}) h =
    is-closed-under-eq-Subgroup G H
      ( u (is-closed-under-inverses-Subgroup G K {x} k) h)
      ( is-retraction-conjugation-inv-Group G x y)

  backward-implication-is-normalizer-normalizer-Subgroup :
    {l : Level} (K : Subgroup l G) → leq-Subgroup G K normalizer-Subgroup →
    {x y : type-Group G} → is-in-Subgroup G K x →
    is-in-Subgroup G H y →
    is-in-Subgroup G H (conjugation-Group G x y)
  backward-implication-is-normalizer-normalizer-Subgroup K u {x} {y} k h =
    forward-implication (u x k) h

  is-normalizer-normalizer-Subgroup :
    is-normalizer-Subgroup G H normalizer-Subgroup
  pr1 (is-normalizer-normalizer-Subgroup K) =
    forward-implication-is-normalizer-normalizer-Subgroup K
  pr2 (is-normalizer-normalizer-Subgroup K) =
    backward-implication-is-normalizer-normalizer-Subgroup K

The inclusion of H into its normalizer Nᴳ(H)

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

  is-in-normalizer-is-in-type-Subgroup :
    (x : type-Group G) → is-in-Subgroup G H x → is-in-Subgroup G N x
  is-in-normalizer-is-in-type-Subgroup =
    forward-implication
      ( is-normalizer-G-H-N H)
      ( λ x' y' →
        is-closed-under-multiplication-Subgroup G H
          ( is-closed-under-multiplication-Subgroup G H x' y')
          ( is-closed-under-inverses-Subgroup G H x'))

  inclusion-is-normalizer-Subgroup : type-Subgroup G H → type-Subgroup G N
  inclusion-is-normalizer-Subgroup = tot is-in-normalizer-is-in-type-Subgroup

  hom-inclusion-is-normalizer-Subgroup :
    hom-Group (group-Subgroup G H) (group-Subgroup G N)
  pr1 hom-inclusion-is-normalizer-Subgroup =
    inclusion-is-normalizer-Subgroup
  pr2 hom-inclusion-is-normalizer-Subgroup =
    eq-type-subtype (subset-Subgroup G N) refl

See also

Recent changes