🔍

Equations Inline Footnotes

open import Cat.Functor.WideSubcategory
open import Cat.Instances.Functor
open import Cat.Groupoid
open import Cat.Prelude

import Cat.Reasoning

module Cat.Instances.Core where

open Functor

The core of a category🔗

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

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-∘

private module Core {o ℓ} (C : Precategory o ℓ) = Cat.Reasoning (Core C)

module _ {o ℓ} {C : Precategory o ℓ} where
  private
    module C = Cat.Reasoning C

  Core-is-groupoid : is-pregroupoid (Core C)
  Core-is-groupoid 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 f-inv = C.is-invertible (f .witness)

Note that isomorphisms in $\mathcal{C}$ are equivalent to morphisms in the core of $\mathcal{C}\text{.}$ This means that if $\mathcal{C}$ is univalent, then we can transfer the associated identity system on isomorphisms to an identity system on morphisms of the core, and thus the core must be a univalent groupoid.

  iso≃Core-hom : ∀ {x y} → (x C.≅ y) ≃ Core.Hom C x y
  iso≃Core-hom {x} {y} =
    x C.≅ y                              ≃⟨ C.iso≃is-invertible ⟩≃
    Σ[ f ∈ C.Hom x y ] C.is-invertible f ≃˘⟨ Wide-hom≃witness ⟩≃˘
    Core.Hom C x y                       ≃∎

  Core-is-univalent-groupoid : is-category C → is-univalent-groupoid (Core C)
  Core-is-univalent-groupoid C-cat =
    transfer-identity-system C-cat (λ _ _ → iso≃Core-hom) λ _ → ext refl

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

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 $\mathrm{Free}⊣U⊣\mathrm{Core}\text{,}$ where $U$ is the forgetful functor from the bicategory of groupoids to the bicategory of categories.