whiskerRight

Mathlib.CategoryTheory.Monoidal.Center

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Center.whiskerRight

Lean4

/-- Auxiliary definition for the `MonoidalCategory` instance on `Center C`. -/
def whiskerRight {X₁ X₂ : Center C} (f : X₁ ⟶ X₂) (Y : Center C) : tensorObj X₁ Y ⟶ tensorObj X₂ Y
    where
  f := f.f ▷ Y.1
  comm U := whiskerRight_comm f Y U

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

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

Разделы

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

Аффилиация

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