Documentation

Mathlib.CategoryTheory.Comma.Over.Pullback

Adjunctions related to the over category #

In a category with pullbacks, for any morphism f : X ⟶ Y, the functor Over.map f : Over X ⥤ Over Y has a right adjoint Over.pullback f.

In a category with binary products, for any object X the functor Over.forget X : Over X ⥤ C has a right adjoint Over.star X.

Main declarations #

TODO #

Show star X itself has a right adjoint provided C is cartesian closed and has pullbacks.

def CategoryTheory.Over.pullback {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] {X Y : C} (f : X Y) :
Functor (Over Y) (Over X)

In a category with 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
    @[simp]
    @[simp]

    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
      @[simp]

      pullback (𝟙 X) : Over X ⥤ Over X 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
          def CategoryTheory.Over.postAdjunctionLeft {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPullbacks C] {X : C} {F : Functor C D} {G : Functor D C} (a : F G) :
          post F (post G).comp (pullback (a.unit.app X))

          If F is a left adjoint and its source category has pullbacks, then so is post F : Over Y ⥤ Over (G Y).

          If the right adjoint of F is G, then the right adjoint of post F is given by (Y ⟶ F X) ↦ (G Y ⟶ X ×_{G F X} G Y ⟶ X).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            noncomputable def CategoryTheory.Over.forgetMapTerminal {C : Type u} [Category.{v, u} C] (X : C) {T : C} (hT : Limits.IsTerminal T) :

            The category over any object X factors through the category over the terminal object T.

            Equations
            Instances For
              @[simp]
              @[simp]

              The functor from C to Over X which sends Y : C to π₁ : X ⨯ Y ⟶ X, sometimes denoted X*.

              Equations
              Instances For
                @[simp]
                theorem CategoryTheory.Over.star_map_left {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] {X✝ Y✝ : C} (f : X✝ Y✝) :
                @[simp]
                theorem CategoryTheory.Over.star_obj_left {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryProducts C] (X✝ : C) :
                ((star X).obj X✝).left = (X X✝)

                The functor Over.forget X : Over X ⥤ C has a right adjoint given by star X.

                Note that the binary products assumption is necessary: the existence of a right adjoint to Over.forget X is equivalent to the existence of each binary product X ⨯ -.

                Equations
                Instances For

                  Note that the binary products assumption is necessary: the existence of a right adjoint to Over.forget X is equivalent to the existence of each binary product X ⨯ -.

                  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
                    @[simp]
                    theorem CategoryTheory.Under.pushout_obj {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X Y) (x : Under X) :
                    @[simp]
                    theorem CategoryTheory.Under.pushout_map {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X Y) (x : Under X) {x' : Under X} {u : x x'} :

                    Under.pushout f is left adjoint to Under.map f.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Under.mapPushoutAdj_unit_app {C : Type u} [Category.{v, u} C] [Limits.HasPushouts C] {X Y : C} (f : X Y) (X✝ : Under X) :

                      pushout (𝟙 X) : Under X ⥤ Under X is the identity functor.

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

                        pushout commutes with composition (up to natural isomorphism).

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[deprecated CategoryTheory.Under.pushoutComp (since := "2025-04-15")]

                          Alias of CategoryTheory.Under.pushoutComp.


                          pushout commutes with composition (up to natural isomorphism).

                          Equations
                          Instances For
                            def CategoryTheory.Under.postAdjunctionRight {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasPushouts D] {Y : D} {F : Functor C D} {G : Functor D C} (a : F G) :

                            If G is a right adjoint and its source category has pushouts, then so is post G : Under Y ⥤ Under (G Y).

                            If the left adjoint of G is F, then the left adjoint of post G is given by (G Y ⟶ X) ↦ (Y ⟶ Y ⨿_{F G Y} F X ⟶ F X).

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              noncomputable def CategoryTheory.Under.forgetMapInitial {C : Type u} [Category.{v, u} C] (X : C) {I : C} (hI : Limits.IsInitial I) :

                              The category under any object X factors through the category under the initial object I.

                              Equations
                              Instances For
                                @[simp]
                                @[simp]

                                The functor from C to Under X which sends Y : C to in₁ : X ⟶ X ⨿ Y.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Under.costar_obj_left {C : Type u} [Category.{v, u} C] (X : C) [Limits.HasBinaryCoproducts C] (X✝ : C) :
                                  ((costar X).obj X✝).left = { as := PUnit.unit }

                                  The functor Under.forget X : Under X ⥤ C has a left adjoint given by costar X.

                                  Note that the binary coproducts assumption is necessary: the existence of a left adjoint to Under.forget X is equivalent to the existence of each binary coproduct X ⨿ -.

                                  Equations
                                  Instances For

                                    Note that the binary coproducts assumption is necessary: the existence of a left adjoint to Under.forget X is equivalent to the existence of each binary coproduct X ⨿ -.