Cores of categories

Content created by Fredrik Bakke.

Created on 2023-11-01.
Last modified on 2023-11-09.

module category-theory.cores-categories where

Imports

open import category-theory.categories
open import category-theory.cores-precategories
open import category-theory.groupoids
open import category-theory.isomorphisms-in-categories
open import category-theory.precategories
open import category-theory.pregroupoids
open import category-theory.subcategories
open import category-theory.wide-subcategories

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.universe-levels

Idea

The core of a category C is the maximal subgroupoid of it. It consists of all objects and isomorphisms in C.

Definitions

The core wide subcategory

module _
  {l1 l2 : Level} (C : Category l1 l2)
  where

  core-wide-subcategory-Category : Wide-Subcategory l2 C
  core-wide-subcategory-Category =
    core-wide-subprecategory-Precategory (precategory-Category C)

The core subcategory

module _
  {l1 l2 : Level} (C : Category l1 l2)
  where

  core-subcategory-Category : Subcategory lzero l2 C
  core-subcategory-Category =
    core-subprecategory-Precategory (precategory-Category C)

  is-wide-core-Category : is-wide-Subcategory C core-subcategory-Category
  is-wide-core-Category = is-wide-core-Precategory (precategory-Category C)

The core precategory

core-precategory-Category :
  {l1 l2 : Level} (C : Category l1 l2) → Precategory l1 l2
core-precategory-Category C =
  core-precategory-Precategory (precategory-Category C)

The core category

core-category-Category :
  {l1 l2 : Level} (C : Category l1 l2) → Category l1 l2
pr1 (core-category-Category C) = core-precategory-Category C
pr2 (core-category-Category C) =
  is-category-core-is-category-Precategory
    ( precategory-Category C)
    ( is-category-Category C)

The core pregroupoid

module _
  {l1 l2 : Level} (C : Category l1 l2)
  where

  is-pregroupoid-core-Category :
    is-pregroupoid-Precategory (core-precategory-Category C)
  is-pregroupoid-core-Category =
    is-pregroupoid-core-Precategory (precategory-Category C)

  core-pregroupoid-Category : Pregroupoid l1 l2
  core-pregroupoid-Category =
    core-pregroupoid-Precategory (precategory-Category C)

The core groupoid

module _
  {l1 l2 : Level} (C : Category l1 l2)
  where

  is-groupoid-core-Category : is-groupoid-Category (core-category-Category C)
  is-groupoid-core-Category = is-pregroupoid-core-Category C

  core-groupoid-Category : Groupoid l1 l2
  pr1 core-groupoid-Category = core-category-Category C
  pr2 core-groupoid-Category = is-groupoid-core-Category

Properties

Computing isomorphisms in the core

module _
  {l1 l2 : Level} (C : Category l1 l2) {x y : obj-Category C}
  where

  compute-iso-core-Category :
    iso-Category C x y ≃ iso-Category (core-category-Category C) x y
  compute-iso-core-Category =
    compute-iso-core-Precategory (precategory-Category C)

  inv-compute-iso-core-Category :
    iso-Category (core-category-Category C) x y ≃ iso-Category C x y
  inv-compute-iso-core-Category =
    inv-compute-iso-core-Precategory (precategory-Category C)