congrLeftFunctor

Mathlib.CategoryTheory.Equivalence.Symmetry

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

Lean4

/-- Promoting `Equivalence.congrLeft` to a functor. -/
@[simps!]
def congrLeftFunctor (E : Type*) [Category E] : (C ≌ D) ⥤ ((C ⥤ E) ≌ (D ⥤ E))ᵒᵖ :=
  Functor.rightOp
    { obj f := f.unop.congrLeft
      map {e f}
        α :=
        mkHom <|
          (whiskeringLeft _ _ _).map <|
            conjugateEquiv e.unop.toAdjunction f.unop.toAdjunction <| asNatTrans <| Quiver.Hom.unop α
      map_comp _
        _ := by
        ext
        simp [← map_comp] }

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

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

Разделы

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

Аффилиация

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