Documentation

Mathlib.CategoryTheory.Limits.Over

Limits and colimits in the over and under categories #

Show that the forgetful functor forget X : Over X ⥤ C creates colimits, and hence Over X has any colimits that C has (as well as the dual that forget X : Under X ⟶ C creates limits).

Note that the folder CategoryTheory.Limits.Shapes.Constructions.Over further shows that forget X : Over X ⥤ C creates connected limits (so Over X has connected limits), and that Over X has J-indexed products if C has J-indexed wide pullbacks.

TODO: If C has binary products, then forget X : Over X ⥤ C has a right adjoint.

Equations
  • CategoryTheory.Over.createsColimitsOfSize = CategoryTheory.CostructuredArrow.createsColimitsOfSize

If c is a colimit cocone, then so is the cocone c.toOver with cocone point 𝟙 c.pt.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.Over.pullback_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X Y) (g : CategoryTheory.Over Y) {h : CategoryTheory.Over Y} {k : g h} :
    (CategoryTheory.Over.pullback f).map k = CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst k.left) CategoryTheory.Limits.pullback.snd )
    @[simp]

    When C has pullbacks, a morphism f : X ⟶ Y induces a functor Over Y ⥤ Over X, by pulling back a morphism along f.

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

      Over.map f is left adjoint to Over.pullback f.

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

        pullback (𝟙 A) : Over A ⥤ Over A is the identity functor.

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

          pullback commutes with composition (up to natural isomorphism).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • CategoryTheory.Under.createsLimitsOfSize = CategoryTheory.StructuredArrow.createsLimitsOfSize

            If c is a limit cone, then so is the cone c.toUnder with cone point 𝟙 c.pt.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem CategoryTheory.Under.pushout_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPushouts C] {X : C} {Y : C} (f : X Y) (g : CategoryTheory.Under X) {h : CategoryTheory.Under X} {k : g h} :
              (CategoryTheory.Under.pushout f).map k = CategoryTheory.Under.homMk (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp k.right CategoryTheory.Limits.pushout.inl) CategoryTheory.Limits.pushout.inr )

              When C has pushouts, a morphism f : X ⟶ Y induces a functor Under X ⥤ Under Y, by pushing a morphism forward along f.

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