piConst

Mathlib.CategoryTheory.Limits.Shapes.Products

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.piConst

Lean4

/-- The functor sending `(X, n)` to the product of copies of `X` indexed by `n`. -/
@[simps]
def piConst [Limits.HasProducts.{w} C] : C ⥤ Type wᵒᵖ ⥤ C
    where
  obj X := { obj n := ∏ᶜ fun _ : (unop n) ↦ X, map f := Limits.Pi.map' f.unop fun _ ↦ 𝟙 _ }
  map f := { app n := Limits.Pi.map fun _ ↦ f }

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

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

Разделы

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

Аффилиация

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