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

theorem CategoryTheory.Cat.ext {C D : Cat} {F G : C ⟶ D} {α β : F ⟶ G} (w : α.app = β.app) :

α = β

source

theorem CategoryTheory.Cat.ext_iff {C D : Cat} {F G : C ⟶ D} {α β : F ⟶ G} :

α = β ↔ α.app = β.app

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.eqToHom_app {C D : Cat} (F G : C ⟶ D) (h : F = G) (X : ↑C) :

(eqToHom h).app X = eqToHom ⋯

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

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.{v_1, 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 u} [Category.{v, u} C] [Category.{v, u} 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 u} [Category.{v, u} C] [Category.{v, u} D] (F : Cat.of C ⟶ Cat.of D) :

(ofCatHom F).toCatHom = F

source

@[simp]

theorem CategoryTheory.Functor.of_toCatHom {C D : Type u} [Category.{v, u} C] [Category.{v, u} 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)

See through the defeq objects.obj X = X.

Equations

X.instCategoryObjObjects = inferInstanceAs (CategoryTheory.Category.{?u.7, ?u.6} ↑X)

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.Cat.isoOfEquiv {C D : Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) :

C ≅ D

Under certain hypotheses, an equivalence of categories actually defines an isomorphism in Cat.

Equations

CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄ = { hom := e.functor, inv := e.inverse, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Cat.isoOfEquiv_hom {C D : Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) :

(isoOfEquiv e h₁ h₂ h₃ h₄).hom = e.functor

source

@[simp]

theorem CategoryTheory.Cat.isoOfEquiv_inv {C D : Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = eqToHom ⋯ := by cat_disch) :

(isoOfEquiv e h₁ h₂ h₃ h₄).inv = e.inverse

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