# Kernels of homomorphisms of groups

Content created by Egbert Rijke.

Created 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