# Isomorphisms of semigroups

```agda
module group-theory.isomorphisms-semigroups where
```

<details><summary>Imports</summary>

```agda
open import category-theory.isomorphisms-in-large-precategories

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import group-theory.equivalences-semigroups
open import group-theory.homomorphisms-semigroups
open import group-theory.precategory-of-semigroups
open import group-theory.semigroups
```

</details>

## Idea

Isomorphisms of semigroups are homomorphisms that have a two-sided inverse.

## Definition

### The predicate of being an isomorphism of semigroups

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

  is-iso-Semigroup : UU (l1 ⊔ l2)
  is-iso-Semigroup =
    is-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} f

  hom-inv-is-iso-Semigroup :
    is-iso-Semigroup → hom-Semigroup H G
  hom-inv-is-iso-Semigroup =
    hom-inv-is-iso-Large-Precategory
      ( Semigroup-Large-Precategory)
      { X = G}
      { Y = H}
      ( f)

  map-inv-is-iso-Semigroup :
    is-iso-Semigroup → type-Semigroup H → type-Semigroup G
  map-inv-is-iso-Semigroup U =
    map-hom-Semigroup H G (hom-inv-is-iso-Semigroup U)

  is-section-hom-inv-is-iso-Semigroup :
    (U : is-iso-Semigroup) →
    comp-hom-Semigroup H G H f (hom-inv-is-iso-Semigroup U) ＝
    id-hom-Semigroup H
  is-section-hom-inv-is-iso-Semigroup =
    is-section-hom-inv-is-iso-Large-Precategory
      ( Semigroup-Large-Precategory)
      { X = G}
      { Y = H}
      ( f)

  is-section-map-inv-is-iso-Semigroup :
    (U : is-iso-Semigroup) →
    ( map-hom-Semigroup G H f ∘ map-inv-is-iso-Semigroup U) ~ id
  is-section-map-inv-is-iso-Semigroup U =
    htpy-eq-hom-Semigroup H H
      ( comp-hom-Semigroup H G H f (hom-inv-is-iso-Semigroup U))
      ( id-hom-Semigroup H)
      ( is-section-hom-inv-is-iso-Semigroup U)

  is-retraction-hom-inv-is-iso-Semigroup :
    (U : is-iso-Semigroup) →
    comp-hom-Semigroup G H G (hom-inv-is-iso-Semigroup U) f ＝
    id-hom-Semigroup G
  is-retraction-hom-inv-is-iso-Semigroup =
    is-retraction-hom-inv-is-iso-Large-Precategory
      ( Semigroup-Large-Precategory)
      { X = G}
      { Y = H}
      ( f)

  is-retraction-map-inv-is-iso-Semigroup :
    (U : is-iso-Semigroup) →
    ( map-inv-is-iso-Semigroup U ∘ map-hom-Semigroup G H f) ~ id
  is-retraction-map-inv-is-iso-Semigroup U =
    htpy-eq-hom-Semigroup G G
      ( comp-hom-Semigroup G H G (hom-inv-is-iso-Semigroup U) f)
      ( id-hom-Semigroup G)
      ( is-retraction-hom-inv-is-iso-Semigroup U)
```

### Isomorphisms of semigroups

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

  iso-Semigroup : UU (l1 ⊔ l2)
  iso-Semigroup = iso-Large-Precategory Semigroup-Large-Precategory G H

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

  hom-iso-Semigroup : hom-Semigroup G H
  hom-iso-Semigroup =
    hom-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} f

  map-iso-Semigroup : type-Semigroup G → type-Semigroup H
  map-iso-Semigroup = map-hom-Semigroup G H hom-iso-Semigroup

  preserves-mul-iso-Semigroup :
    {x y : type-Semigroup G} →
    map-iso-Semigroup (mul-Semigroup G x y) ＝
    mul-Semigroup H (map-iso-Semigroup x) (map-iso-Semigroup y)
  preserves-mul-iso-Semigroup =
    preserves-mul-hom-Semigroup G H hom-iso-Semigroup

  is-iso-iso-Semigroup : is-iso-Semigroup G H hom-iso-Semigroup
  is-iso-iso-Semigroup =
    is-iso-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} f

  inv-iso-Semigroup : iso-Semigroup H G
  inv-iso-Semigroup =
    inv-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} f

  hom-inv-iso-Semigroup : hom-Semigroup H G
  hom-inv-iso-Semigroup =
    hom-inv-iso-Large-Precategory Semigroup-Large-Precategory {X = G} {Y = H} f

  map-inv-iso-Semigroup : type-Semigroup H → type-Semigroup G
  map-inv-iso-Semigroup =
    map-hom-Semigroup H G hom-inv-iso-Semigroup

  preserves-mul-inv-iso-Semigroup :
    {x y : type-Semigroup H} →
    map-inv-iso-Semigroup (mul-Semigroup H x y) ＝
    mul-Semigroup G (map-inv-iso-Semigroup x) (map-inv-iso-Semigroup y)
  preserves-mul-inv-iso-Semigroup =
    preserves-mul-hom-Semigroup H G hom-inv-iso-Semigroup

  is-section-hom-inv-iso-Semigroup :
    comp-hom-Semigroup H G H hom-iso-Semigroup hom-inv-iso-Semigroup ＝
    id-hom-Semigroup H
  is-section-hom-inv-iso-Semigroup =
    is-section-hom-inv-iso-Large-Precategory
      ( Semigroup-Large-Precategory)
      { X = G}
      { Y = H}
      ( f)

  is-section-map-inv-iso-Semigroup :
    map-iso-Semigroup ∘ map-inv-iso-Semigroup ~ id
  is-section-map-inv-iso-Semigroup =
    htpy-eq-hom-Semigroup H H
      ( comp-hom-Semigroup H G H
        ( hom-iso-Semigroup)
        ( hom-inv-iso-Semigroup))
      ( id-hom-Semigroup H)
      ( is-section-hom-inv-iso-Semigroup)

  is-retraction-hom-inv-iso-Semigroup :
    comp-hom-Semigroup G H G hom-inv-iso-Semigroup hom-iso-Semigroup ＝
    id-hom-Semigroup G
  is-retraction-hom-inv-iso-Semigroup =
    is-retraction-hom-inv-iso-Large-Precategory
      ( Semigroup-Large-Precategory)
      { X = G}
      { Y = H}
      ( f)

  is-retraction-map-inv-iso-Semigroup :
    map-inv-iso-Semigroup ∘ map-iso-Semigroup ~ id
  is-retraction-map-inv-iso-Semigroup =
    htpy-eq-hom-Semigroup G G
      ( comp-hom-Semigroup G H G
        ( hom-inv-iso-Semigroup)
        ( hom-iso-Semigroup))
      ( id-hom-Semigroup G)
      ( is-retraction-hom-inv-iso-Semigroup)
```

