pi

Mathlib.CategoryTheory.Pi.Basic

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

Lean4

/-- Assemble an `I`-indexed family of equivalences of categories
into a single equivalence. -/
@[simps]
def pi (E : ∀ i, C i ≌ D i) : (∀ i, C i) ≌ (∀ i, D i)
    where
  functor := Functor.pi (fun i => (E i).functor)
  inverse := Functor.pi (fun i => (E i).inverse)
  unitIso := NatIso.pi (fun i => (E i).unitIso)
  counitIso := NatIso.pi (fun i => (E i).counitIso)

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

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

Разделы

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

Аффилиация

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