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.

def CategoryTheory.Cat : Type (max (u + 1) u (v + 1))

Category of categories.

@[implicit_reducible]

instance CategoryTheory.Cat.instInhabited : Inhabited Cat

@[implicit_reducible]

instance CategoryTheory.Cat.instCoeSortType : CoeSort Cat (Type u)

@[implicit_reducible]

instance CategoryTheory.Cat.str (C : Cat) : Category.{v, u} ↑C

def CategoryTheory.Cat.of (C : Type u) [Category.{v, u} C] : Cat

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

structure CategoryTheory.Cat.Hom (C D : Cat) : Type (max u v)

The type of 1-morphisms in the bicategory of categories Cat. This is a structure around Functor to prevent defeq-abuse

• ofFunctor :: (
• toFunctor : Functor ↑C ↑D

  The Functor underlying a 1-morphism in Cat

• )

theorem CategoryTheory.Cat.Hom.ext_iff {C D : Cat} {x y : C.Hom D} : x = y ↔ x.toFunctor = y.toFunctor

theorem CategoryTheory.Cat.Hom.ext {C D : Cat} {x y : C.Hom D} (toFunctor : x.toFunctor = y.toFunctor) : x = y

@[implicit_reducible]

instance CategoryTheory.Cat.instQuiver : Quiver Cat

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

The 1-morphism in Cat corresponding to a functor.

@[simp]

theorem CategoryTheory.Functor.toCatHom_toFunctor {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) : F.toCatHom.toFunctor = F

theorem CategoryTheory.Cat.ext {C D : Cat} {F G : C ⟶ D} (h : F.toFunctor = G.toFunctor) : F = G

theorem CategoryTheory.Cat.ext_iff {C D : Cat} {F G : C ⟶ D} : F = G ↔ F.toFunctor = G.toFunctor

def CategoryTheory.Functor.equivCatHom (C D : Type u) [Category.{v, u} C] [Category.{v, u} D] : Functor C D ≃ (Cat.of C ⟶ Cat.of D)

The equivalence between the type of functors between two categories and the type of 1-morphisms in Cat between the objects corresponding to those categories.

@[simp]

theorem CategoryTheory.Functor.equivCatHom_symm_apply (C D : Type u) [Category.{v, u} C] [Category.{v, u} D] (self : (Cat.of C).Hom (Cat.of D)) : (equivCatHom C D).symm self = self.toFunctor

@[simp]

theorem CategoryTheory.Functor.equivCatHom_apply (C D : Type u) [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) : (equivCatHom C D) F = F.toCatHom

def CategoryTheory.Cat.Hom.equivFunctor (C D : Cat) : (C ⟶ D) ≃ Functor ↑C ↑D

The equivalence between the type of 1-morphisms in Cat between two objects and the type of functors between the categories corresponding to those objects.

@[simp]

theorem CategoryTheory.Cat.Hom.equivFunctor_apply (C D : Cat) (a✝ : of ↑C ⟶ of ↑D) : (equivFunctor C D) a✝ = a✝.toFunctor

@[simp]

theorem CategoryTheory.Cat.Hom.equivFunctor_symm_apply (C D : Cat) (a✝ : Functor ↑C ↑D) : (equivFunctor C D).symm a✝ = a✝.toCatHom

structure CategoryTheory.Cat.Hom₂ {C D : Cat} (F G : C ⟶ D) : Type (max u v)

The type of 2-morphisms in the bicategory of categories Cat. This is a wrapper around NatTrans to prevent defeq-abuse.

• ofNatTrans :: (
• toNatTrans : F.toFunctor ⟶ G.toFunctor

  The natural transformation underlying a 2-morphism in Cat

• )

@[implicit_reducible]

instance CategoryTheory.Cat.Hom.instQuiver {C D : Cat} : Quiver (C ⟶ D)

def CategoryTheory.NatTrans.toCatHom₂ {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G : Functor C D} (η : F ⟶ G) : F.toCatHom ⟶ G.toCatHom

The 2-morphism in Cat corresponding to a natural transformation between functors.

@[simp]

theorem CategoryTheory.NatTrans.toCatHom₂_toNatTrans {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G : Functor C D} (η : F ⟶ G) : (toCatHom₂ η).toNatTrans = η

@[implicit_reducible]

instance CategoryTheory.Cat.Hom.instCategory {X Y : Cat} : Category.{max u v, max u v} (X ⟶ Y)

