whiskerRight

Mathlib.CategoryTheory.Enriched.EnrichedCat

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

Lean4

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

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

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

Разделы

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

Аффилиация

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