Subgroups of concrete groups

module group-theory.subgroups-concrete-groups where

open import foundation.0-connected-types
open import foundation.0-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.faithful-maps
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.structure-identity-principle
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.concrete-group-actions
open import group-theory.concrete-groups
open import group-theory.equivalences-concrete-group-actions
open import group-theory.homomorphisms-concrete-groups
open import group-theory.orbits-concrete-group-actions
open import group-theory.transitive-concrete-group-actions

open import structured-types.pointed-maps
open import structured-types.pointed-types

open import synthetic-homotopy-theory.functoriality-loop-spaces
open import synthetic-homotopy-theory.loop-spaces

Idea

A subgroup of a concrete group G is a pointed transitive G-set.

Definition

subgroup-action-Concrete-Group :
  {l1 : Level} (l2 : Level) (G : Concrete-Group l1) →
  classifying-type-Concrete-Group G → UU (l1 ⊔ lsuc l2)
subgroup-action-Concrete-Group l2 G u =
  Σ ( transitive-action-Concrete-Group l2 G)
    ( λ X → type-Set (action-transitive-action-Concrete-Group G X u))

subgroup-Concrete-Group :
  {l1 : Level} (l2 : Level) (G : Concrete-Group l1) → UU (l1 ⊔ lsuc l2)
subgroup-Concrete-Group l2 G =
  subgroup-action-Concrete-Group l2 G (shape-Concrete-Group G)

module _
  {l1 l2 : Level} (G : Concrete-Group l1) (H : subgroup-Concrete-Group l2 G)
  where

  transitive-action-subgroup-Concrete-Group :
    transitive-action-Concrete-Group l2 G
  transitive-action-subgroup-Concrete-Group = pr1 H

  action-subgroup-Concrete-Group : action-Concrete-Group l2 G
  action-subgroup-Concrete-Group =
    action-transitive-action-Concrete-Group G
      transitive-action-subgroup-Concrete-Group

  coset-subgroup-Concrete-Group : Set l2
  coset-subgroup-Concrete-Group =
    action-subgroup-Concrete-Group (shape-Concrete-Group G)

  type-coset-subgroup-Concrete-Group : UU l2
  type-coset-subgroup-Concrete-Group = type-Set coset-subgroup-Concrete-Group

  is-transitive-action-subgroup-Concrete-Group :
    is-transitive-action-Concrete-Group G action-subgroup-Concrete-Group
  is-transitive-action-subgroup-Concrete-Group =
    is-transitive-transitive-action-Concrete-Group G
      transitive-action-subgroup-Concrete-Group

  mul-transitive-action-subgroup-Concrete-Group :
    type-Concrete-Group G → type-coset-subgroup-Concrete-Group →
    type-coset-subgroup-Concrete-Group
  mul-transitive-action-subgroup-Concrete-Group =
    mul-transitive-action-Concrete-Group G
      transitive-action-subgroup-Concrete-Group

  is-transitive-mul-transitive-action-subgroup-Concrete-Group :
    ( x y : type-coset-subgroup-Concrete-Group) →
    ∃ ( type-Concrete-Group G)
      ( λ g → mul-transitive-action-subgroup-Concrete-Group g x ＝ y)
  is-transitive-mul-transitive-action-subgroup-Concrete-Group =
    is-transitive-mul-transitive-action-Concrete-Group G
      transitive-action-subgroup-Concrete-Group

  classifying-type-subgroup-Concrete-Group : UU (l1 ⊔ l2)
  classifying-type-subgroup-Concrete-Group =
    orbit-action-Concrete-Group G action-subgroup-Concrete-Group

  unit-coset-subgroup-Concrete-Group : type-coset-subgroup-Concrete-Group
  unit-coset-subgroup-Concrete-Group = pr2 H

  shape-subgroup-Concrete-Group : classifying-type-subgroup-Concrete-Group
  pr1 shape-subgroup-Concrete-Group = shape-Concrete-Group G
  pr2 shape-subgroup-Concrete-Group = unit-coset-subgroup-Concrete-Group

  classifying-pointed-type-subgroup-Concrete-Group : Pointed-Type (l1 ⊔ l2)
  pr1 classifying-pointed-type-subgroup-Concrete-Group =
    classifying-type-subgroup-Concrete-Group
  pr2 classifying-pointed-type-subgroup-Concrete-Group =
    shape-subgroup-Concrete-Group

  is-connected-classifying-type-subgroup-Concrete-Group :
    is-0-connected classifying-type-subgroup-Concrete-Group
  is-connected-classifying-type-subgroup-Concrete-Group =
    is-transitive-action-subgroup-Concrete-Group

  classifying-inclusion-subgroup-Concrete-Group :
    classifying-type-subgroup-Concrete-Group →
    classifying-type-Concrete-Group G
  classifying-inclusion-subgroup-Concrete-Group = pr1

  preserves-shape-classifying-inclusion-subgroup-Concrete-Group :
    classifying-inclusion-subgroup-Concrete-Group
      shape-subgroup-Concrete-Group ＝
    shape-Concrete-Group G
  preserves-shape-classifying-inclusion-subgroup-Concrete-Group = refl

  classifying-pointed-inclusion-subgroup-Concrete-Group :
    classifying-pointed-type-subgroup-Concrete-Group →∗
    classifying-pointed-type-Concrete-Group G
  pr1 classifying-pointed-inclusion-subgroup-Concrete-Group =
    classifying-inclusion-subgroup-Concrete-Group
  pr2 classifying-pointed-inclusion-subgroup-Concrete-Group =
    preserves-shape-classifying-inclusion-subgroup-Concrete-Group

  is-0-map-classifying-inclusion-subgroup-Concrete-Group :
    is-0-map classifying-inclusion-subgroup-Concrete-Group
  is-0-map-classifying-inclusion-subgroup-Concrete-Group =
    is-0-map-pr1 (λ u → is-set-type-Set (action-subgroup-Concrete-Group u))

  is-faithful-classifying-inclusion-subgroup-Concrete-Group :
    is-faithful classifying-inclusion-subgroup-Concrete-Group
  is-faithful-classifying-inclusion-subgroup-Concrete-Group =
    is-faithful-is-0-map is-0-map-classifying-inclusion-subgroup-Concrete-Group

  type-subgroup-Concrete-Group : UU (l1 ⊔ l2)
  type-subgroup-Concrete-Group =
    type-Ω classifying-pointed-type-subgroup-Concrete-Group

  concrete-group-subgroup-Concrete-Group :
    Concrete-Group (l1 ⊔ l2)
  pr1 (pr1 concrete-group-subgroup-Concrete-Group) =
    classifying-pointed-type-subgroup-Concrete-Group
  pr2 (pr1 concrete-group-subgroup-Concrete-Group) =
    is-connected-classifying-type-subgroup-Concrete-Group
  pr2 concrete-group-subgroup-Concrete-Group =
    is-set-is-emb
      ( map-Ω
        ( classifying-pointed-type-subgroup-Concrete-Group)
        ( classifying-pointed-type-Concrete-Group G)
        ( classifying-pointed-inclusion-subgroup-Concrete-Group))
      ( is-emb-map-Ω
        ( classifying-pointed-type-subgroup-Concrete-Group)
        ( classifying-pointed-type-Concrete-Group G)
        ( classifying-pointed-inclusion-subgroup-Concrete-Group)
        ( is-faithful-classifying-inclusion-subgroup-Concrete-Group))
      ( is-set-type-Concrete-Group G)

  hom-inclusion-subgroup-Concrete-Group :
    hom-Concrete-Group concrete-group-subgroup-Concrete-Group G
  pr1 hom-inclusion-subgroup-Concrete-Group =
    classifying-inclusion-subgroup-Concrete-Group
  pr2 hom-inclusion-subgroup-Concrete-Group =
    preserves-shape-classifying-inclusion-subgroup-Concrete-Group

