whiskerLeft

Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Oplax.OplaxTrans.whiskerLeft

Lean4

/-- Left whiskering of an oplax natural transformation and a modification. -/
@[simps]
def whiskerLeft (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) : η ≫ θ ⟶ η ≫ ι
    where
  app a := η.app a ◁ Γ.app a
  naturality {a b}
    f := by
    dsimp
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc]
    simp

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

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

Разделы

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

Аффилиация

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