Automorphism groups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Eléonore Mangel.

Created on 2022-04-13.
Last modified on 2024-01-31.

module group-theory.automorphism-groups where
Imports 
open import foundation.0-connected-types
open import foundation.1-types
open import foundation.connected-components
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.propositional-truncations
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.equivalences-concrete-groups

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

open import structured-types.pointed-types

Idea

The automorphim group of a : A is the group of symmetries of a in A.

Definitions

Automorphism ∞-groups of a type

module _
  {l : Level} (A : UU l) (a : A)
  where

  classifying-type-Automorphism-∞-Group : UU l
  classifying-type-Automorphism-∞-Group = connected-component A a

  shape-Automorphism-∞-Group : classifying-type-Automorphism-∞-Group
  pr1 shape-Automorphism-∞-Group = a
  pr2 shape-Automorphism-∞-Group = unit-trunc-Prop refl

  classifying-pointed-type-Automorphism-∞-Group : Pointed-Type l
  pr1 classifying-pointed-type-Automorphism-∞-Group =
    classifying-type-Automorphism-∞-Group
  pr2 classifying-pointed-type-Automorphism-∞-Group =
    shape-Automorphism-∞-Group

  is-0-connected-classifying-type-Automorphism-∞-Group :
    is-0-connected classifying-type-Automorphism-∞-Group
  is-0-connected-classifying-type-Automorphism-∞-Group =
    is-0-connected-connected-component A a

  Automorphism-∞-Group : ∞-Group l
  pr1 Automorphism-∞-Group = classifying-pointed-type-Automorphism-∞-Group
  pr2 Automorphism-∞-Group =
    is-0-connected-classifying-type-Automorphism-∞-Group

Automorphism groups of objects in a 1-type

module _
  {l : Level} (A : 1-Type l) (a : type-1-Type A)
  where

  classifying-type-Automorphism-Group : UU l
  classifying-type-Automorphism-Group =
    classifying-type-Automorphism-∞-Group (type-1-Type A) a

  shape-Automorphism-Group : classifying-type-Automorphism-Group
  shape-Automorphism-Group = shape-Automorphism-∞-Group (type-1-Type A) a

  Automorphism-Group : Concrete-Group l
  pr1 Automorphism-Group = Automorphism-∞-Group (type-1-Type A) a
  pr2 Automorphism-Group =
    is-trunc-connected-component
      ( type-1-Type A)
      ( a)
      ( is-1-type-type-1-Type A)
      ( pair a (unit-trunc-Prop refl))
      ( pair a (unit-trunc-Prop refl))

  ∞-group-Automorphism-Group : ∞-Group l
  ∞-group-Automorphism-Group = ∞-group-Concrete-Group Automorphism-Group

Properties

Characerizing the identity type of Automorphism-∞-Group

module _
  {l : Level} {A : UU l} (a : A)
  where

  Eq-classifying-type-Automorphism-∞-Group :
    (X Y : classifying-type-Automorphism-∞-Group A a) → UU l
  Eq-classifying-type-Automorphism-∞-Group X Y = pr1 X ＝ pr1 Y

  refl-Eq-classifying-type-Automorphism-∞-Group :
    (X : classifying-type-Automorphism-∞-Group A a) →
    Eq-classifying-type-Automorphism-∞-Group X X
  refl-Eq-classifying-type-Automorphism-∞-Group X = refl

  is-torsorial-Eq-classifying-type-Automorphism-∞-Group :
    (X : classifying-type-Automorphism-∞-Group A a) →
    is-torsorial (Eq-classifying-type-Automorphism-∞-Group X)
  is-torsorial-Eq-classifying-type-Automorphism-∞-Group X =
    is-torsorial-Eq-subtype
      ( is-torsorial-Id (pr1 X))
      ( λ a → is-prop-type-trunc-Prop)
      ( pr1 X)
      ( refl)
      ( pr2 X)

  Eq-eq-classifying-type-Automorphism-∞-Group :
    (X Y : classifying-type-Automorphism-∞-Group A a) →
    (X ＝ Y) → Eq-classifying-type-Automorphism-∞-Group X Y
  Eq-eq-classifying-type-Automorphism-∞-Group X .X refl =
    refl-Eq-classifying-type-Automorphism-∞-Group X

  is-equiv-Eq-eq-classifying-type-Automorphism-∞-Group :
    (X Y : classifying-type-Automorphism-∞-Group A a) →
    is-equiv (Eq-eq-classifying-type-Automorphism-∞-Group X Y)
  is-equiv-Eq-eq-classifying-type-Automorphism-∞-Group X =
    fundamental-theorem-id
      ( is-torsorial-Eq-classifying-type-Automorphism-∞-Group X)
      ( Eq-eq-classifying-type-Automorphism-∞-Group X)

  extensionality-classifying-type-Automorphism-∞-Group :
    (X Y : classifying-type-Automorphism-∞-Group A a) →
    (X ＝ Y) ≃ Eq-classifying-type-Automorphism-∞-Group X Y
  pr1 (extensionality-classifying-type-Automorphism-∞-Group X Y) =
    Eq-eq-classifying-type-Automorphism-∞-Group X Y
  pr2 (extensionality-classifying-type-Automorphism-∞-Group X Y) =
    is-equiv-Eq-eq-classifying-type-Automorphism-∞-Group X Y

  eq-Eq-classifying-type-Automorphism-∞-Group :
    (X Y : classifying-type-Automorphism-∞-Group A a) →
    Eq-classifying-type-Automorphism-∞-Group X Y → X ＝ Y
  eq-Eq-classifying-type-Automorphism-∞-Group X Y =
    map-inv-equiv (extensionality-classifying-type-Automorphism-∞-Group X Y)

