open import Algebra.Semigroup using (is-semigroup)
open import Algebra.Monoid using (is-monoid)
open import Algebra.Group
open import Algebra.Magma using (is-magma)

open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Properties
open import Cat.Prelude

import Cat.Reasoning as Cat

module Algebra.Group.Cat.Base where

private variable
  β„“ : Level
open Cat.Displayed.Univalence.Thin public
open Functor
import Cat.Reasoning as CR

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)

LiftGroup : βˆ€ {β„“} β„“' β†’ Group β„“ β†’ Group (β„“ βŠ” β„“')
LiftGroup {β„“} β„“' G = G' where
  module G = Group-on (G .snd)
  open is-group
  open is-monoid
  open is-semigroup
  open is-magma

  G' : Group (β„“ βŠ” β„“')
  G' .fst = el! (Lift β„“' ⌞ G ⌟)
  G' .snd ._⋆_ (lift x) (lift y) = lift (x G.⋆ y)
  G' .snd .has-is-group .unit = lift G.unit
  G' .snd .has-is-group .inverse (lift x) = lift (G.inverse x)
  G' .snd .has-is-group .has-is-monoid .has-is-semigroup .has-is-magma .has-is-set = hlevel 2
  G' .snd .has-is-group .has-is-monoid .has-is-semigroup .associative = ap lift G.associative
  G' .snd .has-is-group .has-is-monoid .idl = ap lift G.idl
  G' .snd .has-is-group .has-is-monoid .idr = ap lift G.idr
  G' .snd .has-is-group .inversel = ap lift G.inversel
  G' .snd .has-is-group .inverser = ap lift G.inverser

Gβ†’LiftG : βˆ€ {β„“} (G : Group β„“) β†’ Groups.Hom G (LiftGroup lzero G)
G→LiftG G .hom = lift
Gβ†’LiftG G .preserves .pres-⋆ _ _ = refl

The underlying setπŸ”—

The category of groups admits a faithful functor into the category of sets, written 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.

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

Grpβ†ͺSets-is-faithful : is-faithful (Grpβ†ͺSets {β„“})
Grpβ†ͺSets-is-faithful = Structured-hom-path (Group-structure _)