symmEquivFunctor

Mathlib.CategoryTheory.Equivalence.Symmetry

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.symmEquivFunctor

Lean4

/-- The forward functor of the equivalence `(C ≌ D) ≌ (D ≌ C)ᵒᵖ`. -/
@[simps]
def symmEquivFunctor : (C ≌ D) ⥤ (D ≌ C)ᵒᵖ where
  obj e := Opposite.op e.symm
  map {e f} α := (mkHom <| conjugateEquiv f.toAdjunction e.toAdjunction <| asNatTrans α).op
  map_comp _ _ := Quiver.Hom.unop_inj (by cat_disch)

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

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

Разделы

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

Аффилиация

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