# Category of categories #

This file contains the definition of the category `Cat` of all categories. In this category objects are categories and morphisms are functors between these categories.

## Implementation notes #

Though `Cat` is not a concrete category, we use `bundled` to define its carrier type.

source
def CategoryTheory.Cat :
Type (max (u + 1) u (v + 1))

Category of categories.

Equations

- CategoryTheory.Cat = CategoryTheory.Bundled CategoryTheory.Category.{?u.3, ?u.2}

Instances For

source
instance CategoryTheory.Cat.instInhabited :
Inhabited Cat
Equations

- CategoryTheory.Cat.instInhabited = { default := { α := Type ?u.2, str := CategoryTheory.types } }

source
instance CategoryTheory.Cat.instCoeSortType :
CoeSort Cat (Type u)
Equations

- CategoryTheory.Cat.instCoeSortType = { coe := CategoryTheory.Bundled.α }

source
instance CategoryTheory.Cat.str (C : Cat) :
Category.{v, u} ↑C
Equations

- C.str = C.str

source
def CategoryTheory.Cat.of (C : Type u) [Category.{v, u} C] :
Cat

Construct a bundled `Cat` from the underlying type and the typeclass.

Equations

- CategoryTheory.Cat.of C = CategoryTheory.Bundled.of C

Instances For

source
instance CategoryTheory.Cat.bicategory :
Bicategory Cat

Bicategory structure on `Cat`

Equations

- One or more equations did not get rendered due to their size.

source
instance CategoryTheory.Cat.bicategory.strict :
Bicategory.Strict Cat

`Cat` is a strict bicategory.

source
instance CategoryTheory.Cat.category :
LargeCategory Cat

Category structure on `Cat`

Equations

- CategoryTheory.Cat.category = CategoryTheory.StrictBicategory.category CategoryTheory.Cat

source
theorem CategoryTheory.Cat.ext {C D : Cat} {F G : C ⟶ D} {α β : F ⟶ G} (w : α.app = β.app) :
α = β
source
theorem CategoryTheory.Cat.ext_iff {C D : Cat} {F G : C ⟶ D} {α β : F ⟶ G} :
α = β ↔ α.app = β.app
source
@[simp]
theorem CategoryTheory.Cat.id_obj {C : Cat} (X : ↑C) :
(CategoryStruct.id C).obj X = X
source
@[simp]
theorem CategoryTheory.Cat.id_map {C : Cat} {X Y : ↑C} (f : X ⟶ Y) :
(CategoryStruct.id C).map f = f
source
@[simp]
theorem CategoryTheory.Cat.comp_obj {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) :
(CategoryStruct.comp F G).obj X = G.obj (F.obj X)
source
@[simp]
theorem CategoryTheory.Cat.comp_map {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↑C} (f : X ⟶ Y) :
(CategoryStruct.comp F G).map f = G.map (F.map f)
source
@[simp]
theorem CategoryTheory.Cat.id_app {C D : Cat} (F : C ⟶ D) (X : ↑C) :
(CategoryStruct.id F).app X = CategoryStruct.id (F.obj X)
source
@[simp]
theorem CategoryTheory.Cat.comp_app {C D : Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) :
(CategoryStruct.comp α β).app X = CategoryStruct.comp (α.app X) (β.app X)
source
@[simp]
theorem CategoryTheory.Cat.eqToHom_app {C D : Cat} (F G : C ⟶ D) (h : F = G) (X : ↑C) :
(eqToHom h).app X = eqToHom ⋯
source
@[simp]
theorem CategoryTheory.Cat.whiskerLeft_app {C D E : Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : ↑C) :
(Bicategory.whiskerLeft F η).app X = η.app (F.obj X)
source
@[simp]
theorem CategoryTheory.Cat.whiskerRight_app {C D E : Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : ↑C) :
(Bicategory.whiskerRight η H).app X = H.map (η.app X)
source
theorem CategoryTheory.Cat.leftUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :
(Bicategory.leftUnitor F).hom.app X = eqToHom ⋯
source
theorem CategoryTheory.Cat.leftUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :
(Bicategory.leftUnitor F).inv.app X = eqToHom ⋯
source
theorem CategoryTheory.Cat.rightUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :
(Bicategory.rightUnitor F).hom.app X = eqToHom ⋯
source
theorem CategoryTheory.Cat.rightUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :
(Bicategory.rightUnitor F).inv.app X = eqToHom ⋯
source
theorem CategoryTheory.Cat.associator_hom_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) :
(Bicategory.associator F G H).hom.app X = eqToHom ⋯
source
theorem CategoryTheory.Cat.associator_inv_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) :
(Bicategory.associator F G H).inv.app X = eqToHom ⋯
source
theorem CategoryTheory.Cat.id_eq_id (X : Cat) :
CategoryStruct.id X = Functor.id ↑X

