Documentation

Mathlib.CategoryTheory.Category.Cat.Limit

The category of small categories has all small limits. #

An object in the limit consists of a family of objects, which are carried to one another by the functors in the diagram. A morphism between two such objects is a family of morphisms between the corresponding objects, which are carried to one another by the action on morphisms of the functors in the diagram.

Future work #

Can the indexing category live in a lower universe?

source
instance CategoryTheory.Cat.HasLimits.categoryObjects {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} {j : J} :
CategoryTheory.SmallCategory ((F.comp CategoryTheory.Cat.objects).obj j)
Equations
  • CategoryTheory.Cat.HasLimits.categoryObjects = (F.obj j).str
source
@[simp]
theorem CategoryTheory.Cat.HasLimits.homDiagram_map {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) :
∀ {X_1 Y_1 : J} (f : X_1 ⟶ Y_1) (g : CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) X_1 X ⟶ CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) X_1 Y), (CategoryTheory.Cat.HasLimits.homDiagram X Y).map f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((F.map f).map g) (CategoryTheory.eqToHom ⋯))
source
@[simp]
theorem CategoryTheory.Cat.HasLimits.homDiagram_obj {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (j : J) :
(CategoryTheory.Cat.HasLimits.homDiagram X Y).obj j = (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j X ⟶ CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j Y)
source
def CategoryTheory.Cat.HasLimits.homDiagram {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) :
CategoryTheory.Functor J (Type v)

Auxiliary definition: the diagram whose limit gives the morphism space between two objects of the limit category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects_comp {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) {X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)} {Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)} {Z : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)} (f : X ⟶ Y) (g : Y ⟶ Z) :
    CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X Z) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f) (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram Y Z) j g)) ⋯
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects_id {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) :
    CategoryTheory.CategoryStruct.id X = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X X) (fun (j : J) => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j X)) ⋯
    source
    instance CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    CategoryTheory.Category.{v, v} (CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects))
    Equations
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.limitConeX_α {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    ↑(CategoryTheory.Cat.HasLimits.limitConeX F) = CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)
    source
    @[simp]
    theorem CategoryTheory.Cat.HasLimits.limitConeX_str {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    (CategoryTheory.Cat.HasLimits.limitConeX F).str = inferInstance
    source
    def CategoryTheory.Cat.HasLimits.limitConeX {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
    CategoryTheory.Cat

    Auxiliary definition: the limit category.

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_map {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) :
      ∀ {X Y : ↑(((CategoryTheory.Functor.const J).obj (CategoryTheory.Cat.HasLimits.limitConeX F)).obj j)} (f : X ⟶ Y), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).map f = CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j f
      source
      @[simp]
      theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_obj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) :
      ∀ (a : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).obj a = CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j a
      source
      @[simp]
      theorem CategoryTheory.Cat.HasLimits.limitCone_pt {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
      (CategoryTheory.Cat.HasLimits.limitCone F).pt = CategoryTheory.Cat.HasLimits.limitConeX F
      source
      def CategoryTheory.Cat.HasLimits.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
      CategoryTheory.Limits.Cone F

      Auxiliary definition: the cone over the limit category.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Cat.HasLimits.limitConeLift_obj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) :
        ∀ (a : { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } }.pt), (CategoryTheory.Cat.HasLimits.limitConeLift F s).obj a = CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } } a
        source
        @[simp]
        theorem CategoryTheory.Cat.HasLimits.limitConeLift_map {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) :
        ∀ {X Y : ↑s.pt} (f : X ⟶ Y), (CategoryTheory.Cat.HasLimits.limitConeLift F s).map f = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } } X) (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).obj, naturality := ⋯ } } Y)) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((s.π.app j).map f) (CategoryTheory.eqToHom ⋯))) ⋯
        source
        def CategoryTheory.Cat.HasLimits.limitConeLift {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) :
        s.pt ⟶ CategoryTheory.Cat.HasLimits.limitConeX F

        Auxiliary definition: the universal morphism to the proposed limit cone.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)) (j : J) (h : X = Y) :
          CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
          source
          def CategoryTheory.Cat.HasLimits.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) :
          CategoryTheory.Limits.IsLimit (CategoryTheory.Cat.HasLimits.limitCone F)

          Auxiliary definition: the proposed cone is a limit cone.

          Equations
          Instances For
            source
            instance CategoryTheory.Cat.instHasLimits :
            CategoryTheory.Limits.HasLimits CategoryTheory.Cat

            The category of small categories has all small limits.

            Equations
            source
            instance CategoryTheory.Cat.instPreservesLimitsObjects :
            CategoryTheory.Limits.PreservesLimits CategoryTheory.Cat.objects
            Equations
            • One or more equations did not get rendered due to their size.