Documentation

Mathlib.CategoryTheory.Category.Cat

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.

Equations
Instances For

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

    Equations
    Instances For

      Bicategory structure on Cat

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.Cat.id_map {C : CategoryTheory.Cat} {X : C} {Y : C} (f : X Y) :
      @[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)
      @[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)
      @[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) :
      @[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)
      @[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)
      @[simp]
      theorem CategoryTheory.Cat.eqToHom_app {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} (F : C D) (G : C D) (h : F = G) (X : C) :

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

      Composition in the category of categories equals functor composition.

      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

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

        Equations
        Instances For
          @[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))

          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