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.4, ?u.3}

Instances For

source

instance CategoryTheory.Cat.instInhabited :

Inhabited CategoryTheory.Cat

Equations

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

source

instance CategoryTheory.Cat.instCoeSortType :

CoeSort CategoryTheory.Cat (Type u)

Equations

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

source

instance CategoryTheory.Cat.str (C : CategoryTheory.Cat) :

CategoryTheory.Category.{v, u} ↑C

Equations

C.str = C.str

source

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

source

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.

source

instance CategoryTheory.Cat.bicategory.strict :

CategoryTheory.Bicategory.Strict CategoryTheory.Cat

Cat is a strict bicategory.

Equations

CategoryTheory.Cat.bicategory.strict = ⋯

source

instance CategoryTheory.Cat.category :

CategoryTheory.LargeCategory CategoryTheory.Cat

Category structure on Cat

Equations

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

source

@[simp]

theorem CategoryTheory.Cat.id_obj {C : CategoryTheory.Cat} (X : ↑C) :

(CategoryTheory.CategoryStruct.id C).obj X = X

source

@[simp]

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

(CategoryTheory.CategoryStruct.id C).map f = f

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 ⋯

source

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 ⋯

source

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 ⋯

source

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 ⋯

source

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 ⋯

source

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 ⋯

source

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.

source

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.

source

@[simp]

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

↑(CategoryTheory.Cat.of C) = C

source

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.

source

instance CategoryTheory.Cat.instCategoryObjObjects (X : CategoryTheory.Cat) :

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

Equations

X.instCategoryObjObjects = inferInstance

source

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 := ⋯ }

source

@[simp]

theorem CategoryTheory.typeToCat_obj (X : Type u) :

CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)

source

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

source

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.

Instances For

source

instance CategoryTheory.instFaithfulCatTypeToCat :

CategoryTheory.typeToCat.Faithful

Equations

CategoryTheory.instFaithfulCatTypeToCat = ⋯

source

instance CategoryTheory.instFullCatTypeToCat :

CategoryTheory.typeToCat.Full

Equations

CategoryTheory.instFullCatTypeToCat = ⋯

Documentation

Mathlib.CategoryTheory.Category.Cat

Category of categories #

Implementation notes #