# Homomorphisms of groups equipped with normal subgroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-22.

module group-theory.homomorphisms-groups-equipped-with-normal-subgroups where

Imports
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.normal-subgroups
open import group-theory.pullbacks-subgroups
open import group-theory.subgroups


## Idea

Consider a group G equipped with a normal subgroup and a group H equipped with a normal subgroup M. A homomorphism of groups equipped with normal subgroups from (G,N) to (H,M) consists of a group homomorphism f : G → H which reflects the normal subgroup N into M, i.e., such that the condition x ∈ N ⇒ f x ∈ M holds.

## Definitions

### The property of group homomorphisms of reflecting a normal subgroup

We say that a group homomorphism f : G → H reflects a normal subgroup N of G into a normal subgroup M of H if the property

  x ∈ N ⇒ f x ∈ M


holds for every x : G, i.e., if f maps elements in N to elements in M.

## Definitions

### The predicate of reflecting a normal subgroup

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

reflects-normal-subgroup-hom-Group : hom-Group G H → UU (l1 ⊔ l3 ⊔ l4)
reflects-normal-subgroup-hom-Group f =
leq-Normal-Subgroup G N (pullback-Normal-Subgroup G H f M)

reflecting-hom-Group : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
reflecting-hom-Group = Σ (hom-Group G H) reflects-normal-subgroup-hom-Group


### Reflecting group homomorphisms

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

hom-reflecting-hom-Group : hom-Group G H
hom-reflecting-hom-Group = pr1 f

reflects-normal-subgroup-reflecting-hom-Group :
reflects-normal-subgroup-hom-Group G H N M hom-reflecting-hom-Group
reflects-normal-subgroup-reflecting-hom-Group = pr2 f

map-reflecting-hom-Group : type-Group G → type-Group H
map-reflecting-hom-Group = map-hom-Group G H hom-reflecting-hom-Group


### The identity reflecting group homomorphism

We define two variations of the identity reflecting group homomorphism. We will define the standard identity reflecting group homomorphism, but we will also we define a generalized version which takes as an argument an arbitrary element of

  reflects-normal-subgroup-hom-Group G G N N (id-hom-Group G).


The purpose is that in functoriality proofs, the proof that the identity homomorphism is reflecting is not always the standard one.

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

reflects-normal-subgroup-id-hom-Group :
reflects-normal-subgroup-hom-Group G G N N (id-hom-Group G)
reflects-normal-subgroup-id-hom-Group =
refl-leq-subtype (subset-Normal-Subgroup G N)

id-reflecting-hom-Group' :
(p : reflects-normal-subgroup-hom-Group G G N N (id-hom-Group G)) →
reflecting-hom-Group G G N N
pr1 (id-reflecting-hom-Group' p) = id-hom-Group G
pr2 (id-reflecting-hom-Group' p) = p

id-reflecting-hom-Group : reflecting-hom-Group G G N N
id-reflecting-hom-Group =
id-reflecting-hom-Group' reflects-normal-subgroup-id-hom-Group


### Composition of reflecting group homomorphisms

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

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

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

reflects-normal-subgroup-comp-reflecting-hom-Group :
(g : reflecting-hom-Group H K M N) →
(f : reflecting-hom-Group G H L M) →
reflects-normal-subgroup-hom-Group G K L N
( hom-comp-reflecting-hom-Group g f)
reflects-normal-subgroup-comp-reflecting-hom-Group g f =
transitive-leq-subtype
( subset-Normal-Subgroup G L)
( subset-Normal-Subgroup H M ∘ map-reflecting-hom-Group G H L M f)
( subset-Normal-Subgroup K N ∘ map-comp-reflecting-hom-Group g f)
( ( reflects-normal-subgroup-reflecting-hom-Group H K M N g) ∘
( map-reflecting-hom-Group G H L M f))
( reflects-normal-subgroup-reflecting-hom-Group G H L M f)

comp-reflecting-hom-Group' :
(g : reflecting-hom-Group H K M N) (f : reflecting-hom-Group G H L M) →
(p :
reflects-normal-subgroup-hom-Group G K L N
( hom-comp-reflecting-hom-Group g f)) →
reflecting-hom-Group G K L N
pr1 (comp-reflecting-hom-Group' g f p) = hom-comp-reflecting-hom-Group g f
pr2 (comp-reflecting-hom-Group' g f p) = p

comp-reflecting-hom-Group :
reflecting-hom-Group H K M N →
reflecting-hom-Group G H L M →
reflecting-hom-Group G K L N
comp-reflecting-hom-Group g f =
comp-reflecting-hom-Group' g f
( reflects-normal-subgroup-comp-reflecting-hom-Group g f)


### Homotopies of reflecting homomorphisms

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

htpy-reflecting-hom-Group :
reflecting-hom-Group G H N M → reflecting-hom-Group G H N M → UU (l1 ⊔ l2)
htpy-reflecting-hom-Group f g =
htpy-hom-Group G H
( hom-reflecting-hom-Group G H N M f)
( hom-reflecting-hom-Group G H N M g)

refl-htpy-reflecting-hom-Group :
(f : reflecting-hom-Group G H N M) → htpy-reflecting-hom-Group f f
refl-htpy-reflecting-hom-Group f =
refl-htpy-hom-Group G H (hom-reflecting-hom-Group G H N M f)


## Properties

### Characterization of equality of reflecting homomorphisms

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

htpy-eq-reflecting-hom-Group :
(g : reflecting-hom-Group G H N M) →
f ＝ g → htpy-reflecting-hom-Group G H N M f g
htpy-eq-reflecting-hom-Group g refl =
refl-htpy-reflecting-hom-Group G H N M f