Characerizing the identity type of Automorphism-Group

module _
  {l : Level} (A : 1-Type l) (a : type-1-Type A)
  where

  Eq-classifying-type-Automorphism-Group :
    (X Y : classifying-type-Automorphism-Group A a) → UU l
  Eq-classifying-type-Automorphism-Group =
    Eq-classifying-type-Automorphism-∞-Group a

  refl-Eq-classifying-type-Automorphism-Group :
    (X : classifying-type-Automorphism-Group A a) →
    Eq-classifying-type-Automorphism-Group X X
  refl-Eq-classifying-type-Automorphism-Group =
    refl-Eq-classifying-type-Automorphism-∞-Group a

  is-torsorial-Eq-classifying-type-Automorphism-Group :
    (X : classifying-type-Automorphism-Group A a) →
    is-torsorial (Eq-classifying-type-Automorphism-Group X)
  is-torsorial-Eq-classifying-type-Automorphism-Group =
    is-torsorial-Eq-classifying-type-Automorphism-∞-Group a

  Eq-eq-classifying-type-Automorphism-Group :
    (X Y : classifying-type-Automorphism-Group A a) →
    (X ＝ Y) → Eq-classifying-type-Automorphism-Group X Y
  Eq-eq-classifying-type-Automorphism-Group X .X refl =
    refl-Eq-classifying-type-Automorphism-Group X

  is-equiv-Eq-eq-classifying-type-Automorphism-Group :
    (X Y : classifying-type-Automorphism-Group A a) →
    is-equiv (Eq-eq-classifying-type-Automorphism-Group X Y)
  is-equiv-Eq-eq-classifying-type-Automorphism-Group X =
    fundamental-theorem-id
      ( is-torsorial-Eq-classifying-type-Automorphism-Group X)
      ( Eq-eq-classifying-type-Automorphism-Group X)

  extensionality-classifying-type-Automorphism-Group :
    (X Y : classifying-type-Automorphism-Group A a) →
    (X ＝ Y) ≃ Eq-classifying-type-Automorphism-Group X Y
  pr1 (extensionality-classifying-type-Automorphism-Group X Y) =
    Eq-eq-classifying-type-Automorphism-Group X Y
  pr2 (extensionality-classifying-type-Automorphism-Group X Y) =
    is-equiv-Eq-eq-classifying-type-Automorphism-Group X Y

  eq-Eq-classifying-type-Automorphism-Group :
    (X Y : classifying-type-Automorphism-Group A a) →
    Eq-classifying-type-Automorphism-Group X Y → X ＝ Y
  eq-Eq-classifying-type-Automorphism-Group X Y =
    map-inv-equiv (extensionality-classifying-type-Automorphism-Group X Y)

Equal elements have equivalent automorphism ∞-groups

module _
  {l : Level} {A : UU l}
  where

  equiv-eq-Automorphism-∞-Group :
    {x y : A} (p : x ＝ y) →
    equiv-∞-Group (Automorphism-∞-Group A x) (Automorphism-∞-Group A y)
  equiv-eq-Automorphism-∞-Group refl =
    id-equiv-∞-Group (Automorphism-∞-Group A _)

Equal elements in a 1-type have isomorphic automorphism groups

module _
  {l : Level} (A : 1-Type l)
  where

  equiv-eq-Automorphism-Group :
    {x y : type-1-Type A} (p : x ＝ y) →
    equiv-Concrete-Group (Automorphism-Group A x) (Automorphism-Group A y)
  equiv-eq-Automorphism-Group refl =
    id-equiv-Concrete-Group (Automorphism-Group A _)

Recent changes