module Algebra.Group.Cat.Base where

The category of groupsπŸ”—

The category of groups, as the name implies, has its objects the Groups, with the morphisms between them the group homomorphisms.

open Group-on
open is-group-hom

Group-structure : βˆ€ β„“ β†’ Thin-structure β„“ Group-on
Group-structure β„“ .is-hom f G G' = el! (is-group-hom G G' f)

Group-structure β„“ .id-is-hom        .pres-⋆ x y = refl
Group-structure β„“ .∘-is-hom f g Ξ± Ξ² .pres-⋆ x y =
  ap f (Ξ² .pres-⋆ x y) βˆ™ Ξ± .pres-⋆ _ _

Group-structure β„“ .id-hom-unique {s = s} {t = t} Ξ± Ξ² i =
  record
    { _⋆_          = Ξ» x y β†’ Ξ± .pres-⋆ x y i
    ; has-is-group =
      is-propβ†’pathp (Ξ» i β†’ is-group-is-prop {_*_ = Ξ» x y β†’ Ξ± .pres-⋆ x y i})
        (s .has-is-group)
        (t .has-is-group)
        i
    }

Groups : βˆ€ β„“ β†’ Precategory (lsuc β„“) β„“
Groups β„“ = Structured-objects (Group-structure β„“)

Groups-is-category : βˆ€ {β„“} β†’ is-category (Groups β„“)
Groups-is-category = Structured-objects-is-category (Group-structure _)

instance
  Groups-equational : βˆ€ {β„“} β†’ is-equational (Group-structure β„“)
  Groups-equational .is-equational.invert-id-hom x .pres-⋆ a b = sym (x .pres-⋆ a b)

module Groups {β„“} = Cat (Groups β„“)

Group : βˆ€ β„“ β†’ Type (lsuc β„“)
Group _ = Groups.Ob

to-group : βˆ€ {β„“} {A : Type β„“} β†’ make-group A β†’ Group β„“
to-group {A = A} mg = el A (mg .make-group.group-is-set) , (to-group-on mg)

The underlying setπŸ”—

The category of groups admits a faithful functor into the category of sets, written U:Groups→SetsU : \mathrm{Groups} \to \mathbf{Sets}, which projects out the underlying set of the group. Faithfulness of this functor says, in more specific words, that equality of group homomorphisms can be tested by comparing the underlying morphisms of sets.

Forget : Functor (Groups β„“) (Sets β„“)
Forget = Forget-structure (Group-structure _)

Forget-is-faithful : is-faithful (Forget {β„“})
Forget-is-faithful = Structured-hom-path (Group-structure _)