Functors from small to large categories

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-27.
Last modified on 2024-01-27.

module category-theory.functors-from-small-to-large-categories where
Imports 
open import category-theory.categories
open import category-theory.functors-from-small-to-large-precategories
open import category-theory.large-categories
open import category-theory.maps-from-small-to-large-categories

open import foundation.equivalences
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels

Idea

A functor from a (small) category C to a large category D consists of:

  • a map C → D on objects at some chosen universe level γ,
  • a map hom x y → hom (F x) (F y) on morphisms, such that the following identities hold:
  • F id_x = id_(F x),
  • F (g ∘ f) = F g ∘ F f.

Definition

The predicate on maps from small to large categories of being a functor

module _
  {l1 l2 γ : Level} {α : Level → Level} {β : Level → Level → Level}
  (C : Category l1 l2) (D : Large-Category α β)
  (F : map-Small-Large-Category C D γ)
  where

  preserves-comp-hom-map-Small-Large-Category : UU (l1 ⊔ l2 ⊔ β γ γ)
  preserves-comp-hom-map-Small-Large-Category =
    preserves-comp-hom-map-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  preserves-id-hom-map-Small-Large-Category : UU (l1 ⊔ β γ γ)
  preserves-id-hom-map-Small-Large-Category =
    preserves-id-hom-map-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  is-functor-map-Small-Large-Category : UU (l1 ⊔ l2 ⊔ β γ γ)
  is-functor-map-Small-Large-Category =
    is-functor-map-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  preserves-comp-is-functor-map-Small-Large-Category :
    is-functor-map-Small-Large-Category →
    preserves-comp-hom-map-Small-Large-Category
  preserves-comp-is-functor-map-Small-Large-Category =
    preserves-comp-is-functor-map-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  preserves-id-is-functor-map-Small-Large-Category :
    is-functor-map-Small-Large-Category →
    preserves-id-hom-map-Small-Large-Category
  preserves-id-is-functor-map-Small-Large-Category =
    preserves-id-is-functor-map-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

Functors from small to large categories

module _
  {l1 l2 : Level} {α : Level → Level} {β : Level → Level → Level}
  (C : Category l1 l2) (D : Large-Category α β)
  where

  functor-Small-Large-Category :
    (γ : Level) → UU (l1 ⊔ l2 ⊔ α γ ⊔ β γ γ)
  functor-Small-Large-Category =
    functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)

module _
  {l1 l2 : Level} {α : Level → Level} {β : Level → Level → Level}
  (C : Category l1 l2) (D : Large-Category α β)
  {γ : Level} (F : functor-Small-Large-Category C D γ)
  where

  obj-functor-Small-Large-Category :
    obj-Category C → obj-Large-Category D γ
  obj-functor-Small-Large-Category =
    obj-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  hom-functor-Small-Large-Category :
    {x y : obj-Category C} →
    (f : hom-Category C x y) →
    hom-Large-Category D
      ( obj-functor-Small-Large-Category x)
      ( obj-functor-Small-Large-Category y)
  hom-functor-Small-Large-Category =
    hom-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  map-functor-Small-Large-Category :
    map-Small-Large-Category C D γ
  map-functor-Small-Large-Category =
    map-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  is-functor-functor-Small-Large-Category :
    is-functor-map-Small-Large-Category C D
      ( map-functor-Small-Large-Category)
  is-functor-functor-Small-Large-Category =
    is-functor-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)

  preserves-comp-functor-Small-Large-Category :
    {x y z : obj-Category C}
    (g : hom-Category C y z) (f : hom-Category C x y) →
    ( hom-functor-Small-Large-Category (comp-hom-Category C g f)) ＝
    ( comp-hom-Large-Category D
      ( hom-functor-Small-Large-Category g)
      ( hom-functor-Small-Large-Category f))
  preserves-comp-functor-Small-Large-Category =
    preserves-comp-is-functor-map-Small-Large-Category C D
      ( map-functor-Small-Large-Category)
      ( is-functor-functor-Small-Large-Category)

  preserves-id-functor-Small-Large-Category :
    (x : obj-Category C) →
    ( hom-functor-Small-Large-Category (id-hom-Category C {x})) ＝
    ( id-hom-Large-Category D {γ} {obj-functor-Small-Large-Category x})
  preserves-id-functor-Small-Large-Category =
    preserves-id-is-functor-map-Small-Large-Category C D
      ( map-functor-Small-Large-Category)
      ( is-functor-functor-Small-Large-Category)

