whiskerLeft

Mathlib.CategoryTheory.Enriched.EnrichedCat

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

Lean4

/-- Whisker a `V`-enriched natural transformation on the left. -/
@[simps!]
def whiskerLeft (F : EnrichedFunctor V C D) {G H : EnrichedFunctor V D E} (α : G ⟶ H) : F.comp V G ⟶ F.comp V H :=
  ⟨(F.forgetComp G).hom ≫ F.forget.whiskerLeft α.out ≫ (F.forgetComp H).inv⟩

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

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

Разделы

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

Аффилиация

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