whiskeringRight

Mathlib.CategoryTheory.Limits.ExactFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.LeftExactFunctor.whiskeringRight

Lean4

/-- Whiskering a left exact functor by a left exact functor yields a left exact functor. -/
@[simps! obj_obj obj_map map_app_app]
def whiskeringRight : (D ⥤ₗ E) ⥤ (C ⥤ₗ D) ⥤ (C ⥤ₗ E)
    where
  obj
    F :=
    ObjectProperty.lift _ (forget _ _ ⋙ (Functor.whiskeringRight C D E).obj F.obj)
      (fun G => by dsimp; exact comp_preservesFiniteLimits _ _)
  map {F G}
    η :=
    { app := fun H => ((Functor.whiskeringRight C D E).map η).app H.obj
      naturality := fun _ _ f => ((Functor.whiskeringRight C D E).map η).naturality f }

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

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

Разделы

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

Аффилиация

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