Properties

Characterizing equality of functors from small to large categories

Equality of functors is equality of underlying maps

module _
  {l1 l2 γ : Level} {α : Level → Level} {β : Level → Level → Level}
  (C : Category l1 l2) (D : Large-Category α β)
  (F G : functor-Small-Large-Category C D γ)
  where

  equiv-eq-map-eq-functor-Small-Large-Category :
    ( F ＝ G) ≃
    ( map-functor-Small-Large-Category C D F ＝
      map-functor-Small-Large-Category C D G)
  equiv-eq-map-eq-functor-Small-Large-Category =
    equiv-eq-map-eq-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)

  eq-map-eq-functor-Small-Large-Category :
    (F ＝ G) →
    ( map-functor-Small-Large-Category C D F ＝
      map-functor-Small-Large-Category C D G)
  eq-map-eq-functor-Small-Large-Category =
    map-equiv equiv-eq-map-eq-functor-Small-Large-Category

  eq-eq-map-functor-Small-Large-Category :
    ( map-functor-Small-Large-Category C D F ＝
      map-functor-Small-Large-Category C D G) →
    ( F ＝ G)
  eq-eq-map-functor-Small-Large-Category =
    map-inv-equiv equiv-eq-map-eq-functor-Small-Large-Category

  is-section-eq-eq-map-functor-Small-Large-Category :
    ( eq-map-eq-functor-Small-Large-Category ∘
      eq-eq-map-functor-Small-Large-Category) ~
    id
  is-section-eq-eq-map-functor-Small-Large-Category =
    is-section-map-inv-equiv equiv-eq-map-eq-functor-Small-Large-Category

  is-retraction-eq-eq-map-functor-Small-Large-Category :
    ( eq-eq-map-functor-Small-Large-Category ∘
      eq-map-eq-functor-Small-Large-Category) ~
    id
  is-retraction-eq-eq-map-functor-Small-Large-Category =
    is-retraction-map-inv-equiv equiv-eq-map-eq-functor-Small-Large-Category

Equality of functors is homotopy of underlying maps

module _
  {l1 l2 γ : Level} {α : Level → Level} {β : Level → Level → Level}
  (C : Category l1 l2) (D : Large-Category α β)
  (F G : functor-Small-Large-Category C D γ)
  where

  htpy-functor-Small-Large-Category : UU (l1 ⊔ l2 ⊔ α γ ⊔ β γ γ)
  htpy-functor-Small-Large-Category =
    htpy-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)

  equiv-htpy-eq-functor-Small-Large-Category :
    (F ＝ G) ≃ htpy-functor-Small-Large-Category
  equiv-htpy-eq-functor-Small-Large-Category =
    equiv-htpy-eq-functor-Small-Large-Precategory
      ( precategory-Category C)
      ( large-precategory-Large-Category D)
      ( F)
      ( G)

  htpy-eq-functor-Small-Large-Category :
    (F ＝ G) → htpy-functor-Small-Large-Category
  htpy-eq-functor-Small-Large-Category =
    map-equiv equiv-htpy-eq-functor-Small-Large-Category

  eq-htpy-functor-Small-Large-Category :
    htpy-functor-Small-Large-Category → F ＝ G
  eq-htpy-functor-Small-Large-Category =
    map-inv-equiv equiv-htpy-eq-functor-Small-Large-Category

  is-section-eq-htpy-functor-Small-Large-Category :
    ( htpy-eq-functor-Small-Large-Category ∘
      eq-htpy-functor-Small-Large-Category) ~
    id
  is-section-eq-htpy-functor-Small-Large-Category =
    is-section-map-inv-equiv equiv-htpy-eq-functor-Small-Large-Category

  is-retraction-eq-htpy-functor-Small-Large-Category :
    ( eq-htpy-functor-Small-Large-Category ∘
      htpy-eq-functor-Small-Large-Category) ~
    id
  is-retraction-eq-htpy-functor-Small-Large-Category =
    is-retraction-map-inv-equiv
      equiv-htpy-eq-functor-Small-Large-Category

See also

Recent changes