rightDualIso

Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Lean4

/-- Right duals are isomorphic. -/
def rightDualIso {X Y₁ Y₂ : C} (p₁ : ExactPairing X Y₁) (p₂ : ExactPairing X Y₂) : Y₁ ≅ Y₂
    where
  hom := @rightAdjointMate C _ _ X X ⟨Y₂⟩ ⟨Y₁⟩ (𝟙 X)
  inv := @rightAdjointMate C _ _ X X ⟨Y₁⟩ ⟨Y₂⟩ (𝟙 X)
  hom_inv_id := by
    -- Make all arguments explicit, because we want to find them by unification not synthesis.

    rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]
    rfl
  inv_hom_id := by
    rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]
    rfl

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

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

Разделы

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

Аффилиация

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