Properties

The type of subgroups of a group is a set

subtype-preserves-unit-coset-equiv-action-Concrete-Group :
  {l1 l2 l3 : Level} (G : Concrete-Group l1) (X : subgroup-Concrete-Group l2 G)
  (Y : subgroup-Concrete-Group l3 G) →
  subtype l3
    ( equiv-action-Concrete-Group G
      ( action-subgroup-Concrete-Group G X)
      ( action-subgroup-Concrete-Group G Y))
subtype-preserves-unit-coset-equiv-action-Concrete-Group G X Y e =
  Id-Prop
    ( coset-subgroup-Concrete-Group G Y)
    ( map-equiv-action-Concrete-Group G
      ( action-subgroup-Concrete-Group G X)
      ( action-subgroup-Concrete-Group G Y)
      ( e)
      ( unit-coset-subgroup-Concrete-Group G X))
    ( unit-coset-subgroup-Concrete-Group G Y)

equiv-subgroup-Concrete-Group :
  {l1 l2 l3 : Level} (G : Concrete-Group l1) → subgroup-Concrete-Group l2 G →
  subgroup-Concrete-Group l3 G → UU (l1 ⊔ l2 ⊔ l3)
equiv-subgroup-Concrete-Group G X Y =
  type-subtype
    ( subtype-preserves-unit-coset-equiv-action-Concrete-Group G X Y)

extensionality-subgroup-Concrete-Group :
  {l1 l2 : Level} (G : Concrete-Group l1) (X Y : subgroup-Concrete-Group l2 G) →
  (X ＝ Y) ≃ equiv-subgroup-Concrete-Group G X Y
extensionality-subgroup-Concrete-Group G X =
  extensionality-Σ
    ( λ {Y} y e →
      ( map-equiv
        ( e (shape-Concrete-Group G))
        ( unit-coset-subgroup-Concrete-Group G X)) ＝
      ( y))
    ( id-equiv-action-Concrete-Group G (action-subgroup-Concrete-Group G X))
    ( refl)
    ( extensionality-transitive-action-Concrete-Group G
      ( transitive-action-subgroup-Concrete-Group G X))
    ( λ x → id-equiv)

is-set-subgroup-Concrete-Group :
  {l1 l2 : Level} (G : Concrete-Group l1) →
  is-set (subgroup-Concrete-Group l2 G)
is-set-subgroup-Concrete-Group G X Y =
  is-prop-equiv
    ( extensionality-subgroup-Concrete-Group G X Y)
    ( λ e f →
      is-proof-irrelevant-is-prop
        ( is-set-type-subtype
          ( subtype-preserves-unit-coset-equiv-action-Concrete-Group G X Y)
          ( is-set-equiv-action-Concrete-Group G
            ( action-subgroup-Concrete-Group G X)
            ( action-subgroup-Concrete-Group G Y))
          ( e)
          ( f))
        ( eq-type-subtype
          ( subtype-preserves-unit-coset-equiv-action-Concrete-Group G X Y)
          ( eq-htpy-equiv-action-Concrete-Group G
            ( action-subgroup-Concrete-Group G X)
            ( action-subgroup-Concrete-Group G Y)
            ( pr1 e)
            ( pr1 f)
            ( htpy-exists-equiv-transitive-action-Concrete-Group G
              ( transitive-action-subgroup-Concrete-Group G X)
              ( transitive-action-subgroup-Concrete-Group G Y)
              ( pr1 e)
              ( pr1 f)
              ( intro-∃
                ( unit-coset-subgroup-Concrete-Group G X)
                ( pr2 e ∙ inv (pr2 f)))))))