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.

Instances For

source

@[implicit_reducible]

instance CategoryTheory.Cat.instInhabited :

Inhabited Cat

source

@[implicit_reducible]

instance CategoryTheory.Cat.instCoeSortType :

CoeSort Cat (Type u)

source

@[implicit_reducible]

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

Category.{v, u} ↑C

source

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

Cat

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

Instances For

source

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

)

Instances For

source

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

x = y

source

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

x = y ↔ x.toFunctor = y.toFunctor

source

@[implicit_reducible]

instance CategoryTheory.Cat.instQuiver :

Quiver Cat

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

The 1-morphism in Cat corresponding to a functor.

Instances For

source

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

source

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

F = G

source

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

F = G ↔ F.toFunctor = G.toFunctor

source

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.

Instances For

source

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

source

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

source

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.

Instances For

source

@[simp]

theorem CategoryTheory.Cat.Hom.equivFunctor_symm_apply (C D : Cat) (a✝ : Functor ↑C ↑D) :

(equivFunctor C D).symm a✝ = a✝.toCatHom

source

@[simp]

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

(equivFunctor C D) a✝ = a✝.toFunctor

source

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

)

Instances For

source

@[implicit_reducible]

instance CategoryTheory.Cat.Hom.instQuiver {C D : Cat} :

Quiver (C ⟶ D)

source

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.

Instances For

source

@[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 = η

source

@[implicit_reducible]

instance CategoryTheory.Cat.Hom.instCategory {X Y : Cat} :

Category.{max u v, max u v} (X ⟶ Y)

source

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

source

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

source

@[simp]

theorem CategoryTheory.Cat.Hom.toNatTrans_id {C D : Cat} (F : C ⟶ D) :

(CategoryStruct.id F).toNatTrans = CategoryStruct.id F.toFunctor

source

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

source

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

η₁ = η₂

source

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

η₁ = η₂ ↔ η₁.toNatTrans = η₂.toNatTrans

source

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.

Instances For

source

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

source

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

source

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

Instances For

source

@[simp]

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

(toNatIso e).inv = e.inv.toNatTrans

source

@[simp]

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

(toNatIso e).hom = e.hom.toNatTrans

source

@[simp]

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

isoMk (toNatIso e) = e

source

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

source

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

IsIso e.hom.toNatTrans

source

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

IsIso e.inv.toNatTrans

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[implicit_reducible]

instance CategoryTheory.Cat.bicategory :

Bicategory Cat

Bicategory structure on Cat

source

instance CategoryTheory.Cat.bicategory.strict :

Bicategory.Strict Cat

Cat is a strict bicategory.

source

@[implicit_reducible]

instance CategoryTheory.Cat.category :

LargeCategory Cat

Category structure on Cat

source

@[simp]

theorem CategoryTheory.Cat.Hom.id_toFunctor {C : Cat} :

(CategoryStruct.id C).toFunctor = Functor.id ↑C

source

@[simp]

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

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

source

@[simp]

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

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

source

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

source

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

source

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

source

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

source

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

source

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)

source

@[simp]

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

(eqToHom h).toNatTrans = eqToHom ⋯

source

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

(eqToHom h).toNatTrans.app X = eqToHom ⋯

source

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

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 η).toNatTrans.app X = η.toNatTrans.app (F.toFunctor.obj X)

source

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

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).toNatTrans.app X = H.toFunctor.map (η.toNatTrans.app X)

source

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_leftUnitor {B C : Cat} (F : B ⟶ C) :

toNatIso (Bicategory.leftUnitor F) = F.toFunctor.leftUnitor

source

@[simp]

theorem CategoryTheory.Cat.leftUnitor_hom_toNatTrans {B C : Cat} (F : B ⟶ C) :

(Bicategory.leftUnitor F).hom.toNatTrans = F.toFunctor.leftUnitor.hom

source

@[simp]

theorem CategoryTheory.Cat.leftUnitor_inv_toNatTrans {B C : Cat} (F : B ⟶ C) :

(Bicategory.leftUnitor F).inv.toNatTrans = F.toFunctor.leftUnitor.inv

source

theorem CategoryTheory.Cat.leftUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :

(Bicategory.leftUnitor F).hom.toNatTrans.app X = eqToHom ⋯

source

theorem CategoryTheory.Cat.leftUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :

(Bicategory.leftUnitor F).inv.toNatTrans.app X = eqToHom ⋯

source

@[simp]

theorem CategoryTheory.Cat.Hom.toNatIso_rightUnitor {B C : Cat} (F : B ⟶ C) :

toNatIso (Bicategory.rightUnitor F) = eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ eqToIso ⋯

source

@[simp]

theorem CategoryTheory.Cat.rightUnitor_hom_toNatTrans {B C : Cat} (F : B ⟶ C) :

(Bicategory.rightUnitor F).hom.toNatTrans = F.toFunctor.rightUnitor.hom

source

@[simp]

theorem CategoryTheory.Cat.rightUnitor_inv_toNatTrans {B C : Cat} (F : B ⟶ C) :

(Bicategory.rightUnitor F).inv.toNatTrans = F.toFunctor.rightUnitor.inv

source

theorem CategoryTheory.Cat.rightUnitor_hom_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :

(Bicategory.rightUnitor F).hom.toNatTrans.app X = eqToHom ⋯

source

theorem CategoryTheory.Cat.rightUnitor_inv_app {B C : Cat} (F : B ⟶ C) (X : ↑B) :

(Bicategory.rightUnitor F).inv.toNatTrans.app X = eqToHom ⋯

source

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

source

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

source

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

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

source

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.

source

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.

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

Instances For

source

@[implicit_reducible]

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

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

See through the defeq objects.obj X = X.

source

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

↑C ≌ ↑D

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

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.

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

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