whiskerRight

Mathlib.CategoryTheory.Adjunction.Whiskering

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

Lean4

/-- Given an adjunction `F ⊣ G`, this provides the natural adjunction
  `(whiskeringRight C _ _).obj F ⊣ (whiskeringRight C _ _).obj G`. -/
@[simps! unit_app_app counit_app_app]
protected def whiskerRight (adj : F ⊣ G) : (whiskeringRight C D E).obj F ⊣ (whiskeringRight C E D).obj G
    where
  unit :=
    { app := fun X => (rightUnitor _).inv ≫ whiskerLeft X adj.unit ≫ (associator _ _ _).inv
      naturality := by intros; ext; simp }
  counit :=
    { app := fun X => (associator _ _ _).hom ≫ whiskerLeft X adj.counit ≫ (rightUnitor _).hom
      naturality := by intros; ext; simp }

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

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

Разделы

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

Аффилиация

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