pi'

Mathlib.CategoryTheory.Pi.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.pi'

Lean4

/-- Assemble an `I`-indexed family of natural transformations into a single natural transformation.
-/
@[simps]
def pi' {E : Type*} [Category E] {F G : E ⥤ ∀ i, C i} (τ : ∀ i, F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i) : F ⟶ G
    where
  app := fun X i => (τ i).app X
  naturality _ _
    f := by
    ext i
    exact (τ i).naturality f

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

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

Разделы

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

Аффилиация

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