derivedε

Mathlib.CategoryTheory.Functor.Derived.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.derivedε

Lean4

/-- The counit of the derived adjunction, see `Adjunction.derived`. -/
noncomputable def derivedε : F' ⋙ G' ⟶ 𝟭 D₂ :=
  (F' ⋙ G').rightDerivedDesc (whiskerRight β G' ≫ (Functor.associator _ _ _).hom) W₂ _
    ((Functor.associator _ _ _).hom ≫
      whiskerLeft F α ≫
        (Functor.associator _ _ _).inv ≫ whiskerRight adj.counit _ ≫ L₂.leftUnitor.hom ≫ L₂.rightUnitor.inv)

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

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

Разделы

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

Аффилиация

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