whiskerIso

Mathlib.CategoryTheory.Bicategory.Extension

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.LeftLift.whiskerIso

Lean4

/-- Construct an isomorphism between whiskered lifts. -/
def whiskerIso (i : s ≅ t) {x : B} (h : x ⟶ c) : s.whisker h ≅ t.whisker h :=
  Iso.mk (whiskerHom i.hom h) (whiskerHom i.inv h)
    (StructuredArrow.hom_ext _ _ <|
      calc
        _ = h ◁ (i.hom ≫ i.inv).right := by simp [-Iso.hom_inv_id]
        _ = 𝟙 _ := by simp [Iso.hom_inv_id])
    (StructuredArrow.hom_ext _ _ <|
      calc
        _ = h ◁ (i.inv ≫ i.hom).right := by simp [-Iso.inv_hom_id]
        _ = 𝟙 _ := by simp [Iso.inv_hom_id])

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

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

Разделы

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

Аффилиация

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