mathlib3 documentation

category_theory.category.Cat

Category of categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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