# Nullifying group homomorphisms

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.

module group-theory.nullifying-group-homomorphisms where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.propositions
open import foundation.reflecting-maps-equivalence-relations
open import foundation.subtypes
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

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


## Idea

Consider a group homomorphism f : G → H and a normal subgroup N of the group G. We say that f nullifies N if it satisfies the condition

  N ⊆ ker f,


i.e., if f x ＝ 1 for all x ∈ N. Nullifying group homomorphisms are used to define quotient groups.

## Definitions

### The predicate of nullifying a normal subgroup

module _
{l1 l2 l3 : Level} (G : Group l1) (K : Group l2)
where

nullifies-normal-subgroup-prop-hom-Group :
hom-Group G K → Normal-Subgroup l3 G → Prop (l1 ⊔ l2 ⊔ l3)
nullifies-normal-subgroup-prop-hom-Group f H =
leq-prop-Normal-Subgroup G H (kernel-hom-Group G K f)

nullifies-normal-subgroup-hom-Group :
hom-Group G K → Normal-Subgroup l3 G → UU (l1 ⊔ l2 ⊔ l3)
nullifies-normal-subgroup-hom-Group f H =
type-Prop (nullifies-normal-subgroup-prop-hom-Group f H)


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

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

nullifying-hom-Group : UU (l1 ⊔ l2 ⊔ l3)
nullifying-hom-Group =
type-subtype (λ f → nullifies-normal-subgroup-prop-hom-Group G K f H)

hom-nullifying-hom-Group :
nullifying-hom-Group → hom-Group G K
hom-nullifying-hom-Group = pr1

nullifies-normal-subgroup-nullifying-hom-Group :
(f : nullifying-hom-Group) →
nullifies-normal-subgroup-hom-Group G K
( hom-nullifying-hom-Group f) H
nullifies-normal-subgroup-nullifying-hom-Group = pr2


## Properties

### A group homomorphism nullifies a normal subgroup if and only if it reflects the equivalence relation induced by the normal subgroup

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

reflects-equivalence-relation-nullifies-normal-subgroup-hom-Group :
(f : hom-Group G K) →
nullifies-normal-subgroup-hom-Group G K f H →
reflects-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G H)
( map-hom-Group G K f)
reflects-equivalence-relation-nullifies-normal-subgroup-hom-Group f p α =
( inv (right-unit-law-mul-Group K _)) ∙
( inv-transpose-eq-mul-Group' K
( ( p (left-div-Group G _ _) α) ∙
( preserves-left-div-hom-Group G K f)))

nullifies-normal-subgroup-reflects-equivalence-relation-hom-Group :
(f : hom-Group G K) →
reflects-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G H)
( map-hom-Group G K f) →
nullifies-normal-subgroup-hom-Group G K f H
nullifies-normal-subgroup-reflects-equivalence-relation-hom-Group f p x q =
( inv (preserves-unit-hom-Group G K f)) ∙
( p ( is-closed-under-multiplication-Normal-Subgroup G H
( is-closed-under-inverses-Normal-Subgroup G H
( contains-unit-Normal-Subgroup G H))
( q)))

compute-nullifying-hom-Group :
Σ ( reflecting-map-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G H)
( type-Group K))
( λ f → preserves-mul-Group G K (pr1 f)) ≃
nullifying-hom-Group G K H
compute-nullifying-hom-Group =
( equiv-type-subtype
( λ f →
is-prop-reflects-equivalence-relation
( equivalence-relation-congruence-Normal-Subgroup G H)
( set-Group K)
( pr1 f))
( λ f → is-prop-leq-Normal-Subgroup G H (kernel-hom-Group G K f))
( nullifies-normal-subgroup-reflects-equivalence-relation-hom-Group)
( reflects-equivalence-relation-nullifies-normal-subgroup-hom-Group)) ∘e
( equiv-right-swap-Σ)


### Composition of nullifying homomorphisms and reflecting homomorphisms

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

hom-comp-nullifying-hom-reflecting-hom-Group :
nullifying-hom-Group H K M →
reflecting-hom-Group G H N M →
hom-Group G K
hom-comp-nullifying-hom-reflecting-hom-Group g f =
comp-hom-Group G H K
( hom-nullifying-hom-Group H K M g)
( hom-reflecting-hom-Group G H N M f)

nullifies-normal-subgroup-comp-nullifying-hom-reflecting-hom-Group :
( g : nullifying-hom-Group H K M)
( f : reflecting-hom-Group G H N M) →
nullifies-normal-subgroup-hom-Group G K
( hom-comp-nullifying-hom-reflecting-hom-Group g f)
( N)
nullifies-normal-subgroup-comp-nullifying-hom-reflecting-hom-Group g f x n =
nullifies-normal-subgroup-nullifying-hom-Group H K M g
( map-reflecting-hom-Group G H N M f x)
( reflects-normal-subgroup-reflecting-hom-Group G H N M f x n)

comp-nullifying-hom-reflecting-hom-Group :
nullifying-hom-Group H K M →
reflecting-hom-Group G H N M →
nullifying-hom-Group G K N
pr1 (comp-nullifying-hom-reflecting-hom-Group g f) =
hom-comp-nullifying-hom-reflecting-hom-Group g f
pr2 (comp-nullifying-hom-reflecting-hom-Group g f) =
nullifies-normal-subgroup-comp-nullifying-hom-reflecting-hom-Group g f