open import Algebra.Prelude open import Algebra.Group open import Cat.Prelude 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.
Groups : β β β Precategory (lsuc β) β Groups β = c where open Precategory open Group-hom open Group-on c : Precategory _ _ c .Ob = Group β c .Hom A B = Group[ A β B ] c .Hom-set _ (B , bg) = hlevel 2 where open Group-on bg
We must show that the identity is a group homomorphisms, and group homs are closed under composition, but this follows immediately from the properties of equality:
c .id .fst = Ξ» x β x c .id .snd = record { pres-β = Ξ» _ _ β refl } c ._β_ {x} {y} {z} (f , fh) (g , gh) = (Ξ» x β f (g x)) , fogh where abstract fogh : Group-hom x z (Ξ» x β f (g x)) fogh .pres-β x y = ap f (gh .pres-β x y) β fh .pres-β _ _ c .idr f = Ξ£-prop-path (Ξ» _ β Group-hom-is-prop) refl c .idl f = Ξ£-prop-path (Ξ» _ β Group-hom-is-prop) refl c .assoc f g h = Ξ£-prop-path (Ξ» _ β Group-hom-is-prop) refl module Groups {β} = Cat (Groups β)
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.
Forget : Functor (Groups β) (Sets β) Forget .Fβ (G , ggroup) = G , ggroup .Group-on.has-is-set Forget .Fβ = fst Forget .F-id = refl Forget .F-β _ _ = refl Forget-is-faithful : is-faithful (Forget {β}) Forget-is-faithful = Ξ£-prop-path Ξ» _ β Group-hom-is-prop
Univalenceπ
The structure identity principle already implies that identification of groups is equivalent to isomorphism of groups. We now extend this to proving that the category of groups is univalent, but first we take a detour by showing that isomorphisms in the category of groups are the same thing as homomorphic equivalences of the groupsβ underlying types.
Group-equivβGroups-iso : β {A B : Group β} β (Ξ£ (Groupβ A B)) β (A Groups.β B) Group-equivβGroups-iso {A = A} {B = B} .fst ((f , eqv) , grh) = Groups.make-iso (f , grh) (equivβinverse eqv , inv-group-hom) (Forget-is-faithful (funext (equivβsection eqv))) (Forget-is-faithful (funext (equivβretraction eqv)))
To build an isomorphism given a homomorphic equivalence, we use Forget-is-faithful, reducing equality of morphisms in Groups to equality of morphisms in Sets. But then, the data of an equivalence guarantees that it has a two-sided inverse, so the only thing left to establish is that the inverse of a homomorphic equivalence is also homomorphic:
where module A = Group-on (A .snd) module B = Group-on (B .snd) open Group-hom g : B .fst β A .fst g = equivβinverse eqv abstract inv-group-hom : Group-hom B A g inv-group-hom .pres-β x y = g (x B.β y) β‘Λβ¨ apβ (Ξ» x y β g (x B.β y)) (equivβsection eqv _) (equivβsection eqv _) β©β‘Λ g (f (g x) B.β f (g y)) β‘Λβ¨ ap g (grh .pres-β _ _) β©β‘Λ g (f (g x A.β g y)) β‘β¨ equivβretraction eqv _ β©β‘ g x A.β g y β
With this equivalence in hands, we can establish that the category of groups is indeed univalent.
Groups-is-category : is-category (Groups β) Groups-is-category = isoβpathβis-category _ eqv where open is-iso eqv : β {A B} β (A β‘ B) β (A Groups.β B) eqv {A} {B} = (A β‘ B) ββ¨ SIP Group-univalent eβ»ΒΉ β©β Ξ£ (Groupβ A B) ββ¨ Group-equivβGroups-iso β©β (A Groups.β B) ββ