open import Algebra.Group.Cat.Base
open import Algebra.Group

open import Cat.Instances.Sets.Complete as SL
open import Cat.Prelude

module Algebra.Group.Cat.FinitelyComplete {β„“} where

Finite limits of groupsπŸ”—

We present explicit computations of finite limits in the category of groups, though do note that the terminal group is also initial (i.e. it is a zero object). Knowing that the category of groups admits a right adjoint functor into the category of sets (the underlying set functor) drives us in computing limits of groups as limits of sets, and equipping those with a group structure: we are forced to do this since right adjoints preserve limits.

The zero groupπŸ”—

open import Cat.Diagram.Terminal (Groups β„“)
open import Cat.Diagram.Initial (Groups β„“)
open import Cat.Diagram.Zero (Groups β„“)

The zero object in the category of groups is given by the unit type, equipped with its unique group structure. Correspondingly, we may refer to this group in prose either as 00 or as {⋆}\{\star\}.

Zero-group : βˆ€ {β„“} β†’ Group β„“
Zero-group = to-group zg where
  zg : make-group (Lift _ ⊀)
  zg .make-group.group-is-set x y p q i j = lift tt
  zg .make-group.unit = lift tt
  zg .make-group.mul = Ξ» x y β†’ lift tt
  zg .make-group.inv x = lift tt
  zg .make-group.assoc x y z = refl
  zg .make-group.invl x = refl
  zg .make-group.invr x = refl
  zg .make-group.idl x = refl

Zero-group-is-initial : is-initial Zero-group
Zero-group-is-initial (_ , G) .centre = total-hom (Ξ» x β†’ G.unit) gh where
  module G = Group-on G
  gh : Group-hom _ _ (Ξ» x β†’ G.unit)
  gh .pres-⋆ x y =
    G.unit            β‰‘Λ˜βŸ¨ G.idl βŸ©β‰‘Λ˜
    G.unit G.⋆ G.unit ∎
Zero-group-is-initial (_ , G) .paths x =
  Homomorphism-path Ξ» _ β†’ sym (Group-hom.pres-id (x .preserves))

Zero-group-is-terminal : is-terminal Zero-group
Zero-group-is-terminal _ .centre =
  total-hom (Ξ» _ β†’ lift tt) record { pres-⋆ = Ξ» _ _ _ β†’ lift tt }
Zero-group-is-terminal _ .paths x = Homomorphism-path Ξ» _ β†’ refl

Zero-group-is-zero : is-zero Zero-group
Zero-group-is-zero = record
  { has-is-initial = Zero-group-is-initial
  ; has-is-terminal = Zero-group-is-terminal
  }

βˆ…α΄³ : Zero
βˆ…α΄³ .Zero.βˆ… = Zero-group
βˆ…α΄³ .Zero.has-is-zero = Zero-group-is-zero

Direct productsπŸ”—

open import Cat.Diagram.Product (Groups β„“)

We compute the product of two groups GΓ—HG \times H as the product of their underlying sets, equipped with the operation of β€œpointwise addition”.

Direct-product : Group β„“ β†’ Group β„“ β†’ Group β„“
Direct-product (G , Gg) (H , Hg) = to-group GΓ—Hg where
  module G = Group-on Gg
  module H = Group-on Hg

  GΓ—Hg : make-group (∣ G ∣ Γ— ∣ H ∣)
  GΓ—Hg .make-group.group-is-set = hlevel!
  GΓ—Hg .make-group.unit = G.unit , H.unit
  GΓ—Hg .make-group.mul (a , x) (b , y) = a G.⋆ b , x H.⋆ y
  GΓ—Hg .make-group.inv (a , x) = a G.⁻¹ , x H.⁻¹
  GΓ—Hg .make-group.assoc x y z = apβ‚‚ _,_ (sym G.associative) (sym H.associative)
  GΓ—Hg .make-group.invl x = apβ‚‚ _,_ G.inversel H.inversel
  GΓ—Hg .make-group.invr x = apβ‚‚ _,_ G.inverser H.inverser
  GΓ—Hg .make-group.idl x = apβ‚‚ _,_ G.idl H.idl

