Quotients of abelian groups

{-# OPTIONS --lossy-unification #-}
module group-theory.quotients-abelian-groups where
Imports
open import foundation.binary-functoriality-set-quotients
open import foundation.dependent-pair-types
open import foundation.effective-maps-equivalence-relations
open import foundation.equivalences
open import foundation.functoriality-set-quotients
open import foundation.identity-types
open import foundation.propositions
open import foundation.reflecting-maps-equivalence-relations
open import foundation.set-quotients
open import foundation.sets
open import foundation.surjective-maps
open import foundation.universal-property-set-quotients
open import foundation.universe-levels

open import group-theory.abelian-groups
open import group-theory.groups
open import group-theory.homomorphisms-abelian-groups
open import group-theory.quotient-groups
open import group-theory.semigroups
open import group-theory.subgroups-abelian-groups

Idea

Given a subgroup B of an abelian group A, the quotient group is an abelian group A/B equipped with a group homomorphism q : A → A/B such that H ⊆ ker q, and such that q satisfies the universal abelian group with the property that any group homomorphism f : A → C such that B ⊆ ker f extends uniquely along q to a group homomorphism A/B → C.

Definitions

Group homomorphisms that nullify a subgroup, i.e., that contain a subgroup in their kernel

module _
  {l1 l2 l3 : Level} (A : Ab l1) (B : Ab l2)
  where

  nullifies-subgroup-hom-Ab-Prop :
    type-hom-Ab A B  Subgroup-Ab l3 A  Prop (l1  l2  l3)
  nullifies-subgroup-hom-Ab-Prop f H =
    nullifies-normal-subgroup-hom-Group-Prop
      ( group-Ab A)
      ( group-Ab B)
      ( f)
      ( normal-subgroup-Subgroup-Ab A H)

  nullifies-normal-subgroup-hom-Ab :
    type-hom-Ab A B  Subgroup-Ab l3 A  UU (l1  l2  l3)
  nullifies-normal-subgroup-hom-Ab f H =
    nullifies-normal-subgroup-hom-Group
      ( group-Ab A)
      ( group-Ab B)
      ( f)
      ( normal-subgroup-Subgroup-Ab A H)

  nullifying-hom-Ab : Subgroup-Ab l3 A  UU (l1  l2  l3)
  nullifying-hom-Ab H =
    nullifying-hom-Group
      ( group-Ab A)
      ( group-Ab B)
      ( normal-subgroup-Subgroup-Ab A H)

  hom-nullifying-hom-Ab :
    (H : Subgroup-Ab l3 A)  nullifying-hom-Ab H  type-hom-Ab A B
  hom-nullifying-hom-Ab H =
    hom-nullifying-hom-Group
      ( group-Ab A)
      ( group-Ab B)
      ( normal-subgroup-Subgroup-Ab A H)

  nullifies-nullifying-hom-Ab :
    (H : Subgroup-Ab l3 A) (f : nullifying-hom-Ab H) 
    nullifies-normal-subgroup-hom-Ab
      ( hom-nullifying-hom-Ab H f) H
  nullifies-nullifying-hom-Ab H =
    nullifies-nullifying-hom-Group
      ( group-Ab A)
      ( group-Ab B)
      ( normal-subgroup-Subgroup-Ab A H)

The universal property of quotient groups

precomp-nullifying-hom-Ab :
  {l1 l2 l3 l4 : Level} (A : Ab l1) (H : Subgroup-Ab l2 A)
  (B : Ab l3) (f : nullifying-hom-Ab A B H)
  (C : Ab l4)  type-hom-Ab B C  nullifying-hom-Ab A C H
precomp-nullifying-hom-Ab A H B f C =
  precomp-nullifying-hom-Group
    ( group-Ab A)
    ( normal-subgroup-Subgroup-Ab A H)
    ( group-Ab B)
    ( f)
    ( group-Ab C)

universal-property-quotient-Ab :
  {l1 l2 l3 : Level} (l : Level) (A : Ab l1)
  (H : Subgroup-Ab l2 A) (B : Ab l3)
  (q : nullifying-hom-Ab A B H)  UU (l1  l2  l3  lsuc l)
universal-property-quotient-Ab l A H B q =
  (C : Ab l)  is-equiv (precomp-nullifying-hom-Ab A H B q C)

The quotient group

The quotient map and the underlying set of the quotient group

module _
  {l1 l2 : Level} (A : Ab l1) (H : Subgroup-Ab l2 A)
  where

  set-quotient-Ab : Set (l1  l2)
  set-quotient-Ab =
    quotient-Set (eq-rel-congruence-Subgroup-Ab A H)

  type-quotient-Ab : UU (l1  l2)
  type-quotient-Ab =
    set-quotient (eq-rel-congruence-Subgroup-Ab A H)

  is-set-type-quotient-Ab : is-set type-quotient-Ab
  is-set-type-quotient-Ab =
    is-set-set-quotient (eq-rel-congruence-Subgroup-Ab A H)

  map-quotient-hom-Ab : type-Ab A  type-quotient-Ab
  map-quotient-hom-Ab =
    quotient-map (eq-rel-congruence-Subgroup-Ab A H)

  is-surjective-map-quotient-hom-Ab :
    is-surjective map-quotient-hom-Ab
  is-surjective-map-quotient-hom-Ab =
    is-surjective-quotient-map (eq-rel-congruence-Subgroup-Ab A H)

  is-effective-map-quotient-hom-Ab :
    is-effective
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( map-quotient-hom-Ab)
  is-effective-map-quotient-hom-Ab =
    is-effective-quotient-map (eq-rel-congruence-Subgroup-Ab A H)

  apply-effectiveness-map-quotient-hom-Ab :
    {x y : type-Ab A} 
    map-quotient-hom-Ab x  map-quotient-hom-Ab y 
    sim-congruence-Subgroup-Ab A H x y
  apply-effectiveness-map-quotient-hom-Ab =
    apply-effectiveness-quotient-map
      ( eq-rel-congruence-Subgroup-Ab A H)

  apply-effectiveness-map-quotient-hom-Ab' :
    {x y : type-Ab A} 
    sim-congruence-Subgroup-Ab A H x y 
    map-quotient-hom-Ab x  map-quotient-hom-Ab y
  apply-effectiveness-map-quotient-hom-Ab' =
    apply-effectiveness-quotient-map'
      ( eq-rel-congruence-Subgroup-Ab A H)

  reflecting-map-quotient-hom-Ab :
    reflecting-map-Eq-Rel
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( type-quotient-Ab)
  reflecting-map-quotient-hom-Ab =
    reflecting-map-quotient-map
      ( eq-rel-congruence-Subgroup-Ab A H)

  is-set-quotient-set-quotient-Ab :
    {l : Level} 
    is-set-quotient l
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( set-quotient-Ab)
      ( reflecting-map-quotient-hom-Ab)
  is-set-quotient-set-quotient-Ab =
    is-set-quotient-set-quotient
      ( eq-rel-congruence-Subgroup-Ab A H)

The group structure on the quotient group

  zero-quotient-Ab : type-quotient-Ab
  zero-quotient-Ab = map-quotient-hom-Ab (zero-Ab A)

  binary-hom-add-quotient-Ab :
    binary-hom-Eq-Rel
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( eq-rel-congruence-Subgroup-Ab A H)
  binary-hom-add-quotient-Ab =
    binary-hom-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  add-quotient-Ab :
    (x y : type-quotient-Ab)  type-quotient-Ab
  add-quotient-Ab =
    mul-quotient-Group (group-Ab A) (normal-subgroup-Subgroup-Ab A H)

  add-quotient-Ab' :
    (x y : type-quotient-Ab)  type-quotient-Ab
  add-quotient-Ab' =
    mul-quotient-Group' (group-Ab A) (normal-subgroup-Subgroup-Ab A H)

  compute-add-quotient-Ab :
    (x y : type-Ab A) 
    add-quotient-Ab
      ( map-quotient-hom-Ab x)
      ( map-quotient-hom-Ab y) 
    map-quotient-hom-Ab (add-Ab A x y)
  compute-add-quotient-Ab =
    compute-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  hom-neg-quotient-Ab :
    hom-Eq-Rel
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( eq-rel-congruence-Subgroup-Ab A H)
  hom-neg-quotient-Ab =
    hom-inv-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  neg-quotient-Ab : type-quotient-Ab  type-quotient-Ab
  neg-quotient-Ab =
    inv-quotient-Group (group-Ab A) (normal-subgroup-Subgroup-Ab A H)

  compute-neg-quotient-Ab :
    (x : type-Ab A) 
    neg-quotient-Ab (map-quotient-hom-Ab x) 
    map-quotient-hom-Ab (neg-Ab A x)
  compute-neg-quotient-Ab =
    compute-inv-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  left-unit-law-add-quotient-Ab :
    (x : type-quotient-Ab)  add-quotient-Ab zero-quotient-Ab x  x
  left-unit-law-add-quotient-Ab =
    left-unit-law-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  right-unit-law-add-quotient-Ab :
    (x : type-quotient-Ab)  add-quotient-Ab x zero-quotient-Ab  x
  right-unit-law-add-quotient-Ab =
    right-unit-law-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  associative-add-quotient-Ab :
    (x y z : type-quotient-Ab) 
    ( add-quotient-Ab (add-quotient-Ab x y) z) 
    ( add-quotient-Ab x (add-quotient-Ab y z))
  associative-add-quotient-Ab =
    associative-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  left-inverse-law-add-quotient-Ab :
    (x : type-quotient-Ab) 
    add-quotient-Ab (neg-quotient-Ab x) x  zero-quotient-Ab
  left-inverse-law-add-quotient-Ab =
    left-inverse-law-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  right-inverse-law-add-quotient-Ab :
    (x : type-quotient-Ab) 
    add-quotient-Ab x (neg-quotient-Ab x)  zero-quotient-Ab
  right-inverse-law-add-quotient-Ab =
    right-inverse-law-mul-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  commutative-add-quotient-Ab :
    (x y : type-quotient-Ab) 
    add-quotient-Ab x y  add-quotient-Ab y x
  commutative-add-quotient-Ab =
    double-induction-set-quotient'
      ( eq-rel-congruence-Subgroup-Ab A H)
      ( λ x y 
        Id-Prop
          ( set-quotient-Ab)
          ( add-quotient-Ab x y)
          ( add-quotient-Ab y x))
      ( λ x y 
        ( compute-add-quotient-Ab x y) 
        ( ( ap map-quotient-hom-Ab (commutative-add-Ab A x y)) 
          ( inv (compute-add-quotient-Ab y x))))

  semigroup-quotient-Ab : Semigroup (l1  l2)
  semigroup-quotient-Ab =
    semigroup-quotient-Group
      ( group-Ab A)
      ( normal-subgroup-Subgroup-Ab A H)

  group-quotient-Ab : Group (l1  l2)
  group-quotient-Ab =
    quotient-Group (group-Ab A) (normal-subgroup-Subgroup-Ab A H)

  quotient-Ab : Ab (l1  l2)
  pr1 quotient-Ab = group-quotient-Ab
  pr2 quotient-Ab = commutative-add-quotient-Ab