mkOfUnitCounit

Mathlib.CategoryTheory.Adjunction.Basic

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

Lean4

/-- Construct an adjunction between functors `F` and `G` given a unit and counit for the adjunction
satisfying the triangle identities. -/
@[simps!]
def mkOfUnitCounit (adj : CoreUnitCounit F G) : F ⊣ G
    where
  unit := adj.unit
  counit := adj.counit
  left_triangle_components
    X := by
    have := adj.left_triangle
    rw [NatTrans.ext_iff, funext_iff] at this
    simpa [-CoreUnitCounit.left_triangle] using this X
  right_triangle_components
    Y := by
    have := adj.right_triangle
    rw [NatTrans.ext_iff, funext_iff] at this
    simpa [-CoreUnitCounit.right_triangle] using this Y

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

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

Разделы

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

Аффилиация

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