The identity in the category of categories equals the identity functor.

source
theorem CategoryTheory.Cat.comp_eq_comp {X Y Z : Cat} (F : X ⟶ Y) (G : Y ⟶ Z) :
CategoryStruct.comp F G = Functor.comp F G

Composition in the category of categories equals functor composition.

source
@[simp]
theorem CategoryTheory.Cat.of_α (C : Type u_1) [Category.{u_2, u_1} C] :
↑(of C) = C
source
@[simp]
theorem CategoryTheory.Cat.coe_of (C : Cat) :
of ↑C = C
source
def CategoryTheory.Functor.toCatHom {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) :
Cat.of C ⟶ Cat.of D

Functors between categories of the same size define arrows in `Cat`.

Equations

- F.toCatHom = F

Instances For

source
def CategoryTheory.Functor.ofCatHom {C D : Type} [Category.{u_1, 0} C] [Category.{u_1, 0} D] (F : Cat.of C ⟶ Cat.of D) :
Functor C D

Arrows in `Cat` define functors.

Equations

- CategoryTheory.Functor.ofCatHom F = F

Instances For

source
@[simp]
theorem CategoryTheory.Functor.to_ofCatHom {C D : Type} [Category.{u_1, 0} C] [Category.{u_1, 0} D] (F : Cat.of C ⟶ Cat.of D) :
(ofCatHom F).toCatHom = F
source
@[simp]
theorem CategoryTheory.Functor.of_toCatHom {C D : Type} [Category.{u_1, 0} C] [Category.{u_1, 0} D] (F : Functor C D) :
ofCatHom F.toCatHom = F
source
def CategoryTheory.Cat.objects :
Functor Cat (Type u)

Functor that gets the set of objects of a category. It is not called `forget`, because it is not a faithful functor.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance CategoryTheory.Cat.instCategoryObjObjects (X : Cat) :
Category.{v, u} (objects.obj X)

See through the defeq `objects.obj X = X`.

Equations

- X.instCategoryObjObjects = inferInstanceAs (CategoryTheory.Category.{?u.7, ?u.6} ↑X)

source
def CategoryTheory.Cat.equivOfIso {C D : Cat} (γ : C ≅ D) :
↑C ≌ ↑D

Any isomorphism in `Cat` induces an equivalence of the underlying categories.

Equations

- CategoryTheory.Cat.equivOfIso γ = { functor := γ.hom, inverse := γ.inv, unitIso := CategoryTheory.eqToIso ⋯, counitIso := CategoryTheory.eqToIso ⋯, functor_unitIso_comp := ⋯ }

Instances For

source
def CategoryTheory.Cat.isoOfEquiv {C D : Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) :
C ≅ D

Under certain hypotheses, an equivalence of categories actually defines an isomorphism in `Cat`.

Equations

- CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄ = { hom := e.functor, inv := e.inverse, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Cat.isoOfEquiv_hom {C D : Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) :
(isoOfEquiv e h₁ h₂ h₃ h₄).hom = e.functor
source
@[simp]
theorem CategoryTheory.Cat.isoOfEquiv_inv {C D : Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) :
(isoOfEquiv e h₁ h₂ h₃ h₄).inv = e.inverse
source
def CategoryTheory.typeToCat :
Functor (Type u) Cat

Embedding `Type` into `Cat` as discrete categories.

This ought to be modelled as a 2-functor!

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.typeToCat_map {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) :
typeToCat.map f = Discrete.functor (Discrete.mk ∘ f)
source
@[simp]
theorem CategoryTheory.typeToCat_obj (X : Type u) :
typeToCat.obj X = Cat.of (Discrete X)
source
instance CategoryTheory.instFaithfulCatTypeToCat :
typeToCat.Faithful
source
instance CategoryTheory.instFullCatTypeToCat :
typeToCat.Full