Theorems · Theorem · category theory

CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app

∀ {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) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (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] (x : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
        CategoryTheory.MonoidalCategory.DayConvolutionUnit.can)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit F U).app
          (x, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).hom.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).hom
      (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).inv)

Characterizing the forward direction of rightUnitor via the universal maps.

Defined in

Mathlib.CategoryTheory.Monoidal.DayConvolution

Cited by

4 results in Mathlib

Foundations

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

Assumes

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