Theorems · Theorem · category theory

CategoryTheory.Presheaf.uliftYonedaAdjunction_homEquiv_app

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  {A : CategoryTheory.Functor C ℰ}
  [inst_2 : 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) [inst_3 : L.IsLeftKanExtension α]
  {P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} {Y : ℰ} (f : L.obj P ⟶ Y) {Z : Cᵒᵖ} (z : P.obj Z),
  (CategoryTheory.ConcreteCategory.hom ((((CategoryTheory.Presheaf.uliftYonedaAdjunction L α).homEquiv P Y) f).app Z))
      z =
    {
      down :=
        CategoryTheory.CategoryStruct.comp (α.app (Opposite.unop Z))
          (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.uliftYonedaEquiv.symm z)) f) }

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

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