Equivalences between semigroups

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

Created on 2022-03-17.
Last modified on 2024-01-11.

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)

Recent changes