# Kernels

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Maša Žaucer, Amélia Liao and Gregor Perčič.

Created on 2022-07-15.

module group-theory.kernels 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.abelian-groups
open import group-theory.embeddings-abelian-groups
open import group-theory.embeddings-groups
open import group-theory.groups
open import group-theory.homomorphisms-abelian-groups
open import group-theory.homomorphisms-groups
open import group-theory.normal-subgroups
open import group-theory.subgroups
open import group-theory.subgroups-abelian-groups
open import group-theory.subsets-abelian-groups
open import group-theory.subsets-groups


## Idea

The kernel of a group homomorphism f : A → B is the subgroup of A consisting of those elements which f sends to the unit of B.

## 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 : type-hom-Group G H)
where

subset-kernel-hom-Group : subset-Group k G
subset-kernel-hom-Group x =
Id-Prop (set-Group H) (map-hom-Group G H f x) (unit-Group H)

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 = 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 x y p q =
( preserves-mul-hom-Group G H f x y) ∙
( ( ap (λ (x , y) → mul-Group H x y) (eq-pair p q)) ∙
( left-unit-law-mul-Group H _))

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 x p =
( preserves-inv-hom-Group G H f x) ∙
( ap (inv-Group H) p ∙ inv-unit-Group H)

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 : type-hom-Group group-kernel-hom-Group G
inclusion-kernel-hom-Group =
hom-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 : type-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 =
( preserves-mul-hom-Group G H f (mul-Group G g (pr1 h)) (inv-Group G g)) ∙
( ( ap
( mul-Group' H (map-hom-Group G H f (inv-Group G g)))
( ( preserves-mul-hom-Group G H f g (pr1 h)) ∙
( ( ap (mul-Group H (map-hom-Group G H f g)) (pr2 h)) ∙
( right-unit-law-mul-Group H (map-hom-Group G H f g))))) ∙
( ( ap
( mul-Group H (map-hom-Group G H f g))
( preserves-inv-hom-Group G H f g)) ∙
( 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


### Kernels of group homomorphisms between abelian groups

module _
{l1 l2 : Level} (A : Ab l1) (B : Ab l2) (f : type-hom-Ab A B)
where

subset-kernel-hom-Ab : subset-Ab l2 A
subset-kernel-hom-Ab =
subset-kernel-hom-Group (group-Ab A) (group-Ab B) f

is-in-kernel-hom-Ab : type-Ab A → UU l2
is-in-kernel-hom-Ab =
is-in-kernel-hom-Group (group-Ab A) (group-Ab B) f

contains-zero-subset-kernel-hom-Ab :
is-in-kernel-hom-Ab (zero-Ab A)
contains-zero-subset-kernel-hom-Ab =
contains-unit-subset-kernel-hom-Group (group-Ab A) (group-Ab B) f

is-closed-under-multiplication-subset-kernel-hom-Group
( group-Ab A)
( group-Ab B)
( f)

is-closed-under-negatives-subset-kernel-hom-Ab :
is-closed-under-negatives-subset-Ab A subset-kernel-hom-Ab
is-closed-under-negatives-subset-kernel-hom-Ab =
is-closed-under-inverses-subset-kernel-hom-Group
( group-Ab A)
( group-Ab B)
( f)

kernel-hom-Ab : Subgroup-Ab l2 A
kernel-hom-Ab =
subgroup-kernel-hom-Group (group-Ab A) (group-Ab B) f

ab-kernel-hom-Ab : Ab (l1 ⊔ l2)
ab-kernel-hom-Ab = ab-Subgroup-Ab A kernel-hom-Ab

inclusion-kernel-hom-Ab : type-hom-Ab ab-kernel-hom-Ab A
inclusion-kernel-hom-Ab =
inclusion-kernel-hom-Group (group-Ab A) (group-Ab B) f

is-emb-inclusion-kernel-hom-Ab :
is-emb-hom-Ab ab-kernel-hom-Ab A inclusion-kernel-hom-Ab
is-emb-inclusion-kernel-hom-Ab =
is-emb-inclusion-kernel-hom-Group (group-Ab A) (group-Ab B) f

emb-inclusion-kernel-hom-Ab : emb-Ab ab-kernel-hom-Ab A
emb-inclusion-kernel-hom-Ab =
emb-inclusion-kernel-hom-Group (group-Ab A) (group-Ab B) f