Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (U : CategoryTheory.Functor C V) →
              [CategoryTheory.MonoidalCategory.DayConvolutionUnit U] →
                (F : CategoryTheory.Functor C V) →
                  [∀ (v : V) (d : C),
                        CategoryTheory.Limits.PreservesColimitsOfShape
                          (CategoryTheory.CostructuredArrow
                            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
                          (CategoryTheory.MonoidalCategory.tensorLeft v)] →
                    [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] →
                      (((CategoryTheory.Functor.whiskeringLeft (C × C) C V).obj
                                (CategoryTheory.MonoidalCategory.tensor C)).comp
                            (((CategoryTheory.Functor.whiskeringLeft (C × CategoryTheory.Discrete PUnit.{1}) (C × C)
                                      V).obj
                                  ((CategoryTheory.Functor.id C).prod
                                    (CategoryTheory.Functor.fromPUnit
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))).comp
                              (CategoryTheory.coyoneda.obj
                                (Opposite.op
                                  (CategoryTheory.MonoidalCategory.externalProduct F
                                    (CategoryTheory.Functor.fromPUnit
                                      (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))))))).CorepresentableBy
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution F U)

A CorepresentableBy structure that characterizes maps out of F ⊛ U by leveraging the fact that F ⊠ U is a left Kan extension of F ⊠ (fromPUnit 𝟙_ V).

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategory.DayConvolutionUnitCategoryTheory.Limits.PreservesColimitsOfShapeCategoryTheory.MonoidalCategory.DayConvolution