module Cat.Instances.Core where

# The core of a categoryπ

The **core** of a category
$C$
is the maximal sub-groupoid of
$C:$
the category
$Core(C)$
constructed by keeping only the invertible morphisms. Since the identity
is invertible, and invertibility is closed under composition, we can
construct this as a wide
subcategory of
$C.$

Core : β {o β} β Precategory o β β Precategory o β Core C = Wide sub where open Cat.Reasoning C sub : Wide-subcat C _ sub .Wide-subcat.P = is-invertible sub .Wide-subcat.P-prop _ = is-invertible-is-prop sub .Wide-subcat.P-id = id-invertible sub .Wide-subcat.P-β = invertible-β

Core-is-groupoid : β {o β} {C : Precategory o β} β is-pregroupoid (Core C) Core-is-groupoid {C = C} f = Core.make-invertible _ (wide f-inv.inv ((f .witness) C.invertibleβ»ΒΉ)) (Wide-hom-path f-inv.invl) (Wide-hom-path f-inv.invr) where module C = Cat.Reasoning C module f-inv = C.is-invertible (f .witness)

We have mentioned that the core is the *maximal* sub-groupoid
of
$C:$
we can regard it as the *cofree* groupoid on a category,
summarised by the following universal property. Suppose
$C$
is a groupoid and
$D$
is some category. Any functor
$F:CβD$
must factor through the core of
$D.$

module _ {oc βc od βd} {C : Precategory oc βc} {D : Precategory od βd} (grpd : is-pregroupoid C) where Core-universal : (F : Functor C D) β Functor C (Core D) Core-universal F .Fβ x = F .Fβ x Core-universal F .Fβ f .hom = F .Fβ f Core-universal F .Fβ f .witness = F-map-invertible F (grpd f) Core-universal F .F-id = Wide-hom-path (F .F-id) Core-universal F .F-β f g = Wide-hom-path (F .F-β f g) Core-factor : (F : Functor C D) β F β‘ Forget-wide-subcat Fβ Core-universal F Core-factor F = Functor-path (Ξ» _ β refl) Ξ» _ β refl

This is dual to the free groupoid on a category, in the sense that there is a biadjoint triple $Freeβ£Uβ£Core,$ where $U$ is the forgetful functor from the bicategory of groupoids to the bicategory of categories.