derivedη

Mathlib.CategoryTheory.Functor.Derived.Adjunction

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

Lean4

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

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

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

Разделы

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

Аффилиация

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