# Images of semigroup homomorphisms

Content created by Egbert Rijke.

Created on 2023-11-24.

module group-theory.images-of-semigroup-homomorphisms where

Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.images
open import foundation.images-subtypes
open import foundation.logical-equivalences
open import foundation.propositional-truncations
open import foundation.universal-property-image
open import foundation.universe-levels

open import group-theory.homomorphisms-semigroups
open import group-theory.pullbacks-subsemigroups
open import group-theory.semigroups
open import group-theory.subsemigroups
open import group-theory.subsets-semigroups

open import order-theory.galois-connections-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders


## Idea

The image of a semigroup homomorphism f : G → H consists of the image of the underlying map of f. This subset is closed under multiplication, so it is a subsemigroup of the semigroup H. Alternatively, it can be described as the least subsemigroup of H that contains all the values of f.

More generally, the image of a subsemigroup S under a semigroup homomorphism f : G → H is the subsemigroup consisting of all the elements in the image of the underlying subset of S under the underlying map of f. Since the image of a subsemigroup satisfies the following adjoint relation

  (im f S ⊆ T) ↔ (S ⊆ T ∘ f)


it follows that we obtain a Galois connection.

## Definitions

### The universal property of the image of a semigroup homomorphism

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

is-image-hom-Semigroup : UUω
is-image-hom-Semigroup =
{l : Level} (L : Subsemigroup l H) →
leq-Subsemigroup H K L ↔
( (g : type-Semigroup G) →
is-in-Subsemigroup H L (map-hom-Semigroup G H f g))


### The universal property of the image subsemigroup of a subsemigroup

module _
{l1 l2 l3 l4 : Level} (G : Semigroup l1) (H : Semigroup l2)
(f : hom-Semigroup G H) (S : Subsemigroup l3 G) (T : Subsemigroup l4 H)
where

is-image-subsemigroup-hom-Semigroup : UUω
is-image-subsemigroup-hom-Semigroup =
{l : Level} (U : Subsemigroup l H) →
leq-Subsemigroup H T U ↔
leq-Subsemigroup G S (pullback-Subsemigroup G H f U)


### The image subsemigroup under a semigroup homomorphism

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

subset-image-hom-Semigroup : subset-Semigroup (l1 ⊔ l2) H
subset-image-hom-Semigroup = subtype-im (map-hom-Semigroup G H f)

is-image-subtype-subset-image-hom-Semigroup :
is-image-subtype (map-hom-Semigroup G H f) subset-image-hom-Semigroup
is-image-subtype-subset-image-hom-Semigroup =
is-image-subtype-subtype-im (map-hom-Semigroup G H f)

abstract
is-closed-under-multiplication-image-hom-Semigroup :
is-closed-under-multiplication-subset-Semigroup H
subset-image-hom-Semigroup
is-closed-under-multiplication-image-hom-Semigroup {x} {y} K L =
apply-twice-universal-property-trunc-Prop K L
( subset-image-hom-Semigroup (mul-Semigroup H x y))
( λ where
( g , refl) (h , refl) →
unit-trunc-Prop
( mul-Semigroup G g h , preserves-mul-hom-Semigroup G H f))

image-hom-Semigroup : Subsemigroup (l1 ⊔ l2) H
pr1 image-hom-Semigroup = subset-image-hom-Semigroup
pr2 image-hom-Semigroup = is-closed-under-multiplication-image-hom-Semigroup

is-image-image-hom-Semigroup :
is-image-hom-Semigroup G H f image-hom-Semigroup
is-image-image-hom-Semigroup K =
is-image-subtype-subset-image-hom-Semigroup (subset-Subsemigroup H K)

contains-values-image-hom-Semigroup :
(g : type-Semigroup G) →
is-in-Subsemigroup H image-hom-Semigroup (map-hom-Semigroup G H f g)
contains-values-image-hom-Semigroup =
forward-implication
( is-image-image-hom-Semigroup image-hom-Semigroup)
( refl-leq-Subsemigroup H image-hom-Semigroup)