@[simp]

theorem CategoryTheory.NatTrans.toCatHom₂_id {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] (F : Functor C D) : toCatHom₂ (CategoryStruct.id F) = CategoryStruct.id F.toCatHom

@[simp]

theorem CategoryTheory.NatTrans.toCatHom₂_comp {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G H : Functor C D} (η₁ : F ⟶ G) (η₂ : G ⟶ H) : toCatHom₂ (CategoryStruct.comp η₁ η₂) = CategoryStruct.comp (toCatHom₂ η₁) (toCatHom₂ η₂)

@[simp]

theorem CategoryTheory.Cat.Hom.toNatTrans_id {C D : Cat} (F : C ⟶ D) : (CategoryStruct.id F).toNatTrans = CategoryStruct.id F.toFunctor

@[simp]

theorem CategoryTheory.Cat.Hom.toNatTrans_comp {C D : Cat} {F G H : C ⟶ D} (η₁ : F ⟶ G) (η₂ : G ⟶ H) : (CategoryStruct.comp η₁ η₂).toNatTrans = CategoryStruct.comp η₁.toNatTrans η₂.toNatTrans

theorem CategoryTheory.Cat.Hom₂.ext {C D : Cat} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G} (h : η₁.toNatTrans = η₂.toNatTrans) : η₁ = η₂

theorem CategoryTheory.Cat.Hom₂.ext_iff {C D : Cat} {F G : C ⟶ D} {η₁ η₂ : F ⟶ G} : η₁ = η₂ ↔ η₁.toNatTrans = η₂.toNatTrans

def CategoryTheory.Cat.Hom.isoMk {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G : Functor C D} (e : F ≅ G) : F.toCatHom ≅ G.toCatHom

The 2-iso in Cat corresponding to a natural isomorphism.

@[simp]

theorem CategoryTheory.Cat.Hom.isoMk_inv {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G : Functor C D} (e : F ≅ G) : (isoMk e).inv = NatTrans.toCatHom₂ e.inv

@[simp]

theorem CategoryTheory.Cat.Hom.isoMk_hom {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G : Functor C D} (e : F ≅ G) : (isoMk e).hom = NatTrans.toCatHom₂ e.hom

