Conjugation in groups

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

Created on 2022-03-17.
Last modified on 2024-02-23.

module group-theory.conjugation where
Imports 
open import elementary-number-theory.integers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.retractions
open import foundation.sections
open import foundation.subtypes
open import foundation.transposition-identifications-along-retractions
open import foundation.transposition-identifications-along-sections
open import foundation.universe-levels

open import group-theory.group-actions
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.integer-powers-of-elements-groups
open import group-theory.isomorphisms-groups
open import group-theory.subsets-groups

Idea

Conjugation by an element x of a group G is the map y ↦ (xy)x⁻¹. This can be seen as a homomorphism G → G as well as a group action of G onto itself.

The delooping of the conjugation homomorphism is defined in structured-types.conjugation-pointed-types.md`.

Definitions

Conjugation

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

  equiv-conjugation-Group : (x : type-Group G) → type-Group G ≃ type-Group G
  equiv-conjugation-Group x =
    equiv-mul-Group' G (inv-Group G x) ∘e equiv-mul-Group G x

  conjugation-Group : (x : type-Group G) → type-Group G → type-Group G
  conjugation-Group x = map-equiv (equiv-conjugation-Group x)

  equiv-conjugation-Group' : (x : type-Group G) → type-Group G ≃ type-Group G
  equiv-conjugation-Group' x =
    equiv-mul-Group' G x ∘e equiv-mul-Group G (inv-Group G x)

  conjugation-Group' : (x : type-Group G) → type-Group G → type-Group G
  conjugation-Group' x = map-equiv (equiv-conjugation-Group' x)

The conjugation action of a group on itself

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

  conjugation-action-Group : action-Group G l1
  pr1 conjugation-action-Group = set-Group G
  pr1 (pr2 conjugation-action-Group) g = equiv-conjugation-Group G g
  pr2 (pr2 conjugation-action-Group) {g} {h} =
    eq-htpy-equiv
      ( λ x →
        ( ap-mul-Group G
          ( associative-mul-Group G g h x)
          ( distributive-inv-mul-Group G)) ∙
        ( inv
          ( associative-mul-Group G
            ( mul-Group G g (mul-Group G h x))
            ( inv-Group G h)
            ( inv-Group G g))) ∙
        ( ap
          ( mul-Group' G (inv-Group G g))
          ( associative-mul-Group G g
            ( mul-Group G h x)
            ( inv-Group G h))))

The predicate on subsets of groups of being closed under conjugation

module _
  {l1 l2 : Level} (G : Group l1) (S : subset-Group l2 G)
  where

  is-closed-under-conjugation-subset-Group : UU (l1 ⊔ l2)
  is-closed-under-conjugation-subset-Group =
    (x y : type-Group G) →
    is-in-subtype S y → is-in-subtype S (conjugation-Group G x y)

Properties

Laws for conjugation and multiplication

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

  conjugation-unit-Group :
    (x : type-Group G) → conjugation-Group G x (unit-Group G) ＝ unit-Group G
  conjugation-unit-Group x =
    ( ap (mul-Group' G (inv-Group G x)) (right-unit-law-mul-Group G x)) ∙
    ( right-inverse-law-mul-Group G x)

  compute-conjugation-unit-Group :
    conjugation-Group G (unit-Group G) ~ id
  compute-conjugation-unit-Group x =
    ( ap-mul-Group G (left-unit-law-mul-Group G x) (inv-unit-Group G)) ∙
    ( right-unit-law-mul-Group G x)

  compute-conjugation-mul-Group :
    (x y : type-Group G) →
    conjugation-Group G (mul-Group G x y) ~
    (conjugation-Group G x ∘ conjugation-Group G y)
  compute-conjugation-mul-Group x y z =
    ( ap-mul-Group G
      ( associative-mul-Group G x y z)
      ( distributive-inv-mul-Group G)) ∙
    ( inv
      ( associative-mul-Group G
        ( mul-Group G x (mul-Group G y z))
        ( inv-Group G y)
        ( inv-Group G x))) ∙
    ( ap
      ( mul-Group' G (inv-Group G x))
      ( associative-mul-Group G x (mul-Group G y z) (inv-Group G y)))

  compute-conjugation-mul-Group' :
    (x y : type-Group G) →
    conjugation-Group' G (mul-Group G x y) ~
    ( conjugation-Group' G y ∘ conjugation-Group' G x)
  compute-conjugation-mul-Group' x y z =
    ( ap
      ( mul-Group' G (mul-Group G x y))
      ( ( ap (mul-Group' G z) (distributive-inv-mul-Group G)) ∙
        ( associative-mul-Group G
          ( inv-Group G y)
          ( inv-Group G x)
          ( z)))) ∙
    ( associative-mul-Group G
      ( inv-Group G y)
      ( left-div-Group G x z)
      ( mul-Group G x y)) ∙
    ( ap
      ( left-div-Group G y)
      ( inv (associative-mul-Group G (left-div-Group G x z) x y))) ∙
    ( inv
      ( associative-mul-Group G
        ( inv-Group G y)
        ( conjugation-Group' G x z)
        ( y)))

  htpy-conjugation-Group :
    (x : type-Group G) →
    conjugation-Group' G x ~ conjugation-Group G (inv-Group G x)
  htpy-conjugation-Group x y =
    ap
      ( mul-Group G (mul-Group G (inv-Group G x) y))
      ( inv (inv-inv-Group G x))

  htpy-conjugation-Group' :
    (x : type-Group G) →
    conjugation-Group G x ~ conjugation-Group' G (inv-Group G x)
  htpy-conjugation-Group' x y =
    ap
      ( mul-Group' G (inv-Group G x))
      ( ap (mul-Group' G y) (inv (inv-inv-Group G x)))

  right-conjugation-law-mul-Group :
    (x y : type-Group G) →
    mul-Group G (inv-Group G x) (conjugation-Group G x y) ＝
    right-div-Group G y x
  right-conjugation-law-mul-Group x y =
    inv
      ( transpose-eq-mul-Group' G
        ( inv (associative-mul-Group G x y (inv-Group G x))))

  right-conjugation-law-mul-Group' :
    (x y : type-Group G) →
    mul-Group G x (conjugation-Group' G x y) ＝
    mul-Group G y x
  right-conjugation-law-mul-Group' x y =
    ( ap
      ( mul-Group G x)
      ( associative-mul-Group G (inv-Group G x) y x)) ∙
    ( is-section-left-div-Group G x (mul-Group G y x))

  left-conjugation-law-mul-Group :
    (x y : type-Group G) →
    mul-Group G (conjugation-Group G x y) x ＝ mul-Group G x y
  left-conjugation-law-mul-Group x y =
    ( associative-mul-Group G (mul-Group G x y) (inv-Group G x) x) ∙
    ( ap
      ( mul-Group G (mul-Group G x y))
      ( left-inverse-law-mul-Group G x)) ∙
    ( right-unit-law-mul-Group G (mul-Group G x y))

  left-conjugation-law-mul-Group' :
    (x y : type-Group G) →
    mul-Group G (conjugation-Group' G x y) (inv-Group G x) ＝
    left-div-Group G x y
  left-conjugation-law-mul-Group' x y =
    is-retraction-right-div-Group G x (mul-Group G (inv-Group G x) y)

  distributive-conjugation-mul-Group :
    (x y z : type-Group G) →
    conjugation-Group G x (mul-Group G y z) ＝
    mul-Group G (conjugation-Group G x y) (conjugation-Group G x z)
  distributive-conjugation-mul-Group x y z =
    ( ap
      ( mul-Group' G (inv-Group G x))
      ( ( inv (associative-mul-Group G x y z)) ∙
        ( ap
          ( mul-Group' G z)
          ( inv (is-section-right-div-Group G x (mul-Group G x y)))) ∙
        ( associative-mul-Group G
          ( conjugation-Group G x y)
          ( x)
          ( z)))) ∙
    ( associative-mul-Group G
      ( conjugation-Group G x y)
      ( mul-Group G x z)
      ( inv-Group G x))

  conjugation-inv-Group :
    (x y : type-Group G) →
    conjugation-Group G x (inv-Group G y) ＝
    inv-Group G (conjugation-Group G x y)
  conjugation-inv-Group x y =
    ( inv (inv-inv-Group G (conjugation-Group G x (inv-Group G y)))) ∙
    ( ap
      ( inv-Group G)
      ( ( distributive-inv-mul-Group G) ∙
        ( ap-mul-Group G
          ( inv-inv-Group G x)
          ( ( distributive-inv-mul-Group G) ∙
            ( ap
              ( mul-Group' G (inv-Group G x))
              ( inv-inv-Group G y)))) ∙
        ( inv (associative-mul-Group G x y ( inv-Group G x)))))

  conjugation-inv-Group' :
    (x y : type-Group G) →
    conjugation-Group' G x (inv-Group G y) ＝
    inv-Group G (conjugation-Group' G x y)
  conjugation-inv-Group' x y =
    ( ap (mul-Group' G x) (inv (distributive-inv-mul-Group G))) ∙
    ( ap
      ( mul-Group G (inv-Group G (mul-Group G y x)))
      ( inv (inv-inv-Group G x))) ∙
    ( inv
      ( distributive-inv-mul-Group G)) ∙
    ( ap
      ( inv-Group G)
      ( inv (associative-mul-Group G (inv-Group G x) y x)))

  conjugation-left-div-Group :
    (x y : type-Group G) →
    conjugation-Group G x (left-div-Group G x y) ＝
    right-div-Group G y x
  conjugation-left-div-Group x y =
    ap (λ y → right-div-Group G y x) (is-section-left-div-Group G x y)

  conjugation-left-div-Group' :
    (x y : type-Group G) →
    conjugation-Group G y (left-div-Group G x y) ＝
    right-div-Group G y x
  conjugation-left-div-Group' x y =
    ( ap
      ( λ z → right-div-Group G z y)
      ( inv (associative-mul-Group G y (inv-Group G x) y))) ∙
    ( is-retraction-right-div-Group G y (right-div-Group G y x))

  conjugation-right-div-Group :
    (x y : type-Group G) →
    conjugation-Group' G y (right-div-Group G x y) ＝
    left-div-Group G y x
  conjugation-right-div-Group x y =
    ( associative-mul-Group G
      ( inv-Group G y)
      ( right-div-Group G x y)
      ( y)) ∙
    ( ap (left-div-Group G y) (is-section-right-div-Group G y x))

  conjugation-right-div-Group' :
    (x y : type-Group G) →
    conjugation-Group' G x (right-div-Group G x y) ＝
    left-div-Group G y x
  conjugation-right-div-Group' x y =
    ap (mul-Group' G x) (is-retraction-left-div-Group G x (inv-Group G y))

  is-section-conjugation-inv-Group :
    (x : type-Group G) →
    ( conjugation-Group G x ∘ conjugation-Group G (inv-Group G x)) ~ id
  is-section-conjugation-inv-Group x y =
    ( ap
      ( mul-Group' G (inv-Group G x))
      ( ( ap (mul-Group G x) (associative-mul-Group G _ _ _)) ∙
        ( is-section-left-div-Group G x
          ( right-div-Group G y (inv-Group G x))))) ∙
    ( is-section-right-div-Group G (inv-Group G x) y)

  is-retraction-conjugation-inv-Group :
    (x : type-Group G) →
    ( conjugation-Group G (inv-Group G x) ∘ conjugation-Group G x) ~ id
  is-retraction-conjugation-inv-Group x y =
    ( ap
      ( mul-Group' G (inv-Group G (inv-Group G x)))
      ( ( ap (mul-Group G (inv-Group G x)) (associative-mul-Group G _ _ _)) ∙
        ( is-retraction-left-div-Group G x
          ( right-div-Group G y x)))) ∙
    ( is-retraction-right-div-Group G (inv-Group G x) y)

  transpose-eq-conjugation-Group :
    {x y z : type-Group G} →
    y ＝ conjugation-Group G (inv-Group G x) z → conjugation-Group G x y ＝ z
  transpose-eq-conjugation-Group {x} {y} {z} =
    eq-transpose-is-section
      ( conjugation-Group G x)
      ( conjugation-Group G (inv-Group G x))
      ( is-section-conjugation-inv-Group x)

  transpose-eq-conjugation-Group' :
    {x y z : type-Group G} →
    conjugation-Group G (inv-Group G x) y ＝ z → y ＝ conjugation-Group G x z
  transpose-eq-conjugation-Group' {x} {y} {z} =
    eq-transpose-is-section'
      ( conjugation-Group G x)
      ( conjugation-Group G (inv-Group G x))
      ( is-section-conjugation-inv-Group x)

  transpose-eq-conjugation-inv-Group :
    {x y z : type-Group G} →
    y ＝ conjugation-Group G x z → conjugation-Group G (inv-Group G x) y ＝ z
  transpose-eq-conjugation-inv-Group {x} {y} {z} =
    eq-transpose-is-retraction
      ( conjugation-Group G x)
      ( conjugation-Group G (inv-Group G x))
      ( is-retraction-conjugation-inv-Group x)

  transpose-eq-conjugation-inv-Group' :
    {x y z : type-Group G} →
    conjugation-Group G x y ＝ z → y ＝ conjugation-Group G (inv-Group G x) z
  transpose-eq-conjugation-inv-Group' {x} {y} {z} =
    eq-transpose-is-retraction'
      ( conjugation-Group G x)
      ( conjugation-Group G (inv-Group G x))
      ( is-retraction-conjugation-inv-Group x)

Conjugation by x is an automorphism of G

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

  conjugation-hom-Group : type-Group G → hom-Group G G
  pr1 (conjugation-hom-Group x) = conjugation-Group G x
  pr2 (conjugation-hom-Group x) = distributive-conjugation-mul-Group G x _ _

  conjugation-equiv-Group : type-Group G → equiv-Group G G
  pr1 (conjugation-equiv-Group x) = equiv-conjugation-Group G x
  pr2 (conjugation-equiv-Group x) = distributive-conjugation-mul-Group G x _ _

  conjugation-iso-Group : type-Group G → iso-Group G G
  conjugation-iso-Group x = iso-equiv-Group G G (conjugation-equiv-Group x)

  preserves-integer-powers-conjugation-Group :
    (k : ℤ) (g x : type-Group G) →
    conjugation-Group G g (integer-power-Group G k x) ＝
    integer-power-Group G k (conjugation-Group G g x)
  preserves-integer-powers-conjugation-Group k g =
    preserves-integer-powers-hom-Group G G (conjugation-hom-Group g) k

Any group homomorphism preserves conjugation

module _
  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  where

  preserves-conjugation-hom-Group :
    {x y : type-Group G} →
    map-hom-Group G H f (conjugation-Group G x y) ＝
    conjugation-Group H (map-hom-Group G H f x) (map-hom-Group G H f y)
  preserves-conjugation-hom-Group =
    ( preserves-right-div-hom-Group G H f) ∙
    ( ap (mul-Group' H _) (preserves-mul-hom-Group G H f))

Recent changes