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π

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 or as

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.idl x = refl

Zero-group-is-initial : is-initial (Groups β) Zero-group
Zero-group-is-initial (_ , G) .centre = total-hom (Ξ» x β G.unit) gh where
module G = Group-on G
gh : is-group-hom _ _ (Ξ» x β G.unit)
gh .pres-β x y =
G.unit            β‘Λ
G.unit G.β G.unit β
Zero-group-is-initial (_ , G) .paths x =
ext Ξ» _ β sym (is-group-hom.pres-id (x .preserves))

Zero-group-is-terminal : is-terminal (Groups β) Zero-group
Zero-group-is-terminal _ .centre =
total-hom (Ξ» _ β lift tt) record { pres-β = Ξ» _ _ _ β lift tt }
Zero-group-is-terminal _ .paths x = trivial!

Zero-group-is-zero : is-zero (Groups β) Zero-group
Zero-group-is-zero = record
{ has-is-initial = Zero-group-is-initial
; has-is-terminal = Zero-group-is-terminal
}

βα΄³ : Zero (Groups β)
βα΄³ .Zero.β = Zero-group
βα΄³ .Zero.has-is-zero = Zero-group-is-zero

## Direct productsπ

We compute the product of two groups 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 2
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β _,_ G.associative H.associative
GΓHg .make-group.invl x = apβ _,_ G.inversel H.inversel
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 # x , g # x
factor f g .preserves .pres-β x y = apβ _,_ (f .preserves .pres-β _ _) (g .preserves .pres-β _ _)

Direct-product-is-product : is-product (Groups β) {G} {H} projβ projβ
Direct-product-is-product {G} {H} = p where
open is-product
p : is-product _ _ _
p .Οββfactor = GrpβͺSets-is-faithful refl
p .Οββfactor = GrpβͺSets-is-faithful refl
p .unique other p q = GrpβͺSets-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: 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 = GrpβͺSets-is-faithful (funext Ξ» e i β (x i # 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 = GrpβͺSets-is-faithful (funext Ξ» e i β (x i # e) .snd)

## Equalisersπ

open import Cat.Diagram.Equaliser

The equaliser of two group homomorphisms 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 = is-group-hom (f .preserves)
module g = is-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 together with a proof that To βliftβ the group structure from to we must prove that, if and then But this follows from and 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 # (G .snd ._β_ a b) β‘ g # (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 # (G.inverse x) β‘ g # (G.inverse x)
q = f.pres-inv Β·Β· ap H._β»ΒΉ p Β·Β· sym g.pres-inv

abstract
invs : f # G.unit β‘ g # 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! G.associative
equ-group .make-group.invl x = Ξ£-prop-path! G.inversel
equ-group .make-group.idl x = Ξ£-prop-path! G.idl

open is-equaliser
open Equaliser

We can then, pretty effortlessly, prove that the Equaliser-group, together with the canonical injection equalise the group homomorphisms and

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 = GrpβͺSets-is-faithful seq.equal
Groups-equalisers .has-is-eq .universal {F = F} {e'} p = total-hom go lim-gh where
go = seq.universal {F = underlying-set (F .snd)} (ap hom p)

lim-gh : is-group-hom _ _ go
lim-gh .pres-β x y = Ξ£-prop-path! (e' .preserves .pres-β _ _)

Groups-equalisers .has-is-eq .factors {F = F} {p = p} = GrpβͺSets-is-faithful
(seq.factors {F = underlying-set (F .snd)} {p = ap hom p})

Groups-equalisers .has-is-eq .unique {F = F} {p = p} q = GrpβͺSets-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 (Groups β)
top .Terminal.top = Zero-group
top .Terminal.hasβ€ = Zero-group-is-terminal

prod : β A B β Product (Groups β) 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