whiskerHom

Mathlib.CategoryTheory.Bicategory.Extension

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Bicategory.LeftExtension.whiskerHom

Lean4

/-- Construct a morphism between whiskered extensions. -/
@[simps! right]
def whiskerHom (i : s ⟶ t) {x : B} (h : c ⟶ x) : s.whisker h ⟶ t.whisker h :=
  StructuredArrow.homMk (i.right ▷ h) <| by
    rw [← cancel_mono (α_ _ _ _).inv]
    calc
      _ = (unit s ≫ f ◁ i.right) ▷ h := by simp [-LeftExtension.w]
      _ = unit t ▷ h := (congrArg (· ▷ h) (LeftExtension.w i))
      _ = _ := by simp

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

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

Разделы

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

Аффилиация

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