whisker

Mathlib.CategoryTheory.Bicategory.Extension

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

Lean4

/-- Whisker a 1-morphism to an extension.
```
  b
  △ \
  |   \ extension  △
f |     \          | unit
  |       ◿
  a - - - ▷ c - - - ▷ x
      g         h
```
-/
def whisker (t : LeftExtension f g) {x : B} (h : c ⟶ x) : LeftExtension f (g ≫ h) :=
  .mk _ <| t.unit ▷ h ≫ (α_ _ _ _).hom

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

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

Разделы

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

Аффилиация

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