rIso

Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.Adj.rIso

Lean4

/-- Given an isomorphism between two 1-morphisms in `Adj B`, this is the
underlying isomorphisms between the right adjoints. -/
@[simps]
def rIso {a b : Adj B} {adj₁ adj₂ : a ⟶ b} (e : adj₁ ≅ adj₂) : adj₁.r ≅ adj₂.r
    where
  hom := e.inv.τr
  inv := e.hom.τr
  hom_inv_id := by rw [← comp_τr, e.hom_inv_id, id_τr]
  inv_hom_id := by rw [← comp_τr, e.inv_hom_id, id_τr]

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

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

Разделы

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

Аффилиация

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