lIso

Mathlib.CategoryTheory.Bicategory.Adjunction.Adj

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

Lean4

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

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

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

Разделы

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

Аффилиация

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