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 category_theory.Cat :

Type (max (u+1) u (v+1))

Category of categories.

Equations

category_theory.Cat = category_theory.bundled category_theory.category

source

@[instance]

def category_theory.Cat.inhabited :

inhabited category_theory.Cat

Equations

category_theory.Cat.inhabited = {default := {α := Type u, str := category_theory.types}}

source

@[instance]

def category_theory.Cat.has_coe_to_sort :

has_coe_to_sort category_theory.Cat

Equations

category_theory.Cat.has_coe_to_sort = {S := Type u, coe := category_theory.bundled.α category_theory.category}

source

@[instance]

def category_theory.Cat.str (C : category_theory.Cat) :

category_theory.category ↥C

Equations

C.str = C.str

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

category_theory.Cat.of C = category_theory.bundled.of C

source

@[instance]

def category_theory.Cat.category :

category_theory.large_category category_theory.Cat

Category structure on Cat

Equations

category_theory.Cat.category = {to_category_struct := {to_has_hom := {hom := λ (C D : category_theory.Cat), ↥C ⥤ ↥D}, id := λ (C : category_theory.Cat), 𝟭 ↥C, comp := λ (C D E : category_theory.Cat) (F : C ⟶ D) (G : D ⟶ E), F ⋙ G}, id_comp' := category_theory.Cat.category._proof_1, comp_id' := category_theory.Cat.category._proof_2, assoc' := category_theory.Cat.category._proof_3}

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

category_theory.Cat.objects = {obj := λ (C : category_theory.Cat), ↥C, map := λ (C D : category_theory.Cat) (F : C ⟶ D), F.obj, map_id' := category_theory.Cat.objects._proof_1, map_comp' := category_theory.Cat.objects._proof_2}

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

category_theory.Cat.equiv_of_iso γ = {functor := γ.hom, inverse := γ.inv, unit_iso := category_theory.eq_to_iso _, counit_iso := category_theory.eq_to_iso _, functor_unit_iso_comp' := _}

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

category_theory.Type_to_Cat = {obj := λ (X : Type u), category_theory.Cat.of (category_theory.discrete X), map := λ (X Y : Type u) (f : X ⟶ Y), category_theory.discrete.functor f, map_id' := category_theory.Type_to_Cat._proof_1, map_comp' := category_theory.Type_to_Cat._proof_2}

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

@[instance]

def category_theory.category_theory.faithful :

category_theory.faithful category_theory.Type_to_Cat

source

@[instance]

def category_theory.category_theory.full :

category_theory.full category_theory.Type_to_Cat

Equations

category_theory.category_theory.full = {preimage := λ (X Y : Type (max (max (max u_1 u_2 u_3 u_4) u_1 u_2 u_3) (max u_1 u_2 u_3 u_4) u_1 u_2)) (F : category_theory.Type_to_Cat.obj X ⟶ category_theory.Type_to_Cat.obj Y), F.obj, witness' := category_theory.category_theory.full._proof_1}