Theorems · Theorem · category theory

CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans_app_uliftYoneda_obj

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}
  {G :
    CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂)))
      (CategoryTheory.Functor Dᵒᵖ (Type (max w v₁ v₂)))}
  (φ : F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ⟶ CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp G)
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (X : C),
  (CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.natTrans φ).app
      (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).inv.app X)
      (φ.app X)

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.HasLeftKanExtension