# Conjugation on concrete groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-07-19.

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)