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.

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

Category of categories.

Equations
Instances For
    source
    instance CategoryTheory.Cat.instInhabitedCat :
    Inhabited CategoryTheory.Cat
    Equations
    source
    instance CategoryTheory.Cat.instCoeSortCatType :
    CoeSort CategoryTheory.Cat (Type u)
    Equations
    source
    instance CategoryTheory.Cat.str (C : CategoryTheory.Cat) :
    CategoryTheory.Category.{v, u} ↑C
    Equations
    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
    Instances For
      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
      source
      instance CategoryTheory.Cat.category :
      CategoryTheory.LargeCategory CategoryTheory.Cat

      Category structure on Cat

      Equations
      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
      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
      Instances For
        source
        instance CategoryTheory.Cat.instCategoryObjCatToQuiverToCategoryStructCategoryTypeToQuiverToCategoryStructTypesToPrefunctorObjects (X : CategoryTheory.Cat) :
        CategoryTheory.Category.{v, u} (CategoryTheory.Cat.objects.obj X)
        Equations
        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
        • One or more equations did not get rendered due to their size.
        Instances For
          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
          @[simp]
          theorem CategoryTheory.typeToCat_obj (X : Type u) :
          CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)
          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.instFaithfulTypeTypesCatCategoryTypeToCat :
            CategoryTheory.Faithful CategoryTheory.typeToCat
            Equations
            source
            instance CategoryTheory.instFullTypeTypesCatCategoryTypeToCat :
            CategoryTheory.Full CategoryTheory.typeToCat
            Equations