associator

Mathlib.CategoryTheory.Enriched.EnrichedCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.EnrichedCat.associator

Lean4

/-- Composition of `V`-enriched functors is associative up to isomorphism. -/
@[simps!]
def associator (F : EnrichedFunctor V C D) (G : EnrichedFunctor V D E) (H : EnrichedFunctor V E E') :
    EnrichedFunctor.comp V (EnrichedFunctor.comp V F G) H ≅ EnrichedFunctor.comp V F (EnrichedFunctor.comp V G H) :=
  EnrichedFunctor.isoMk <|
    (F.comp V G).forgetComp H ≪≫
      Functor.isoWhiskerRight (F.forgetComp G) _ ≪≫
        Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ (G.forgetComp H).symm ≪≫ (F.forgetComp _).symm

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru