compNatTrans

Mathlib.CategoryTheory.DinatTrans

URI: https://scilib.ai/kg/mathlib#CategoryTheory.DinatTrans.compNatTrans

Lean4

/-- Post-composition with a natural transformation. -/
@[simps]
def compNatTrans (δ : F ⤞ G) (α : G ⟶ H) : F ⤞ H
    where
  app X := δ.app X ≫ (α.app (op X)).app X
  dinaturality
    f := by
    rw [Category.assoc, Category.assoc, ← NatTrans.naturality_app, ← δ.dinaturality_assoc f, NatTrans.naturality]

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

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

Разделы

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

Аффилиация

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