Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolution.convolution_hom_ext_at

∀ {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]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] (c : C) {v : V}
  {f g : (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj c ⟶ v},
  (∀ {x y : C} (u : CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟶ c),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map u)
            f) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map u)
            g)) →
    f = g

Use the fact that (F ⊛ G).obj c is a colimit to characterize morphisms out of it at a point.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategoryCategoryTheory.MonoidalCategory.DayConvolution