whiskerVertical

Mathlib.CategoryTheory.GuitartExact.VerticalComposition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.TwoSquare.whiskerVertical

Lean4

/-- Given `w : TwoSquare T L R B`, one may obtain a 2-square `TwoSquare T L' R' B` if we
provide natural transformations `α : L ⟶ L'` and `β : R' ⟶ R`. -/
@[simps!]
def whiskerVertical (α : L ⟶ L') (β : R' ⟶ R) : TwoSquare T L' R' B :=
  (w.whiskerLeft α).whiskerRight β

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

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

Разделы

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

Аффилиация

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