comp

Mathlib.CategoryTheory.Adjunction.Basic

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

Lean4

/-- Composition of adjunctions. -/
@[simps! -isSimp unit counit, stacks 0DV0]
def comp : F ⋙ H ⊣ I ⋙ G :=
  mk' {
      homEquiv := fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
      unit :=
        adj₁.unit ≫
          whiskerRight (F.rightUnitor.inv ≫ whiskerLeft F adj₂.unit ≫ (associator _ _ _).inv) G ≫ (associator _ _ _).hom
      counit :=
        (associator _ _ _).inv ≫
          whiskerRight ((associator _ _ _).hom ≫ whiskerLeft _ adj₁.counit ≫ I.rightUnitor.hom) _ ≫ adj₂.counit }

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

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

Разделы

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

Аффилиация

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