Symmetric concrete groups

module group-theory.symmetric-concrete-groups where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.mere-equality
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.universe-levels

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

Idea

The symmetric concrete group of a set X is the connected component of the universe of sets at X.

Definition

module _
  {l : Level} (A : Set l)
  where

  classifying-type-symmetric-Concrete-Group : UU (lsuc l)
  classifying-type-symmetric-Concrete-Group =
    classifying-type-Automorphism-Group (Set-1-Type l) A

  shape-symmetric-Concrete-Group : classifying-type-symmetric-Concrete-Group
  shape-symmetric-Concrete-Group = shape-Automorphism-Group (Set-1-Type l) A

  symmetric-Concrete-Group : Concrete-Group (lsuc l)
  symmetric-Concrete-Group = Automorphism-Group (Set-1-Type l) A

Properties

Characterizing equality of the classifying type of the symmetric concrete groups

module _
  {l : Level} (A : Set l)
  where

  equiv-classifying-type-symmetric-Concrete-Group :
    (X Y : classifying-type-symmetric-Concrete-Group A) → UU l
  equiv-classifying-type-symmetric-Concrete-Group X Y =
    type-equiv-Set (pr1 X) (pr1 Y)

  type-symmetric-Concrete-Group : UU l
  type-symmetric-Concrete-Group =
    equiv-classifying-type-symmetric-Concrete-Group
      ( shape-symmetric-Concrete-Group A)
      ( shape-symmetric-Concrete-Group A)

  extensionality-classifying-type-symmetric-Concrete-Group :
    (X Y : classifying-type-symmetric-Concrete-Group A) →
    (X ＝ Y) ≃ equiv-classifying-type-symmetric-Concrete-Group X Y
  extensionality-classifying-type-symmetric-Concrete-Group X =
    extensionality-type-subtype
      ( λ Y → mere-eq-Prop Y A)
      ( pr2 X)
      ( id-equiv)
      ( extensionality-Set (pr1 X))

  equiv-eq-classifying-type-symmetric-Concrete-Group :
    (X Y : classifying-type-symmetric-Concrete-Group A) →
    (X ＝ Y) → equiv-classifying-type-symmetric-Concrete-Group X Y
  equiv-eq-classifying-type-symmetric-Concrete-Group X Y =
    map-equiv (extensionality-classifying-type-symmetric-Concrete-Group X Y)

  refl-equiv-eq-classifying-type-symmetric-Concrete-Group :
    (X : classifying-type-symmetric-Concrete-Group A) →
    equiv-eq-classifying-type-symmetric-Concrete-Group X X refl ＝ id-equiv
  refl-equiv-eq-classifying-type-symmetric-Concrete-Group X = refl

  preserves-mul-equiv-eq-classifying-type-symmetric-Concrete-Group :
    (X Y Z : classifying-type-symmetric-Concrete-Group A)
    (q : Y ＝ Z) (p : X ＝ Y) →
    equiv-eq-classifying-type-symmetric-Concrete-Group X Z (p ∙ q) ＝
    ( ( equiv-eq-classifying-type-symmetric-Concrete-Group Y Z q) ∘e
      ( equiv-eq-classifying-type-symmetric-Concrete-Group X Y p))
  preserves-mul-equiv-eq-classifying-type-symmetric-Concrete-Group
    X .X Z q refl =
    inv
      ( right-unit-law-equiv
        ( equiv-eq-classifying-type-symmetric-Concrete-Group X Z q))

Equivalent sets have isomorphic symmetric concrete groups