The projection maps and universal factoring are all given exactly as for the category of sets.

proj₁ : Groups.Hom (Direct-product G H) G
proj₁ .hom = fst
proj₁ .preserves .pres-⋆ x y = refl

projβ‚‚ : Groups.Hom (Direct-product G H) H
projβ‚‚ .hom = snd
projβ‚‚ .preserves .pres-⋆ x y = refl

factor : Groups.Hom G H β†’ Groups.Hom G K β†’ Groups.Hom G (Direct-product H K)
factor f g .hom x = f .hom x , g .hom x
factor f g .preserves .pres-⋆ x y = apβ‚‚ _,_ (f .preserves .pres-⋆ _ _) (g .preserves .pres-⋆ _ _)

Direct-product-is-product : is-product {G} {H} proj₁ projβ‚‚
Direct-product-is-product {G} {H} = p where
  open is-product
  p : is-product _ _
  p .⟨_,_⟩ = factor
  p .Ο€β‚βˆ˜factor = Forget-is-faithful refl
  p .Ο€β‚‚βˆ˜factor = Forget-is-faithful refl
  p .unique other p q = Forget-is-faithful (funext Ξ» x β†’
    apβ‚‚ _,_ (happly (ap hom p) x) (happly (ap hom q) x))

What sets the direct product of groups apart from (e.g.) the cartesian product of sets is that both β€œfactors” embed into the direct product, by taking the identity as the other coordinate: xβ†ͺ(x,1)x \hookrightarrow (x, 1). Indeed, in the category of abelian groups, the direct product is also a coproduct.

inj₁ : G Groups.β†ͺ Direct-product G H
inj₁ {G} {H} .mor .hom x = x , H .snd .unit
inj₁ {G} {H} .mor .preserves .pres-⋆ x y = ap (_ ,_) (sym (H .snd .idl))
inj₁ {G} {H} .monic g h x = Forget-is-faithful (funext Ξ» e i β†’ x i .hom e .fst)

injβ‚‚ : H Groups.β†ͺ Direct-product G H
injβ‚‚ {H} {G} .mor .hom x = G .snd .unit , x
injβ‚‚ {H} {G} .mor .preserves .pres-⋆ x y = ap (_, _) (sym (G .snd .idl))
injβ‚‚ {H} {G} .monic g h x = Forget-is-faithful (funext Ξ» e i β†’ x i .hom e .snd)

EqualisersπŸ”—

open import Cat.Diagram.Equaliser

The equaliser of two group homomorphisms f,g:G→Hf, g : G \to H is given by their equaliser as Set-morphisms, equipped with the evident group structure. Indeed, we go ahead and compute the actual Equaliser in sets, and re-use all of its infrastructure to make an equaliser in Groups.

module _ {G H : Group β„“} (f g : Groups.Hom G H) where
  private
    module G = Group-on (G .snd)
    module H = Group-on (H .snd)

    module f = Group-hom (f .preserves)
    module g = Group-hom (g .preserves)
    module seq = Equaliser
      (SL.Sets-equalisers
        {A = G.underlying-set}
        {B = H.underlying-set}
        (f .hom) (g .hom))

