Theorems · Theorem · category theory

CategoryTheory.Enriched.Functor.whiskerRight_app_apply

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L M N : CategoryTheory.Functor C D)
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M) ⟶ K.functorHom M) {X : C}
  (a :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L) (L.functorHom M)) (M.functorHom N)).obj
      X),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.app X)
          ((M.homObjFunctor N).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))))
      a =
    ((CategoryTheory.ConcreteCategory.hom (f.app X)) a.1, a.2)

Defined in

Mathlib.CategoryTheory.Functor.FunctorHom

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category