Conjugation on concrete groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-07-19.
Last modified on 2023-11-04.

module group-theory.conjugation-concrete-groups where
Imports 
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.conjugation
open import group-theory.homomorphisms-concrete-groups

open import higher-group-theory.conjugation

Idea

The conjugation operation on a concrete group G can be seen as a homomorphism of concrete groups and as a concrete group action.

Note that the delooping of the conjugation homomorphism can be defined directly for pointed types, which applies also to the case of ∞-groups.

Definitions

The conjugation homomorphism on concrete groups

module _
  {l : Level} (G : Concrete-Group l) (g : type-Concrete-Group G)
  where

  conjugation-Concrete-Group : hom-Concrete-Group G G
  conjugation-Concrete-Group = conjugation-∞-Group (∞-group-Concrete-Group G) g

  classifying-map-conjugation-Concrete-Group :
    classifying-type-Concrete-Group G → classifying-type-Concrete-Group G
  classifying-map-conjugation-Concrete-Group =
    classifying-map-hom-Concrete-Group G G conjugation-Concrete-Group

  preserves-point-classifying-map-conjugation-Concrete-Group :
    classifying-map-conjugation-Concrete-Group (shape-Concrete-Group G) ＝
    shape-Concrete-Group G
  preserves-point-classifying-map-conjugation-Concrete-Group =
    preserves-point-classifying-map-hom-Concrete-Group G G
      ( conjugation-Concrete-Group)

  map-conjugation-Concrete-Group :
    type-Concrete-Group G → type-Concrete-Group G
  map-conjugation-Concrete-Group =
    map-hom-Concrete-Group G G conjugation-Concrete-Group

  compute-map-conjugation-Concrete-Group :
    conjugation-Group' (group-Concrete-Group G) g ~
    map-conjugation-Concrete-Group
  compute-map-conjugation-Concrete-Group x =
    ( assoc (inv g) x g) ∙
    ( compute-map-conjugation-∞-Group (∞-group-Concrete-Group G) g x)

Recent changes