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.idl â©âĄË 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 p .Ïâââšâ© = GrpâȘSets-is-faithful refl p .Ïâââšâ© = GrpâȘSets-is-faithful refl p .unique 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