Functoriality of quotient groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.
Last modified on 2024-04-25.

{-# OPTIONS --lossy-unification #-}

module group-theory.functoriality-quotient-groups where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.commuting-squares-of-group-homomorphisms
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.homomorphisms-groups-equipped-with-normal-subgroups
open import group-theory.normal-subgroups
open import group-theory.nullifying-group-homomorphisms
open import group-theory.quotient-groups

Idea

Consider a normal subgroup N of a group G and a normal subgroup M of a group H. Then any group homomorphism f : G → H satisfying the property that x ∈ N ⇒ f x ∈ M induces a group homomorphism g : G/N → H/M, which is the unique group homomorphism such that the square

         f
    G -------> H
    |          |
  q |          | q
    ∨          ∨
   G/N -----> H/M
         g

commutes.

Definitions

The quotient functor on groups

The functorial action of the quotient group construction

module _
  {l1 l2 l3 l4 : Level} (G : Group l1) (H : Group l2)
  (N : Normal-Subgroup l3 G) (M : Normal-Subgroup l4 H)
  (f : reflecting-hom-Group G H N M)
  where

  abstract
    unique-hom-quotient-Group :
      is-contr
        ( Σ ( hom-Group (quotient-Group G N) (quotient-Group H M))
            ( coherence-square-hom-Group G H
              ( quotient-Group G N)
              ( quotient-Group H M)
              ( hom-reflecting-hom-Group G H N M f)
              ( quotient-hom-Group G N)
              ( quotient-hom-Group H M)))
    unique-hom-quotient-Group =
      unique-mapping-property-quotient-Group G N
        ( quotient-Group H M)
        ( comp-nullifying-hom-reflecting-hom-Group G H
          ( quotient-Group H M)
          ( N)
          ( M)
          ( nullifying-quotient-hom-Group H M)
          ( f))

  abstract
    hom-quotient-Group : hom-Group (quotient-Group G N) (quotient-Group H M)
    hom-quotient-Group = pr1 (center unique-hom-quotient-Group)

    naturality-hom-quotient-Group :
      coherence-square-hom-Group G H
        ( quotient-Group G N)
        ( quotient-Group H M)
        ( hom-reflecting-hom-Group G H N M f)
        ( quotient-hom-Group G N)
        ( quotient-hom-Group H M)
        ( hom-quotient-Group)
    naturality-hom-quotient-Group =
      pr2 (center unique-hom-quotient-Group)

  map-hom-quotient-Group : type-quotient-Group G N → type-quotient-Group H M
  map-hom-quotient-Group =
    map-hom-Group (quotient-Group G N) (quotient-Group H M) hom-quotient-Group

The functorial action preserves the identity homomorphism

module _
  {l1 l2 : Level} (G : Group l1) (N : Normal-Subgroup l2 G)
  where

  abstract
    preserves-id-hom-quotient-Group' :
      (p : reflects-normal-subgroup-hom-Group G G N N (id-hom-Group G)) →
      hom-quotient-Group G G N N (id-reflecting-hom-Group' G N p) ＝
      id-hom-Group (quotient-Group G N)
    preserves-id-hom-quotient-Group' p =
      ap
        ( pr1)
        ( eq-is-contr'
          ( unique-mapping-property-quotient-Group G N
            ( quotient-Group G N)
            ( nullifying-quotient-hom-Group G N))
          ( hom-quotient-Group G G N N (id-reflecting-hom-Group' G N p) ,
            naturality-hom-quotient-Group G G N N
              ( id-reflecting-hom-Group' G N p))
          ( id-hom-Group (quotient-Group G N) ,
            refl-htpy))

  abstract
    preserves-id-hom-quotient-Group :
      hom-quotient-Group G G N N (id-reflecting-hom-Group G N) ＝
      id-hom-Group (quotient-Group G N)
    preserves-id-hom-quotient-Group =
      preserves-id-hom-quotient-Group'
        ( reflects-normal-subgroup-id-hom-Group G N)

The functorial action preserves composition

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  (G : Group l1) (H : Group l2) (K : Group l3)
  (L : Normal-Subgroup l4 G)
  (M : Normal-Subgroup l5 H)
  (N : Normal-Subgroup l6 K)
  where

  abstract
    preserves-comp-hom-quotient-Group' :
      (g : reflecting-hom-Group H K M N)
      (f : reflecting-hom-Group G H L M)
      (p :
        reflects-normal-subgroup-hom-Group G K L N
          ( hom-comp-reflecting-hom-Group G H K L M N g f)) →
      hom-quotient-Group G K L N
        ( comp-reflecting-hom-Group' G H K L M N g f p) ＝
      comp-hom-Group
        ( quotient-Group G L)
        ( quotient-Group H M)
        ( quotient-Group K N)
        ( hom-quotient-Group H K M N g)
        ( hom-quotient-Group G H L M f)
    preserves-comp-hom-quotient-Group' g f p =
      ap
        ( pr1)
        ( eq-is-contr'
          ( unique-mapping-property-quotient-Group G L
            ( quotient-Group K N)
            ( comp-nullifying-hom-reflecting-hom-Group G K
              ( quotient-Group K N)
              ( L)
              ( N)
              ( nullifying-quotient-hom-Group K N)
              ( comp-reflecting-hom-Group' G H K L M N g f p)))
          ( ( hom-quotient-Group G K L N
              ( comp-reflecting-hom-Group' G H K L M N g f p)) ,
            ( naturality-hom-quotient-Group G K L N
              ( comp-reflecting-hom-Group' G H K L M N g f p)))
          ( comp-hom-Group
            ( quotient-Group G L)
            ( quotient-Group H M)
            ( quotient-Group K N)
            ( hom-quotient-Group H K M N g)
            ( hom-quotient-Group G H L M f) ,
            ( pasting-horizontal-coherence-square-maps
              ( map-reflecting-hom-Group G H L M f)
              ( map-reflecting-hom-Group H K M N g)
              ( map-quotient-hom-Group G L)
              ( map-quotient-hom-Group H M)
              ( map-quotient-hom-Group K N)
              ( map-hom-quotient-Group G H L M f)
              ( map-hom-quotient-Group H K M N g)
              ( naturality-hom-quotient-Group G H L M f)
              ( naturality-hom-quotient-Group H K M N g))))

  abstract
    preserves-comp-hom-quotient-Group :
      (g : reflecting-hom-Group H K M N)
      (f : reflecting-hom-Group G H L M) →
      hom-quotient-Group G K L N (comp-reflecting-hom-Group G H K L M N g f) ＝
      comp-hom-Group
        ( quotient-Group G L)
        ( quotient-Group H M)
        ( quotient-Group K N)
        ( hom-quotient-Group H K M N g)
        ( hom-quotient-Group G H L M f)
    preserves-comp-hom-quotient-Group g f =
      preserves-comp-hom-quotient-Group' g f
        ( reflects-normal-subgroup-comp-reflecting-hom-Group G H K L M N g f)

The quotient group functor

This functor remains to be formalized.

Recent changes