instCategoryStructHom

Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.Adj.instCategoryStructHom

Lean4

@[simps!]
instance : CategoryStruct (a ⟶ b) where
  Hom α β := Hom₂ α β
  id
    α :=
    { τl := 𝟙 _
      τr := 𝟙 _ }
  comp {a b c} x
    y :=
    { τl := x.τl ≫ y.τl
      τr := y.τr ≫ x.τr
      conjugateEquiv_τl := by simp [← conjugateEquiv_comp c.adj b.adj a.adj y.τl x.τl, Hom₂.conjugateEquiv_τl] }

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

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

Разделы

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

Аффилиация

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