Theorems · Definition · category theory

CategoryTheory.Functor.LeibnizAdjunction.adj

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) →
                (F ⊣₂ G) →
                  (X₁ : CategoryTheory.Arrow C₁) →
                    [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] →
                      [inst_4 : CategoryTheory.Limits.HasPushouts C₃] →
                        F.leibnizPushout.obj X₁ ⊣ G.leibnizPullback.obj (Opposite.op X₁)

Given a parametrized adjunction F ⊣₂ G and an arrow X₁ : Arrow C₁, this is the induced adjunction F.leibnizPushout.obj X₁ ⊣ G.leibnizPullback.obj (op X₁).

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Cited by

5 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasPushouts