hasLeftDualOfEquivalence

Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.hasLeftDualOfEquivalence

Lean4

/-- Pull back a left dual along an equivalence. -/
def hasLeftDualOfEquivalence (X : C) [HasLeftDual (F.obj X)] : HasLeftDual X
    where
  leftDual := G.obj (ᘁ(F.obj X))
  exact :=
    by
    letI :=
      exactPairingCongrLeft (X := F.obj (G.obj ᘁ(F.obj X))) (X' := ᘁ(F.obj X)) (Y := F.obj X)
        (adj.toEquivalence.counitIso.app ᘁ(F.obj X))
    apply exactPairingOfFullyFaithful F

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

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

Разделы

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

Аффилиация

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