def CategoryTheory.Cat.Hom.toNatIso {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : F.toFunctor ≅ G.toFunctor

The natural isomorphism corresponding to a 2-iso in Cat

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_hom {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : (toNatIso e).hom = e.hom.toNatTrans

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_inv {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : (toNatIso e).inv = e.inv.toNatTrans

@[simp]

theorem CategoryTheory.Cat.Hom.isoMk_toNatIso {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : isoMk (toNatIso e) = e

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_isoMk {C D : Type u} [Category.{v, u} C] [Category.{v, u} D] {F G : Functor C D} (e : F ≅ G) : toNatIso (isoMk e) = e

instance CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransHomHom {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : IsIso e.hom.toNatTrans

instance CategoryTheory.Cat.Hom.instIsIsoFunctorαCategoryToNatTransInvHom {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : IsIso e.inv.toNatTrans

@[simp]

theorem CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryStruct.comp e.hom.toNatTrans e.inv.toNatTrans = CategoryStruct.id F.toFunctor

@[simp]

theorem CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_assoc {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) {Z : Functor ↑X ↑Y} (h : F.toFunctor ⟶ Z) : CategoryStruct.comp e.hom.toNatTrans (CategoryStruct.comp e.inv.toNatTrans h) = h

@[simp]

theorem CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryStruct.comp e.inv.toNatTrans e.hom.toNatTrans = CategoryStruct.id G.toFunctor

@[simp]

theorem CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_assoc {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) {Z : Functor ↑X ↑Y} (h : G.toFunctor ⟶ Z) : CategoryStruct.comp e.inv.toNatTrans (CategoryStruct.comp e.hom.toNatTrans h) = h

@[simp]

theorem CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) : CategoryStruct.comp (e.hom.toNatTrans.app A) (e.inv.toNatTrans.app A) = CategoryStruct.id (F.toFunctor.obj A)

@[simp]

theorem CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_app_assoc {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) {Z : ↑Y} (h : F.toFunctor.obj A ⟶ Z) : CategoryStruct.comp (e.hom.toNatTrans.app A) (CategoryStruct.comp (e.inv.toNatTrans.app A) h) = h

@[simp]

theorem CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) : CategoryStruct.comp (e.inv.toNatTrans.app A) (e.hom.toNatTrans.app A) = CategoryStruct.id (G.toFunctor.obj A)

@[simp]

theorem CategoryTheory.Cat.Hom.inv_hom_id_toNatTrans_app_assoc {X Y : Cat} {F G : X ⟶ Y} (e : F ≅ G) (A : ↑X) {Z : ↑Y} (h : G.toFunctor.obj A ⟶ Z) : CategoryStruct.comp (e.inv.toNatTrans.app A) (CategoryStruct.comp (e.hom.toNatTrans.app A) h) = h

@[implicit_reducible]

instance CategoryTheory.Cat.bicategory : Bicategory Cat

Bicategory structure on Cat

instance CategoryTheory.Cat.bicategory.strict : Bicategory.Strict Cat

Cat is a strict bicategory.

@[implicit_reducible]

instance CategoryTheory.Cat.category : LargeCategory Cat

Category structure on Cat

@[simp]

theorem CategoryTheory.Cat.Hom.id_toFunctor {C : Cat} : (CategoryStruct.id C).toFunctor = Functor.id ↑C

@[simp]

theorem CategoryTheory.Cat.Hom.id_obj {C : Cat} (X : ↑C) : (CategoryStruct.id C).toFunctor.obj X = X

@[simp]

theorem CategoryTheory.Cat.Hom.id_map {C : Cat} {X Y : ↑C} (f : X ⟶ Y) : (CategoryStruct.id C).toFunctor.map f = f

@[simp]

theorem CategoryTheory.Cat.Hom.comp_toFunctor {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) : (CategoryStruct.comp F G).toFunctor = F.toFunctor.comp G.toFunctor

@[simp]

theorem CategoryTheory.Cat.Hom.comp_obj {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C) : (CategoryStruct.comp F G).toFunctor.obj X = G.toFunctor.obj (F.toFunctor.obj X)

@[simp]

theorem CategoryTheory.Cat.Hom.comp_map {C D E : Cat} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↑C} (f : X ⟶ Y) : (CategoryStruct.comp F G).toFunctor.map f = G.toFunctor.map (F.toFunctor.map f)

@[simp]

theorem CategoryTheory.Cat.Hom₂.id_app {C D : Cat} (F : C ⟶ D) (X : ↑C) : (CategoryStruct.id F).toNatTrans.app X = CategoryStruct.id (F.toFunctor.obj X)

@[simp]

theorem CategoryTheory.Cat.Hom₂.comp_app {C D : Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) : (CategoryStruct.comp α β).toNatTrans.app X = CategoryStruct.comp (α.toNatTrans.app X) (β.toNatTrans.app X)

theorem CategoryTheory.Cat.Hom₂.comp_app_assoc {C D : Cat} {F G H : C ⟶ D} (α : F ⟶ G) (β : G ⟶ H) (X : ↑C) {Z : ↑D} (h : H.toFunctor.obj X ⟶ Z) : CategoryStruct.comp ((CategoryStruct.comp α β).toNatTrans.app X) h = CategoryStruct.comp (α.toNatTrans.app X) (CategoryStruct.comp (β.toNatTrans.app X) h)

@[simp]

theorem CategoryTheory.Cat.Hom₂.eqToHom_toNatTrans {C D : Cat} {F G : C ⟶ D} (h : F = G) : (eqToHom h).toNatTrans = eqToHom ⋯

theorem CategoryTheory.Cat.eqToHom_app {C D : Cat} (F G : C ⟶ D) (h : F = G) (X : ↑C) : (eqToHom h).toNatTrans.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Cat.whiskerLeft_toNatTrans {C D E : Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) : (Bicategory.whiskerLeft F η).toNatTrans = F.toFunctor.whiskerLeft η.toNatTrans

@[simp]

theorem CategoryTheory.Cat.whiskerLeft_app {C D E : Cat} (F : C ⟶ D) {G H : D ⟶ E} (η : G ⟶ H) (X : ↑C) : (Bicategory.whiskerLeft F η).toNatTrans.app X = η.toNatTrans.app (F.toFunctor.obj X)

@[simp]

theorem CategoryTheory.Cat.whiskerRight_toNatTrans {C D E : Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) : (Bicategory.whiskerRight η H).toNatTrans = Functor.whiskerRight η.toNatTrans H.toFunctor

@[simp]

theorem CategoryTheory.Cat.whiskerRight_app {C D E : Cat} {F G : C ⟶ D} (H : D ⟶ E) (η : F ⟶ G) (X : ↑C) : (Bicategory.whiskerRight η H).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_leftUnitor {B C : Cat} (F : B ⟶ C) : toNatIso (Bicategory.leftUnitor F) = F.toFunctor.leftUnitor

@[simp]

theorem CategoryTheory.Cat.leftUnitor_hom_toNatTrans {B C : Cat} (F : B ⟶ C) : (Bicategory.leftUnitor F).hom.toNatTrans = F.toFunctor.leftUnitor.hom

@[simp]

theorem CategoryTheory.Cat.leftUnitor_inv_toNatTrans {B C : Cat} (F : B ⟶ C) : (Bicategory.leftUnitor F).inv.toNatTrans = F.toFunctor.leftUnitor.inv

theorem CategoryTheory.Cat.leftUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : ↑B) : (Bicategory.leftUnitor F).hom.toNatTrans.app X = eqToHom ⋯

theorem CategoryTheory.Cat.leftUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : ↑B) : (Bicategory.leftUnitor F).inv.toNatTrans.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_rightUnitor {B C : Cat} (F : B ⟶ C) : toNatIso (Bicategory.rightUnitor F) = eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ eqToIso ⋯

@[simp]

theorem CategoryTheory.Cat.rightUnitor_hom_toNatTrans {B C : Cat} (F : B ⟶ C) : (Bicategory.rightUnitor F).hom.toNatTrans = F.toFunctor.rightUnitor.hom

@[simp]

theorem CategoryTheory.Cat.rightUnitor_inv_toNatTrans {B C : Cat} (F : B ⟶ C) : (Bicategory.rightUnitor F).inv.toNatTrans = F.toFunctor.rightUnitor.inv

theorem CategoryTheory.Cat.rightUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : ↑B) : (Bicategory.rightUnitor F).hom.toNatTrans.app X = eqToHom ⋯

