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.

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

Category of categories.

Equations

• CategoryTheory.Cat = CategoryTheory.Bundled CategoryTheory.Category.{?u.4, ?u.3}

instance CategoryTheory.Cat.instInhabited : Inhabited CategoryTheory.Cat

Equations

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

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

Equations

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

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

Equations

• C.str = C.str

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

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

Equations

• CategoryTheory.Cat.of C = CategoryTheory.Bundled.of C

instance CategoryTheory.Cat.bicategory : CategoryTheory.Bicategory CategoryTheory.Cat

Bicategory structure on Cat

Equations

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

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

Cat is a strict bicategory.

Equations

• CategoryTheory.Cat.bicategory.strict = ⋯

instance CategoryTheory.Cat.category : CategoryTheory.LargeCategory CategoryTheory.Cat

Category structure on Cat

Equations

• CategoryTheory.Cat.category = CategoryTheory.StrictBicategory.category CategoryTheory.Cat

@[simp]

theorem CategoryTheory.Cat.id_obj {C : CategoryTheory.Cat} (X : ↑C) : (CategoryTheory.CategoryStruct.id C).obj X = X

@[simp]

theorem CategoryTheory.Cat.id_map {C : CategoryTheory.Cat} {X : ↑C} {Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.id C).map f = f

@[simp]

theorem CategoryTheory.Cat.comp_obj {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) : (CategoryTheory.CategoryStruct.comp F G).obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.Cat.comp_map {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E) {X : ↑C} {Y : ↑C} (f : X ⟶ Y) : (CategoryTheory.CategoryStruct.comp F G).map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.Cat.id_app {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : C ⟶ D) (X : ↑C) : (CategoryTheory.CategoryStruct.id F).app X = CategoryTheory.CategoryStruct.id (F.obj X)

@[simp]

theorem CategoryTheory.Cat.comp_app {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {F : C ⟶ D} {G : C ⟶ D} {H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) : (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)

@[simp]

theorem CategoryTheory.Cat.whiskerLeft_app {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : C ⟶ D) {G : D ⟶ E} {H : D ⟶ E} (η : G ⟶ H) (X : ↑C) : (CategoryTheory.Bicategory.whiskerLeft F η).app X = η.app (F.obj X)

@[simp]

theorem CategoryTheory.Cat.whiskerRight_app {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} {F : C ⟶ D} {G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : ↑C) : (CategoryTheory.Bicategory.whiskerRight η H).app X = H.map (η.app X)

@[simp]

theorem CategoryTheory.Cat.eqToHom_app {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : C ⟶ D) (G : C ⟶ D) (h : F = G) (X : ↑C) : (CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.leftUnitor_hom_app {B : CategoryTheory.Cat} {C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.leftUnitor F).hom.app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.leftUnitor_inv_app {B : CategoryTheory.Cat} {C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.leftUnitor F).inv.app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.rightUnitor_hom_app {B : CategoryTheory.Cat} {C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.rightUnitor F).hom.app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.rightUnitor_inv_app {B : CategoryTheory.Cat} {C : CategoryTheory.Cat} (F : B ⟶ C) (X : ↑B) : (CategoryTheory.Bicategory.rightUnitor F).inv.app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.associator_hom_app {B : CategoryTheory.Cat} {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) : (CategoryTheory.Bicategory.associator F G H).hom.app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.associator_inv_app {B : CategoryTheory.Cat} {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) (X : ↑B) : (CategoryTheory.Bicategory.associator F G H).inv.app X = CategoryTheory.eqToHom ⋯

theorem CategoryTheory.Cat.id_eq_id (X : CategoryTheory.Cat) : CategoryTheory.CategoryStruct.id X = CategoryTheory.Functor.id ↑X

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

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

Composition in the category of categories equals functor composition.

@[simp]

theorem CategoryTheory.Cat.of_α (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : ↑(CategoryTheory.Cat.of C) = C

def CategoryTheory.Cat.objects : CategoryTheory.Functor CategoryTheory.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.

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

Equations

• X.instCategoryObjObjects = inferInstance

def CategoryTheory.Cat.equivOfIso {C : CategoryTheory.Cat} {D : CategoryTheory.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 := ⋯ }

@[simp]

theorem CategoryTheory.typeToCat_obj (X : Type u) : CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)

@[simp]

theorem CategoryTheory.typeToCat_map {X : Type u} {Y : Type u} (f : X ⟶ Y) : CategoryTheory.typeToCat.map f = id (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ f))

def CategoryTheory.typeToCat : CategoryTheory.Functor (Type u) CategoryTheory.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.

instance CategoryTheory.instFaithfulCatTypeToCat : CategoryTheory.typeToCat.Faithful

Equations

• CategoryTheory.instFaithfulCatTypeToCat = ⋯

instance CategoryTheory.instFullCatTypeToCat : CategoryTheory.typeToCat.Full

Equations

• CategoryTheory.instFullCatTypeToCat = ⋯