Theorems · Theorem · category theory

CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D)
  [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] (X : C),
  (CategoryTheory.ConcreteCategory.hom
        (((CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan F).inv.app X).app (Opposite.op (F.obj X))))
      ((CategoryTheory.ConcreteCategory.hom
          ((F.op.lanUnit.app (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X)).app (Opposite.op X)))
        { down := CategoryTheory.CategoryStruct.id X }) =
    { down := CategoryTheory.CategoryStruct.id (F.obj X) }

Defined in

Mathlib.CategoryTheory.Limits.Presheaf

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.HasLeftKanExtension