theorem CategoryTheory.Cat.rightUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : ↑B) : (Bicategory.rightUnitor F).inv.toNatTrans.app X = eqToHom ⋯

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_associator {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) : toNatIso (Bicategory.associator F G H) = F.toFunctor.associator G.toFunctor H.toFunctor

@[simp]

theorem CategoryTheory.Cat.associator_hom_toNatTrans {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) : (Bicategory.associator F G H).hom.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).hom

@[simp]

theorem CategoryTheory.Cat.associator_inv_toNatTrans {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) : (Bicategory.associator F G H).inv.toNatTrans = (F.toFunctor.associator G.toFunctor H.toFunctor).inv

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.toNatTrans.app X = eqToHom ⋯

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.toNatTrans.app X = eqToHom ⋯

theorem CategoryTheory.Cat.id_eq_id (X : Cat) : (CategoryStruct.id X).toFunctor = Functor.id ↑X

The identity in the category of categories equals the identity functor.

theorem CategoryTheory.Cat.comp_eq_comp {X Y Z : Cat} (F : X ⟶ Y) (G : Y ⟶ Z) : (CategoryStruct.comp F G).toFunctor = F.toFunctor.comp G.toFunctor

Composition in the category of categories equals functor composition.

@[simp]

theorem CategoryTheory.Cat.of_α (C : Type u_1) [Category.{v_1, u_1} C] : ↑(of C) = C

@[simp]

theorem CategoryTheory.Cat.coe_of (C : Cat) : of ↑C = C

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.

@[implicit_reducible]

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

See through the defeq objects.obj X = X.

def CategoryTheory.Cat.equivOfIso {C D : Cat} (γ : C ≅ D) : ↑C ≌ ↑D

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

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.

@[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.toCatHom

@[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.toCatHom

def CategoryTheory.typeToCat : Functor (Type u) Cat

Embedding Type into Cat as discrete categories.

This ought to be modelled as a 2-functor!

@[simp]

theorem CategoryTheory.typeToCat_obj (X : Type u) : typeToCat.obj X = Cat.of (Discrete X)

@[simp]

theorem CategoryTheory.typeToCat_map {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : typeToCat.map f = (Discrete.functor (Discrete.mk ∘ f)).toCatHom

instance CategoryTheory.instFaithfulCatTypeToCat : typeToCat.Faithful

instance CategoryTheory.instFullCatTypeToCat : typeToCat.Full