Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutions

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

With the data of chosen isomorphic objects to given day convolutions, and provably equal unit maps through these isomorphisms, we can transform a given family of Day convolutions to one with convolutions definitionally equals to the given objects, and component of units definitionally equal to the provided map family.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore