module Cat.Instances.Core where

The core of a categoryπŸ”—

The core of a category C\mathcal{C} is the maximal sub-groupoid of C\mathcal{C}: the category Core(C)\mathrm{Core}(\mathcal{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\mathcal{C}.

Core : βˆ€ {o β„“} β†’ Precategory o β„“ β†’ Precategory o β„“
Core C = Wide sub where
  open Cat.Reasoning C

  sub : Wide-subcat {C = 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)
    module C = Cat.Reasoning C
    module f-inv = (f .witness)

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

module _
  {oc β„“c od β„“d} {C : Precategory oc β„“c} {D : Precategory od β„“d}
  (grpd : is-pregroupoid C)

  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