Documentation

Mathlib.CategoryTheory.Adjunction.Over

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.

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
    @[deprecated CategoryTheory.Over.pullback]

    Alias of CategoryTheory.Over.pullback.


    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
    Instances For
      @[deprecated CategoryTheory.Over.pullback]

      Alias of CategoryTheory.Over.pullback.


      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
      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 (𝟙 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
              @[simp]
              theorem CategoryTheory.Over.star_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.Limits.HasBinaryProducts C] (X : C) :
              ((CategoryTheory.Over.star X✝).obj X).hom = CategoryTheory.Limits.prod.fst

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

              Equations
              Instances For

                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 ⨯ -.

                  Equations
                  • =
                  @[deprecated CategoryTheory.Over.star]

                  Alias of CategoryTheory.Over.star.


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

                  Equations
                  Instances For
                    @[deprecated CategoryTheory.Over.forgetAdjStar]

                    Alias of CategoryTheory.Over.forgetAdjStar.


                    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

                      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

                        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

                          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