postcompFunctor

Mathlib.CategoryTheory.Shift.SingleFunctors

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SingleFunctors.postcompFunctor

Lean4

/-- The functor `SingleFunctors C D A ⥤ SingleFunctors C E A` given by the postcomposition
by a functor `G : D ⥤ E` which commutes with the shift. -/
@[simps]
def postcompFunctor (G : D ⥤ E) [G.CommShift A] : SingleFunctors C D A ⥤ SingleFunctors C E A
    where
  obj F := F.postcomp G
  map {F₁ F₂}
    φ :=
    { hom := fun a => whiskerRight (φ.hom a) G
      comm := fun n a a' ha' => by
        ext X
        simpa using G.congr_map (congr_app (φ.comm n a a' ha') X) }

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

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

Разделы

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

Аффилиация

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