Conjugation in higher groups

Content created by Egbert Rijke.

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

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

open import higher-group-theory.higher-groups
open import higher-group-theory.homomorphisms-higher-groups

open import structured-types.conjugation-pointed-types

open import synthetic-homotopy-theory.conjugation-loops

Idea

The conjugation homomorphism on an ∞-group G is the conjugation map of its classifying pointed type BG.

Definition

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

  conjugation-∞-Group : hom-∞-Group G G
  conjugation-∞-Group =
    conjugation-Pointed-Type (classifying-pointed-type-∞-Group G) g

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

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

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

  compute-map-conjugation-∞-Group :
    map-conjugation-Ω g ~ map-conjugation-∞-Group
  compute-map-conjugation-∞-Group =
    htpy-compute-action-on-loops-conjugation-Pointed-Type
      ( g)

Recent changes