## Properties

### Being an isomorphism is a property

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

  abstract
    is-prop-is-iso-Semigroup :
      (f : hom-Semigroup G H) → is-prop (is-iso-Semigroup G H f)
    is-prop-is-iso-Semigroup =
      is-prop-is-iso-Large-Precategory
        ( Semigroup-Large-Precategory)
        { X = G}
        { Y = H}

  is-iso-prop-Semigroup :
    hom-Semigroup G H → Prop (l1 ⊔ l2)
  is-iso-prop-Semigroup =
    is-iso-prop-Large-Precategory
      ( Semigroup-Large-Precategory)
      { X = G}
      { Y = H}
```

### The inverse of an equivalence of semigroups preserves the binary operation

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

  abstract
    preserves-mul-map-inv-is-equiv-Semigroup :
      ( f : hom-Semigroup G H)
      ( U : is-equiv (map-hom-Semigroup G H f)) →
      preserves-mul-Semigroup H G (map-inv-is-equiv U)
    preserves-mul-map-inv-is-equiv-Semigroup (f , μ-f) U {x} {y} =
      map-inv-is-equiv
        ( is-emb-is-equiv U
          ( map-inv-is-equiv U (mul-Semigroup H x y))
          ( mul-Semigroup G
            ( map-inv-is-equiv U x)
            ( map-inv-is-equiv U y)))
        ( ( is-section-map-inv-is-equiv U (mul-Semigroup H x y)) ∙
          ( ap
            ( λ t → mul-Semigroup H t y)
            ( inv (is-section-map-inv-is-equiv U x))) ∙
          ( ap
            ( mul-Semigroup H (f (map-inv-is-equiv U x)))
            ( inv (is-section-map-inv-is-equiv U y))) ∙
          ( inv μ-f))
```

### A homomorphism of semigroups is an equivalence of semigroups if and only if it is an isomorphism

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

  abstract
    is-iso-is-equiv-hom-Semigroup :
      (f : hom-Semigroup G H) →
      is-equiv-hom-Semigroup G H f → is-iso-Semigroup G H f
    pr1 (pr1 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) =
      map-inv-is-equiv U
    pr2 (pr1 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) =
      preserves-mul-map-inv-is-equiv-Semigroup G H (f , μ-f) U
    pr1 (pr2 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) =
      eq-htpy-hom-Semigroup H H (is-section-map-inv-is-equiv U)
    pr2 (pr2 (is-iso-is-equiv-hom-Semigroup (f , μ-f) U)) =
      eq-htpy-hom-Semigroup G G (is-retraction-map-inv-is-equiv U)

  abstract
    is-equiv-is-iso-Semigroup :
      (f : hom-Semigroup G H) →
      is-iso-Semigroup G H f → is-equiv-hom-Semigroup G H f
    is-equiv-is-iso-Semigroup (f , μ-f) ((g , μ-g) , S , R) =
      is-equiv-is-invertible g
        ( htpy-eq (ap pr1 S))
        ( htpy-eq (ap pr1 R))

  equiv-iso-equiv-Semigroup : equiv-Semigroup G H ≃ iso-Semigroup G H
  equiv-iso-equiv-Semigroup =
    ( equiv-type-subtype
      ( λ f → is-property-is-equiv (map-hom-Semigroup G H f))
      ( is-prop-is-iso-Semigroup G H)
      ( is-iso-is-equiv-hom-Semigroup)
      ( is-equiv-is-iso-Semigroup)) ∘e
    ( equiv-right-swap-Σ)

  iso-equiv-Semigroup : equiv-Semigroup G H → iso-Semigroup G H
  iso-equiv-Semigroup = map-equiv equiv-iso-equiv-Semigroup
```

### Two semigroups are equal if and only if they are isomorphic

```agda
module _
  {l : Level} (G : Semigroup l)
  where

  is-torsorial-iso-Semigroup :
    is-torsorial (iso-Semigroup G)
  is-torsorial-iso-Semigroup =
    is-contr-equiv'
      ( Σ (Semigroup l) (equiv-Semigroup G))
      ( equiv-tot (equiv-iso-equiv-Semigroup G))
      ( is-torsorial-equiv-Semigroup G)

  id-iso-Semigroup : iso-Semigroup G G
  id-iso-Semigroup =
    id-iso-Large-Precategory Semigroup-Large-Precategory {X = G}

  iso-eq-Semigroup : (H : Semigroup l) → Id G H → iso-Semigroup G H
  iso-eq-Semigroup = iso-eq-Large-Precategory Semigroup-Large-Precategory G
```