Recall that points there are elements of the domain (here, a point x:Gx : G) together with a proof that f(x)=g(x)f(x) = g(x). To β€œlift” the group structure from GG to equ(f,g)\id{equ}(f,g), we must prove that, if f(x)=g(x)f(x) = g(x) and f(y)=g(y)f(y) = g(y), then f(x⋆y)=g(x⋆y)f(x\star y) = g(x\star y). But this follows from ff and gg being group homomorphisms:

  Equaliser-group : Group β„“
  Equaliser-group = to-group equ-group where
    equ-⋆ : ∣ seq.apex ∣ β†’ ∣ seq.apex ∣ β†’ ∣ seq.apex ∣
    equ-⋆ (a , p) (b , q) = (a G.⋆ b) , r where abstract
      r : f .hom (G .snd ._⋆_ a b) ≑ g .hom (G .snd ._⋆_ a b)
      r = f.pres-⋆ a b Β·Β· apβ‚‚ H._⋆_ p q Β·Β· sym (g.pres-⋆ _ _)

    equ-inv : ∣ seq.apex ∣ β†’ ∣ seq.apex ∣
    equ-inv (x , p) = x G.⁻¹ , q where abstract
      q : f .hom (G.inverse x) ≑ g .hom (G.inverse x)
      q = f.pres-inv ·· ap H._⁻¹ p ·· sym g.pres-inv

    abstract
      invs : f .hom G.unit ≑ g .hom G.unit
      invs = f.pres-id βˆ™ sym g.pres-id

Similar yoga must be done for the inverse maps and the group unit.

    equ-group : make-group ∣ seq.apex ∣
    equ-group .make-group.group-is-set = seq.apex .is-tr
    equ-group .make-group.unit = G.unit , invs
    equ-group .make-group.mul = equ-⋆
    equ-group .make-group.inv = equ-inv
    equ-group .make-group.assoc x y z = Ξ£-prop-path (Ξ» _ β†’ H.has-is-set _ _) (sym G.associative)
    equ-group .make-group.invl x = Ξ£-prop-path (Ξ» _ β†’ H.has-is-set _ _) G.inversel
    equ-group .make-group.invr x = Ξ£-prop-path (Ξ» _ β†’ H.has-is-set _ _) G.inverser
    equ-group .make-group.idl x = Ξ£-prop-path (Ξ» _ β†’ H.has-is-set _ _) G.idl

  open is-equaliser
  open Equaliser

We can then, pretty effortlessly, prove that the Equaliser-group, together with the canonical injection equ(f,g)β†ͺG\id{equ}(f,g) \mono G, equalise the group homomorphisms ff and gg.

  Groups-equalisers : Equaliser (Groups β„“) f g
  Groups-equalisers .apex = Equaliser-group
  Groups-equalisers .equ = total-hom fst record { pres-⋆ = Ξ» x y β†’ refl }
  Groups-equalisers .has-is-eq .equal = Forget-is-faithful seq.equal
  Groups-equalisers .has-is-eq .limiting {F = F} {eβ€²} p = total-hom map lim-gh where
    map = seq.limiting {F = underlying-set (F .snd)} (ap hom p)

    lim-gh : Group-hom _ _ map
    lim-gh .pres-⋆ x y = Ξ£-prop-path (Ξ» _ β†’ H.has-is-set _ _) (eβ€² .preserves .pres-⋆ _ _)

  Groups-equalisers .has-is-eq .universal {F = F} {p = p} = Forget-is-faithful
    (seq.universal {F = underlying-set (F .snd)} {p = ap hom p})

  Groups-equalisers .has-is-eq .unique {F = F} {p = p} q = Forget-is-faithful
    (seq.unique {F = underlying-set (F .snd)} {p = ap hom p} (ap hom q))

Putting all of these constructions together, we get the proof that Groups is finitely complete, since we can compute pullbacks as certain equalisers.

open import Cat.Diagram.Limit.Finite

Groups-finitely-complete : Finitely-complete (Groups β„“)
Groups-finitely-complete = with-equalisers (Groups β„“) top prod Groups-equalisers
  where
    top : Terminal
    top .Terminal.top = Zero-group
    top .Terminal.has⊀ = Zero-group-is-terminal

    prod : βˆ€ A B β†’ Product A B
    prod A B .Product.apex = Direct-product A B
    prod A B .Product.π₁ = proj₁
    prod A B .Product.Ο€β‚‚ = projβ‚‚
    prod A B .Product.has-is-product = Direct-product-is-product