The category of semigroups

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

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

module group-theory.category-of-semigroups where
Imports 
open import category-theory.categories
open import category-theory.large-categories

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.universe-levels

open import group-theory.isomorphisms-semigroups
open import group-theory.precategory-of-semigroups
open import group-theory.semigroups

Idea

Since isomorphic semigroups are equal, the precategory of semigroups is a category.

Definition

The large category of semigroups

is-large-category-Semigroup :
  is-large-category-Large-Precategory Semigroup-Large-Precategory
is-large-category-Semigroup G =
  fundamental-theorem-id (is-torsorial-iso-Semigroup G) (iso-eq-Semigroup G)

extensionality-Semigroup :
  {l : Level} (G H : Semigroup l) → Id G H ≃ iso-Semigroup G H
pr1 (extensionality-Semigroup G H) = iso-eq-Semigroup G H
pr2 (extensionality-Semigroup G H) = is-large-category-Semigroup G H

eq-iso-Semigroup :
  {l : Level} (G H : Semigroup l) → iso-Semigroup G H → Id G H
eq-iso-Semigroup G H = map-inv-is-equiv (is-large-category-Semigroup G H)

Semigroup-Large-Category : Large-Category lsuc (_⊔_)
large-precategory-Large-Category Semigroup-Large-Category =
  Semigroup-Large-Precategory
is-large-category-Large-Category Semigroup-Large-Category =
  is-large-category-Semigroup

The category of small semigroups

Semigroup-Category : (l : Level) → Category (lsuc l) l
Semigroup-Category = category-Large-Category Semigroup-Large-Category

Recent changes