Theorems · Definition · category theory

CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {A : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} A] →
        [inst_2 : CategoryTheory.MonoidalCategory A] →
          [inst_3 : CategoryTheory.MonoidalClosed A] →
            (M : A) →
              (F G : CategoryTheory.Functor Cᵒᵖ A) →
                [inst_4 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] →
                  (X : C) →
                    ((CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom A F G).comp
                            (CategoryTheory.coyoneda.obj (Opposite.op M))).obj
                        (Opposite.op X) ≃
                      (CategoryTheory.presheafHom
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj F
                              ((CategoryTheory.Functor.const Cᵒᵖ).obj M))
                            G).obj
                        (Opposite.op X)

Relation between functorEnrichedHom and presheafHom.

Defined in

Mathlib.CategoryTheory.Sites.Monoidal

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalClosedCategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom