Documentation

Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Connected limits in the over category #

We show that the projection CostructuredArrow K B ⥤ C creates and preserves connected limits, without assuming that C has any limits. In particular, CostructuredArrow K B has any connected limit which C has.

From this we deduce the corresponding results for the over category.

(Implementation) Given a diagram in CostructuredArrow K B, produce a natural transformation from the diagram legs to the specific object.

Equations
Instances For

    (Implementation) Given a cone in the base category, raise it to a cone in CostructuredArrow K B. Note this is where the connected assumption is used.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem CategoryTheory.CostructuredArrow.CreatesConnected.raiseCone_π_app {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {K : Functor C D} [IsConnected J] {B : D} {F : Functor J (CostructuredArrow K B)} (c : Limits.Cone (F.comp (proj K B))) (j : J) :
      (raiseCone c).π.app j = homMk (c.π.app j)

      (Implementation) Show that the raised cone is a limit.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The projection from CostructuredArrow K B to C creates any connected limit.

        Equations
        • One or more equations did not get rendered due to their size.

        The forgetful functor from CostructuredArrow K B preserves any connected limit.

        The over category has any connected limit which the original category has.

        @[deprecated CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected (since := "2025-09-29")]

        Alias of CategoryTheory.Over.createsLimitsOfShapeForgetOfIsConnected.


        The forgetful functor from the over category creates any connected limit.

        Equations
        Instances For

          The forgetful functor from the over category preserves any connected limit.

          @[deprecated CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected (since := "2025-09-29")]

          Alias of CategoryTheory.Over.preservesLimitsOfShape_forget_of_isConnected.


          The forgetful functor from the over category preserves any connected limit.

          The over category has any connected limit which the original category has.

          The functor taking a cone over F to a cone over Over.post F : Over i ⥤ Over (F.obj i). This takes limit cones to limit cones when J is cofiltered. See isLimitConePost

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Over.conePost_obj_π_app {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) (c : Limits.Cone F) (X : Over i) :
            ((conePost F i).obj c).π.app X = homMk (c.π.app X.left)
            @[simp]
            theorem CategoryTheory.Over.conePost_obj_pt {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) (c : Limits.Cone F) :
            ((conePost F i).obj c).pt = mk (c.π.app i)
            @[simp]
            theorem CategoryTheory.Over.conePost_map_hom {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) (i : J) {X✝ Y✝ : Limits.Cone F} (f : X✝ Y✝) :
            ((conePost F i).map f).hom = homMk f.hom

            conePost is compatible with the forgetful functors on over categories.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def CategoryTheory.Over.isLimitConePost {J : Type u'} [Category.{v', u'} J] {C : Type u} [Category.{v, u} C] [IsCofilteredOrEmpty J] {F : Functor J C} {c : Limits.Cone F} (i : J) (hc : Limits.IsLimit c) :

              The functor taking a cone over F to a cone over Over.post F : Over i ⥤ Over (F.obj i) preserves limit cones

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For