# Quotient groups of concrete groups

Content created by Egbert Rijke, Jonathan Prieto-Cubides and Fredrik Bakke.

Created on 2022-07-18.

module group-theory.quotient-groups-concrete-groups where

Imports
open import foundation.0-connected-types
open import foundation.0-images-of-maps
open import foundation.1-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.mere-equality
open import foundation.propositional-truncations
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.equivalences-concrete-group-actions
open import group-theory.mere-equivalences-concrete-group-actions
open import group-theory.normal-subgroups-concrete-groups
open import group-theory.transitive-concrete-group-actions

open import higher-group-theory.higher-groups

open import structured-types.pointed-types

open import synthetic-homotopy-theory.loop-spaces


## Idea

Given a normal subgroup N of a concrete group G, the quotient group G/N is a concrete group that satisfies the universal property that for any concrete group homomorphism f : G → H such that the kernel of f is contained in N, then f extends uniquely to a group homomorphism G/N → H.

The quotient G/N can be constructed in several ways.

1. We can construct G/N as the type of G-sets merely equivalent to the coset action of N. Since this construction is reminiscent of the torsor construction of BG, we call this the standard construction of G/N.
2. We can construct G/N as the 0-image of the coset action N : BG → U. We call this the 0-image construction of G/N.

## Definitions

### The standard construction of G/N

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

classifying-type-quotient-Concrete-Group : UU (l1 ⊔ lsuc l2)
classifying-type-quotient-Concrete-Group =
Σ ( transitive-action-Concrete-Group l2 G)
( λ X →
mere-equiv-action-Concrete-Group G
( action-normal-subgroup-Concrete-Group G N)
( action-transitive-action-Concrete-Group G X))

shape-quotient-Concrete-Group :
classifying-type-quotient-Concrete-Group
pr1 shape-quotient-Concrete-Group =
transitive-action-normal-subgroup-Concrete-Group G N
pr2 shape-quotient-Concrete-Group =
refl-mere-equiv-action-Concrete-Group G
( action-normal-subgroup-Concrete-Group G N)

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

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

extensionality-classifying-type-quotient-Concrete-Group :
(u v : classifying-type-quotient-Concrete-Group) →
(u ＝ v) ≃ equiv-transitive-action-Concrete-Group G (pr1 u) (pr1 v)
extensionality-classifying-type-quotient-Concrete-Group u =
extensionality-type-subtype
( λ (X : transitive-action-Concrete-Group l2 G) →
mere-equiv-action-Concrete-Group-Prop G
( action-normal-subgroup-Concrete-Group G N)
( action-transitive-action-Concrete-Group G X))
( pr2 u)
( id-equiv-transitive-action-Concrete-Group G
( pr1 u))
( extensionality-transitive-action-Concrete-Group G (pr1 u))

is-0-connected-classifying-type-quotient-Concrete-Group :
is-0-connected classifying-type-quotient-Concrete-Group
is-0-connected-classifying-type-quotient-Concrete-Group =
is-0-connected-mere-eq
( shape-quotient-Concrete-Group)
( λ (pair u p) →
apply-universal-property-trunc-Prop p
( mere-eq-Prop
( shape-quotient-Concrete-Group)
( pair u p))
( λ e →
unit-trunc-Prop
( eq-type-subtype
( λ X →
mere-equiv-action-Concrete-Group-Prop G
( action-normal-subgroup-Concrete-Group G N)
( action-transitive-action-Concrete-Group G X))
( eq-type-subtype
( is-transitive-action-Concrete-Group-Prop G)
( eq-equiv-action-Concrete-Group G
( action-normal-subgroup-Concrete-Group G N)
( pr1 u)
( e))))))

is-1-type-classifying-type-quotient-Concrete-Group :
is-1-type classifying-type-quotient-Concrete-Group
is-1-type-classifying-type-quotient-Concrete-Group =
is-1-type-type-subtype
( λ X →
mere-equiv-action-Concrete-Group-Prop G
( action-normal-subgroup-Concrete-Group G N)
( action-transitive-action-Concrete-Group G X))
( is-1-type-transitive-action-Concrete-Group G)

is-set-type-quotient-Concrete-Group :
is-set type-quotient-Concrete-Group
is-set-type-quotient-Concrete-Group =
is-1-type-classifying-type-quotient-Concrete-Group
shape-quotient-Concrete-Group
shape-quotient-Concrete-Group

∞-group-quotient-Concrete-Group : ∞-Group (l1 ⊔ lsuc l2)
pr1 ∞-group-quotient-Concrete-Group =
classifying-pointed-type-quotient-Concrete-Group
pr2 ∞-group-quotient-Concrete-Group =
is-0-connected-classifying-type-quotient-Concrete-Group

concrete-group-quotient-Concrete-Group :
Concrete-Group (l1 ⊔ lsuc l2)
pr1 concrete-group-quotient-Concrete-Group =
∞-group-quotient-Concrete-Group
pr2 concrete-group-quotient-Concrete-Group =
is-set-type-quotient-Concrete-Group


### The 0-image construction of G/N

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

classifying-type-0-image-quotient-Concrete-Group : UU (l1 ⊔ lsuc l2)
classifying-type-0-image-quotient-Concrete-Group =
0-im (action-normal-subgroup-Concrete-Group G N)

shape-0-image-quotient-Concrete-Group :
classifying-type-0-image-quotient-Concrete-Group
shape-0-image-quotient-Concrete-Group =
unit-0-im
( action-normal-subgroup-Concrete-Group G N)
( shape-Concrete-Group G)

classifying-pointed-type-0-image-quotient-Concrete-Group :
Pointed-Type (l1 ⊔ lsuc l2)
pr1 classifying-pointed-type-0-image-quotient-Concrete-Group =
classifying-type-0-image-quotient-Concrete-Group
pr2 classifying-pointed-type-0-image-quotient-Concrete-Group =
shape-0-image-quotient-Concrete-Group

type-0-image-quotient-Concrete-Group : UU (l1 ⊔ lsuc l2)
type-0-image-quotient-Concrete-Group =
type-Ω classifying-pointed-type-0-image-quotient-Concrete-Group