Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.isPointwiseLeftKanExtensionConvolutionExtensionUnit

{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} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {inst_5 : CategoryTheory.MonoidalCategoryStruct D} →
                  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    (d d' : D) →
                      (CategoryTheory.Functor.LeftExtension.mk
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj d d'))
                          (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit
                            C V d d')).IsPointwiseLeftKanExtension

convolutionUnitUnit exhibits ι.obj (d ⊗ d') as a left Ken extension of ι.obj d ⊠ ι.obj d' along tensor C.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct