Theorems · Definition · category theory

CategoryTheory.Functor.corepresentableByCompCoyonedaObjOfIsColimit

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor D C} →
          {J : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
              {R : CategoryTheory.Functor J F.PartialLeftAdjointSource} →
                {c : CategoryTheory.Limits.Cocone (R.comp F.leftAdjointObjIsDefined.ι)} →
                  CategoryTheory.Limits.IsColimit c →
                    {c' : CategoryTheory.Limits.Cocone (R.comp F.partialLeftAdjoint)} →
                      CategoryTheory.Limits.IsColimit c' →
                        (F.comp (CategoryTheory.coyoneda.obj (Opposite.op c.pt))).CorepresentableBy c'.pt

Auxiliary definition for leftAdjointObjIsDefined_of_isColimit.

Defined in

Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category