leftDualIso

Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Lean4

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

    rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]
    rfl
  inv_hom_id := by
    rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]
    rfl

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

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

Разделы

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

Аффилиация

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