Kernels of homomorphisms of groups

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2023-11-24.

module group-theory.kernels-homomorphisms-groups where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-cartesian-product-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.embeddings-groups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.normal-subgroups
open import group-theory.subgroups
open import group-theory.subsets-groups

Idea

The kernel of a group homomorphism f : G → H is the normal subgroup of G consisting of those elements x : G such that f x ＝ unit-Group H.

Definition

We define the kernel as the subgroup generated by the predicate which associates to x the proposition f(x) = unit.

module _
  {l k : Level} (G : Group l) (H : Group k) (f : hom-Group G H)
  where

  subset-kernel-hom-Group : subset-Group k G
  subset-kernel-hom-Group x =
    is-unit-prop-Group' H (map-hom-Group G H f x)

  is-in-kernel-hom-Group : type-Group G → UU k
  is-in-kernel-hom-Group x = type-Prop (subset-kernel-hom-Group x)

  contains-unit-subset-kernel-hom-Group :
    is-in-kernel-hom-Group (unit-Group G)
  contains-unit-subset-kernel-hom-Group = inv (preserves-unit-hom-Group G H f)

  is-closed-under-multiplication-subset-kernel-hom-Group :
    is-closed-under-multiplication-subset-Group G subset-kernel-hom-Group
  is-closed-under-multiplication-subset-kernel-hom-Group p q =
    ( inv (left-unit-law-mul-Group H _)) ∙
    ( ap-mul-Group H p q) ∙
    ( inv (preserves-mul-hom-Group G H f))

  is-closed-under-inverses-subset-kernel-hom-Group :
    is-closed-under-inverses-subset-Group G subset-kernel-hom-Group
  is-closed-under-inverses-subset-kernel-hom-Group p =
    ( inv (inv-unit-Group H)) ∙
    ( ap (inv-Group H) p) ∙
    ( inv (preserves-inv-hom-Group G H f))

  subgroup-kernel-hom-Group : Subgroup k G
  pr1 subgroup-kernel-hom-Group = subset-kernel-hom-Group
  pr1 (pr2 subgroup-kernel-hom-Group) = contains-unit-subset-kernel-hom-Group
  pr1 (pr2 (pr2 subgroup-kernel-hom-Group)) =
    is-closed-under-multiplication-subset-kernel-hom-Group
  pr2 (pr2 (pr2 subgroup-kernel-hom-Group)) =
    is-closed-under-inverses-subset-kernel-hom-Group

  group-kernel-hom-Group : Group (l ⊔ k)
  group-kernel-hom-Group = group-Subgroup G subgroup-kernel-hom-Group

  inclusion-kernel-hom-Group : hom-Group group-kernel-hom-Group G
  inclusion-kernel-hom-Group =
    hom-inclusion-Subgroup G subgroup-kernel-hom-Group

  type-kernel-hom-Group : UU (l ⊔ k)
  type-kernel-hom-Group = type-Subgroup G subgroup-kernel-hom-Group

  map-inclusion-kernel-hom-Group : type-kernel-hom-Group → type-Group G
  map-inclusion-kernel-hom-Group =
    map-hom-Group group-kernel-hom-Group G inclusion-kernel-hom-Group

  is-in-subgroup-inclusion-kernel-hom-Group :
    (x : type-kernel-hom-Group) →
    is-in-kernel-hom-Group (map-inclusion-kernel-hom-Group x)
  is-in-subgroup-inclusion-kernel-hom-Group =
    is-in-subgroup-inclusion-Subgroup G subgroup-kernel-hom-Group

  is-emb-inclusion-kernel-hom-Group :
    is-emb-hom-Group group-kernel-hom-Group G inclusion-kernel-hom-Group
  is-emb-inclusion-kernel-hom-Group =
    is-emb-inclusion-Subgroup G subgroup-kernel-hom-Group

  emb-inclusion-kernel-hom-Group : emb-Group group-kernel-hom-Group G
  pr1 emb-inclusion-kernel-hom-Group =
    inclusion-kernel-hom-Group
  pr2 emb-inclusion-kernel-hom-Group =
    is-emb-inclusion-kernel-hom-Group

Properties

module _
  {l1 l2 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  where

  is-normal-kernel-hom-Group :
    is-normal-Subgroup G (subgroup-kernel-hom-Group G H f)
  is-normal-kernel-hom-Group g h =
    inv
      ( ( preserves-mul-hom-Group G H f) ∙
        ( ap
          ( mul-Group' H (map-hom-Group G H f (inv-Group G g)))
          ( ( preserves-mul-hom-Group G H f) ∙
            ( inv
              ( ap
                ( mul-Group H (map-hom-Group G H f g))
                ( is-in-subgroup-inclusion-kernel-hom-Group G H f h))) ∙
            ( right-unit-law-mul-Group H (map-hom-Group G H f g)))) ∙
        ( ap (mul-Group H _) (preserves-inv-hom-Group G H f)) ∙
        ( right-inverse-law-mul-Group H (map-hom-Group G H f g)))

  kernel-hom-Group : Normal-Subgroup l2 G
  pr1 kernel-hom-Group = subgroup-kernel-hom-Group G H f
  pr2 kernel-hom-Group = is-normal-kernel-hom-Group

Recent changes