whiskeringRight

Mathlib.CategoryTheory.Limits.ExactFunctor

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

Lean4

/-- Whiskering an exact functor by an exact functor yields an 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 _ _, by dsimp; exact comp_preservesFiniteColimits _ _⟩)
  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