Theorems · Definition · category theory

CategoryTheory.Presheaf.uliftYonedaAdjunction

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        {A : CategoryTheory.Functor C ℰ} →
          [CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A] →
            (L : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) ℰ) →
              (α : A ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp L) →
                [L.IsLeftKanExtension α] → L ⊣ CategoryTheory.Presheaf.restrictedULiftYoneda A

If L : (Cᵒᵖ ⥤ Type max w v₁ v₂) ⥤ ℰ is a pointwise left Kan extension of a functor A : C ⥤ ℰ along the Yoneda embedding, then L is a left adjoint of restrictedULiftYoneda A : ℰ ⥤ Cᵒᵖ ⥤ Type max w v₁ v₂

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.HasPointwiseLeftKanExtensionCategoryTheory.Functor.IsLeftKanExtension