Concrete monoids

Content created by Fredrik Bakke.

Created on 2023-09-15.
Last modified on 2023-11-01.

module group-theory.concrete-monoids where
Imports 
open import category-theory.categories

open import foundation.0-connected-types
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import group-theory.cores-monoids
open import group-theory.monoids
open import group-theory.torsors

Idea

A concrete monoid, or univalent monoid, is the homotopy type theoretic analogue of monoids. We define it as a category whose type of objects is pointed and connected.

Definition

is-concrete-monoid-Category : {l1 l2 : Level} → Category l1 l2 → UU l1
is-concrete-monoid-Category C = obj-Category C × is-0-connected (obj-Category C)

Concrete-Monoid : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
Concrete-Monoid l1 l2 = Σ (Category l1 l2) (is-concrete-monoid-Category)

module _
  {l1 l2 : Level} (M : Concrete-Monoid l1 l2)
  where

  category-Concrete-Monoid : Category l1 l2
  category-Concrete-Monoid = pr1 M

  is-concrete-monoid-category-Concrete-Monoid :
    is-concrete-monoid-Category category-Concrete-Monoid
  is-concrete-monoid-category-Concrete-Monoid = pr2 M

Properties

Concrete monoids from monoids

Given a monoid, we can define its associated concrete monoid. The type of objects is the classifying type of the core of the monoid. Moreover, we must take care in how we define the family of homomorphisms. They cannot simply be the constant family, as transporting along an invertible element should correspond to multiplying by the element in the family.

module _
  {l : Level} (M : Monoid l)
  where

  obj-concrete-monoid-Monoid : UU (lsuc l)
  obj-concrete-monoid-Monoid = classifying-type-Group (core-Monoid M)

The remainder of the construction remains to be written down. We note that this is precisely the Rezk completion of the one object precategory associated to a monoid.

Recent changes