# Homomorphisms of semigroups

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-03-17.

module group-theory.homomorphisms-semigroups where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import group-theory.semigroups


## Idea

A homomorphism between two semigroups is a map between their underlying types that preserves the binary operation.

## Definition

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2}
where

preserves-mul : (μA : A → A → A) (μB : B → B → B) → (A → B) → UU (l1 ⊔ l2)
preserves-mul μA μB f = {x y : A} → f (μA x y) ＝ μB (f x) (f y)

preserves-mul' : (μA : A → A → A) (μB : B → B → B) → (A → B) → UU (l1 ⊔ l2)
preserves-mul' μA μB f = (x y : A) → f (μA x y) ＝ μB (f x) (f y)

module _
{l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2)
where

preserves-mul-prop-Semigroup :
(type-Semigroup G → type-Semigroup H) → Prop (l1 ⊔ l2)
preserves-mul-prop-Semigroup f =
implicit-Π-Prop
( type-Semigroup G)
( λ x →
implicit-Π-Prop
( type-Semigroup G)
( λ y →
Id-Prop
( set-Semigroup H)
( f (mul-Semigroup G x y))
( mul-Semigroup H (f x) (f y))))

preserves-mul-prop-Semigroup' :
(type-Semigroup G → type-Semigroup H) → Prop (l1 ⊔ l2)
preserves-mul-prop-Semigroup' f =
implicit-Π-Prop
( type-Semigroup G)
( λ x →
implicit-Π-Prop
( type-Semigroup G)
( λ y →
Id-Prop
( set-Semigroup H)
( f (mul-Semigroup' G x y))
( mul-Semigroup H (f x) (f y))))

preserves-mul-Semigroup :
(type-Semigroup G → type-Semigroup H) → UU (l1 ⊔ l2)
preserves-mul-Semigroup f =
type-Prop (preserves-mul-prop-Semigroup f)

preserves-mul-Semigroup' :
(type-Semigroup G → type-Semigroup H) → UU (l1 ⊔ l2)
preserves-mul-Semigroup' f =
type-Prop (preserves-mul-prop-Semigroup' f)

is-prop-preserves-mul-Semigroup :
(f : type-Semigroup G → type-Semigroup H) →
is-prop (preserves-mul-Semigroup f)
is-prop-preserves-mul-Semigroup f =
is-prop-type-Prop (preserves-mul-prop-Semigroup f)

is-prop-preserves-mul-Semigroup' :
(f : type-Semigroup G → type-Semigroup H) →
is-prop (preserves-mul-Semigroup' f)
is-prop-preserves-mul-Semigroup' f =
is-prop-type-Prop (preserves-mul-prop-Semigroup' f)

hom-Semigroup : UU (l1 ⊔ l2)
hom-Semigroup =
Σ ( type-Semigroup G → type-Semigroup H)
( preserves-mul-Semigroup)

map-hom-Semigroup :
hom-Semigroup → type-Semigroup G → type-Semigroup H
map-hom-Semigroup f = pr1 f

preserves-mul-hom-Semigroup :
(f : hom-Semigroup) → preserves-mul-Semigroup (map-hom-Semigroup f)
preserves-mul-hom-Semigroup f = pr2 f


### Characterizing the identity type of semigroup homomorphisms

  htpy-hom-Semigroup : (f g : hom-Semigroup) → UU (l1 ⊔ l2)
htpy-hom-Semigroup f g = map-hom-Semigroup f ~ map-hom-Semigroup g

refl-htpy-hom-Semigroup : (f : hom-Semigroup) → htpy-hom-Semigroup f f
refl-htpy-hom-Semigroup f = refl-htpy

htpy-eq-hom-Semigroup :
(f g : hom-Semigroup) → Id f g → htpy-hom-Semigroup f g
htpy-eq-hom-Semigroup f .f refl = refl-htpy-hom-Semigroup f

abstract
is-torsorial-htpy-hom-Semigroup :
(f : hom-Semigroup) → is-torsorial (htpy-hom-Semigroup f)
is-torsorial-htpy-hom-Semigroup f =
is-torsorial-Eq-subtype
( is-torsorial-htpy (map-hom-Semigroup f))
( is-prop-preserves-mul-Semigroup)
( map-hom-Semigroup f)
( refl-htpy)
( preserves-mul-hom-Semigroup f)

abstract
is-equiv-htpy-eq-hom-Semigroup :
(f g : hom-Semigroup) → is-equiv (htpy-eq-hom-Semigroup f g)
is-equiv-htpy-eq-hom-Semigroup f =
fundamental-theorem-id
( is-torsorial-htpy-hom-Semigroup f)
( htpy-eq-hom-Semigroup f)

eq-htpy-hom-Semigroup :
{f g : hom-Semigroup} → htpy-hom-Semigroup f g → Id f g
eq-htpy-hom-Semigroup {f} {g} =
map-inv-is-equiv (is-equiv-htpy-eq-hom-Semigroup f g)

is-set-hom-Semigroup : is-set hom-Semigroup
is-set-hom-Semigroup f g =
is-prop-is-equiv
( is-equiv-htpy-eq-hom-Semigroup f g)
( is-prop-Π
( λ x →
is-set-type-Semigroup H
( map-hom-Semigroup f x)
( map-hom-Semigroup g x)))

hom-set-Semigroup : Set (l1 ⊔ l2)
pr1 hom-set-Semigroup = hom-Semigroup
pr2 hom-set-Semigroup = is-set-hom-Semigroup

preserves-mul-id-Semigroup :
{l : Level} (G : Semigroup l) → preserves-mul-Semigroup G G id
preserves-mul-id-Semigroup G = refl


### The identity homomorphism of semigroups

id-hom-Semigroup :
{l : Level} (G : Semigroup l) → hom-Semigroup G G
pr1 (id-hom-Semigroup G) = id
pr2 (id-hom-Semigroup G) = preserves-mul-id-Semigroup G


### Composition of morphisms of semigroups

module _
{l1 l2 l3 : Level}
(G : Semigroup l1) (H : Semigroup l2) (K : Semigroup l3)
(g : hom-Semigroup H K) (f : hom-Semigroup G H)
where

map-comp-hom-Semigroup : type-Semigroup G → type-Semigroup K
map-comp-hom-Semigroup =
(map-hom-Semigroup H K g) ∘ (map-hom-Semigroup G H f)

preserves-mul-comp-hom-Semigroup :
preserves-mul-Semigroup G K map-comp-hom-Semigroup
preserves-mul-comp-hom-Semigroup =
( ap
( map-hom-Semigroup H K g)
( preserves-mul-hom-Semigroup G H f)) ∙
( preserves-mul-hom-Semigroup H K g)

comp-hom-Semigroup : hom-Semigroup G K
pr1 comp-hom-Semigroup = map-comp-hom-Semigroup
pr2 comp-hom-Semigroup = preserves-mul-comp-hom-Semigroup


### Associativity of composition of homomorphisms of semigroups

module _
{l1 l2 l3 l4 : Level}
(G : Semigroup l1) (H : Semigroup l2) (K : Semigroup l3) (L : Semigroup l4)
(h : hom-Semigroup K L) (g : hom-Semigroup H K) (f : hom-Semigroup G H)
where

associative-comp-hom-Semigroup :
comp-hom-Semigroup G H L (comp-hom-Semigroup H K L h g) f ＝
comp-hom-Semigroup G K L h (comp-hom-Semigroup G H K g f)
associative-comp-hom-Semigroup = eq-htpy-hom-Semigroup G L refl-htpy


### The left and right unit laws for composition of homomorphisms of semigroups

left-unit-law-comp-hom-Semigroup :
{ l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2)
( f : hom-Semigroup G H) →
Id ( comp-hom-Semigroup G H H (id-hom-Semigroup H) f) f
left-unit-law-comp-hom-Semigroup G
(pair (pair H is-set-H) (pair μ-H associative-H)) (pair f μ-f) =
eq-htpy-hom-Semigroup G
( pair (pair H is-set-H) (pair μ-H associative-H))
( refl-htpy)

right-unit-law-comp-hom-Semigroup :
{ l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2)
( f : hom-Semigroup G H) →
Id ( comp-hom-Semigroup G G H f (id-hom-Semigroup G)) f
right-unit-law-comp-hom-Semigroup
(pair (pair G is-set-G) (pair μ-G associative-G)) H (pair f μ-f) =
eq-htpy-hom-Semigroup
( pair (pair G is-set-G) (pair μ-G associative-G)) H refl-htpy