productLimitCone

Mathlib.CategoryTheory.Limits.Types.Shapes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Types.Small.productLimitCone

Lean4

/-- A variant of `productLimitCone` using a `Small` hypothesis rather than a function to `Type`.
-/
noncomputable def productLimitCone : Limits.LimitCone (Discrete.functor F)
    where
  cone :=
    { pt := Shrink (∀ j, F j)
      π := Discrete.natTrans (fun ⟨j⟩ f => (equivShrink (∀ j, F j)).symm f j) }
  isLimit :=
    have : Small.{u} (∀ j, F j) := inferInstance
    { lift := fun s x => (equivShrink _) (fun j => s.π.app ⟨j⟩ x)
      uniq := fun s m w => funext fun x => Shrink.ext <| funext fun j => by simpa using (congr_fun (w ⟨j⟩) x :) }

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

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

Разделы

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

Аффилиация

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