# Equivalences between semigroups

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

Created on 2022-03-17.

module group-theory.equivalences-semigroups where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.structure-identity-principle
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.univalence
open import foundation.universe-levels

open import group-theory.homomorphisms-semigroups
open import group-theory.semigroups


## Idea

An equivalence between semigroups is an equivalence between their underlying types that preserves the binary operation.

## Definition

### Equivalences preserving binary operations

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

preserves-mul-equiv :
(μA : A → A → A) (μB : B → B → B) → (A ≃ B) → UU (l1 ⊔ l2)
preserves-mul-equiv μA μB e = preserves-mul μA μB (map-equiv e)


### Equivalences of semigroups

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

preserves-mul-equiv-Semigroup :
(type-Semigroup G ≃ type-Semigroup H) → UU (l1 ⊔ l2)
preserves-mul-equiv-Semigroup e =
preserves-mul-equiv (mul-Semigroup G) (mul-Semigroup H) e

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

is-equiv-hom-Semigroup : hom-Semigroup G H → UU (l1 ⊔ l2)
is-equiv-hom-Semigroup f = is-equiv (map-hom-Semigroup G H f)


## Properties

### The total space of all equivalences of semigroups with domain G is contractible

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

center-total-preserves-mul-id-Semigroup :
Σ ( has-associative-mul (type-Semigroup G))
( λ μ → preserves-mul-Semigroup G (pair (set-Semigroup G) μ) id)
pr1 (pr1 (center-total-preserves-mul-id-Semigroup)) = mul-Semigroup G
pr2 (pr1 (center-total-preserves-mul-id-Semigroup)) =
associative-mul-Semigroup G
pr2 (center-total-preserves-mul-id-Semigroup) = refl

contraction-total-preserves-mul-id-Semigroup :
( t : Σ ( has-associative-mul (type-Semigroup G))
( λ μ →
preserves-mul-Semigroup G (pair (set-Semigroup G) μ) id)) →
Id center-total-preserves-mul-id-Semigroup t
contraction-total-preserves-mul-id-Semigroup
( (μ-G' , associative-G') , μ-id) =
eq-type-subtype
( λ μ →
preserves-mul-prop-Semigroup G (pair (set-Semigroup G) μ) id)
( eq-type-subtype
( λ μ →
Π-Prop
( type-Semigroup G)
( λ x →
Π-Prop
( type-Semigroup G)
( λ y →
Π-Prop
( type-Semigroup G)
( λ z →
Id-Prop
( set-Semigroup G)
( μ (μ x y) z) (μ x (μ y z))))))
( eq-htpy (λ x → eq-htpy (λ y → μ-id))))

is-torsorial-preserves-mul-id-Semigroup :
is-torsorial
( λ (μ : has-associative-mul (type-Semigroup G)) →
preserves-mul (mul-Semigroup G) (pr1 μ) id)
pr1 is-torsorial-preserves-mul-id-Semigroup =
center-total-preserves-mul-id-Semigroup
pr2 is-torsorial-preserves-mul-id-Semigroup =
contraction-total-preserves-mul-id-Semigroup

is-torsorial-equiv-Semigroup :
is-torsorial (equiv-Semigroup G)
is-torsorial-equiv-Semigroup =
is-torsorial-Eq-structure
( is-torsorial-Eq-subtype
( is-torsorial-equiv (type-Semigroup G))
( is-prop-is-set)
( type-Semigroup G)
( id-equiv)
( is-set-type-Semigroup G))
( pair (set-Semigroup G) id-equiv)
( is-torsorial-preserves-mul-id-Semigroup)