leq-image-hom-Semigroup :
{l : Level} (K : Subsemigroup l H) →
( ( g : type-Semigroup G) →
is-in-Subsemigroup H K (map-hom-Semigroup G H f g)) →
leq-Subsemigroup H image-hom-Semigroup K
leq-image-hom-Semigroup K =
backward-implication (is-image-image-hom-Semigroup K)


### The image of a subsemigroup under a semigroup homomorphism

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

subset-im-hom-Subsemigroup : subset-Semigroup (l1 ⊔ l2 ⊔ l3) H
subset-im-hom-Subsemigroup =
im-subtype (map-hom-Semigroup G H f) (subset-Subsemigroup G K)

abstract
is-closed-under-multiplication-im-hom-Subsemigroup :
is-closed-under-multiplication-subset-Semigroup H
subset-im-hom-Subsemigroup
is-closed-under-multiplication-im-hom-Subsemigroup {x} {y} u v =
apply-twice-universal-property-trunc-Prop u v
( subset-im-hom-Subsemigroup (mul-Semigroup H x y))
( λ where
((x' , k) , refl) ((y' , l) , refl) →
unit-trunc-Prop
( ( mul-Subsemigroup G K (x' , k) (y' , l)) ,
( preserves-mul-hom-Semigroup G H f)))

im-hom-Subsemigroup : Subsemigroup (l1 ⊔ l2 ⊔ l3) H
pr1 im-hom-Subsemigroup =
subset-im-hom-Subsemigroup
pr2 im-hom-Subsemigroup =
is-closed-under-multiplication-im-hom-Subsemigroup

forward-implication-is-image-subsemigroup-im-hom-Subsemigroup :
{l : Level} (U : Subsemigroup l H) →
leq-Subsemigroup H im-hom-Subsemigroup U →
leq-Subsemigroup G K (pullback-Subsemigroup G H f U)
forward-implication-is-image-subsemigroup-im-hom-Subsemigroup U =
( map-hom-Semigroup G H f)
( subset-Subsemigroup G K)
( subset-Subsemigroup H U)

backward-implication-is-image-subsemigroup-im-hom-Subsemigroup :
{l : Level} (U : Subsemigroup l H) →
leq-Subsemigroup G K (pullback-Subsemigroup G H f U) →
leq-Subsemigroup H im-hom-Subsemigroup U
backward-implication-is-image-subsemigroup-im-hom-Subsemigroup U =
( map-hom-Semigroup G H f)
( subset-Subsemigroup G K)
( subset-Subsemigroup H U)

is-image-subsemigroup-im-hom-Subsemigroup :
is-image-subsemigroup-hom-Semigroup G H f K im-hom-Subsemigroup
is-image-subsemigroup-im-hom-Subsemigroup U =
( map-hom-Semigroup G H f)
( subset-Subsemigroup G K)
( subset-Subsemigroup H U)


### The image-pullback Galois connection on subsemigroups

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

preserves-order-im-hom-Subsemigroup :
{l3 l4 : Level} (K : Subsemigroup l3 G) (L : Subsemigroup l4 G) →
leq-Subsemigroup G K L →
leq-Subsemigroup H
( im-hom-Subsemigroup G H f K)
( im-hom-Subsemigroup G H f L)
preserves-order-im-hom-Subsemigroup K L =
preserves-order-im-subtype
( map-hom-Semigroup G H f)
( subset-Subsemigroup G K)
( subset-Subsemigroup G L)

im-hom-subsemigroup-hom-Large-Poset :
hom-Large-Poset
( λ l → l1 ⊔ l2 ⊔ l)
( Subsemigroup-Large-Poset G)
( Subsemigroup-Large-Poset H)
map-hom-Large-Preorder im-hom-subsemigroup-hom-Large-Poset =
im-hom-Subsemigroup G H f
preserves-order-hom-Large-Preorder im-hom-subsemigroup-hom-Large-Poset =
preserves-order-im-hom-Subsemigroup

image-pullback-galois-connection-Subsemigroup :
galois-connection-Large-Poset
( λ l → l1 ⊔ l2 ⊔ l)
( λ l → l)
( Subsemigroup-Large-Poset G)
( Subsemigroup-Large-Poset H)