Theorems · Theorem · category theory

CategoryTheory.Presheaf.uliftYonedaAdjunction_unit_app_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₂))) {Z : Cᵒᵖ} (z : P.obj Z),
  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Presheaf.uliftYonedaAdjunction L α).unit.app P).app Z)) z =
    {
      down :=
        CategoryTheory.CategoryStruct.comp (α.app (Opposite.unop Z)) (L.map (CategoryTheory.uliftYonedaEquiv.symm z)) }

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

0 results in Mathlib

Foundations

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

Assumes

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