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

@[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.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

@[simp]

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

(eqToHom h).app X = eqToHom ⋯

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)

Equations

X.instCategoryObjObjects = inferInstance

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

Documentation

Mathlib.CategoryTheory.Category.Cat

Category of categories #

Implementation notes #