mathlib documentation

category_theory.category.Cat

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
@[nolint]
def category_theory.Cat  :
Type (max (u+1) u (v+1))

Category of categories.

Equations
Instances for category_theory.Cat
source
@[protected, instance]
def category_theory.Cat.inhabited  :
inhabited category_theory.Cat
Equations
source
@[protected, instance]
def category_theory.Cat.has_coe_to_sort  :
has_coe_to_sort category_theory.Cat (Type u)
Equations
source
@[protected, instance]
def category_theory.Cat.str (C : category_theory.Cat) :
category_theory.category ↥C
Equations
source
def category_theory.Cat.of (C : Type u) [category_theory.category C] :
category_theory.Cat

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

Equations
source
@[protected, instance]
def category_theory.Cat.bicategory  :
category_theory.bicategory category_theory.Cat

Bicategory structure on Cat

Equations
source
@[protected, instance]
def category_theory.Cat.bicategory.strict  :
category_theory.bicategory.strict category_theory.Cat

Cat is a strict bicategory.

source
@[protected, instance]
def category_theory.Cat.category  :
category_theory.large_category category_theory.Cat

Category structure on Cat

Equations
source
@[simp]
theorem category_theory.Cat.id_map {C : category_theory.Cat} {X Y : ↥C} (f : X ⟶ Y) :
(𝟙 C).map f = f
source
@[simp]
theorem category_theory.Cat.comp_obj {C D E : category_theory.Cat} (F : C ⟶ D) (G : D ⟶ E) (X : ↥C) :
(F ≫ G).obj X = G.obj (F.obj X)
source
@[simp]
theorem category_theory.Cat.comp_map {C D E : category_theory.Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↥C} (f : X ⟶ Y) :
(F ≫ G).map f = G.map (F.map f)
source
def category_theory.Cat.objects  :
category_theory.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
Instances for category_theory.Cat.objects
source
def category_theory.Cat.equiv_of_iso {C D : category_theory.Cat} (γ : C ≅ D) :
↥C ≌ ↥D

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

Equations
source
@[simp]
theorem category_theory.Type_to_Cat_map (X Y : Type u) (f : X ⟶ Y) :
category_theory.Type_to_Cat.map f = category_theory.discrete.functor (category_theory.discrete.mk ∘ f)
source
def category_theory.Type_to_Cat  :
Type u ⥤ category_theory.Cat

Embedding Type into Cat as discrete categories.

This ought to be modelled as a 2-functor!

Equations
Instances for category_theory.Type_to_Cat
source
@[simp]
theorem category_theory.Type_to_Cat_obj (X : Type u) :
category_theory.Type_to_Cat.obj X = category_theory.Cat.of (category_theory.discrete X)
source
@[protected, instance]
def category_theory.Type_to_Cat.faithful  :
category_theory.faithful category_theory.Type_to_Cat
source
@[protected, instance]
def category_theory.Type_to_Cat.full  :
category_theory.full category_theory.Type_to_Cat
Equations