Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution

(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} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  (d d' : D) →
                    (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj
                        (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj
                          C V d d') ≅
                      CategoryTheory.MonoidalCategory.DayConvolution.convolution
                        ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                              D).obj
                          d)
                        ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                              D).obj
                          d')

Isomorphisms that exhibits the essential image of ι as closed under day convolution.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore