colimitCocone

Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.colimitCocone

Lean4

/-- The (colimit) cocone for `F : J ⥤ PresheafOfModules.{v} R` that is constructed from
the colimit of `F ⋙ evaluation R X` for all `X`. -/
@[simps]
noncomputable def colimitCocone : Cocone F
    where
  pt := colimitPresheafOfModules F
  ι :=
    { app := fun j ↦
        { app := fun X ↦ colimit.ι (F ⋙ evaluation R X) j
          naturality := fun {X Y} f ↦ by
            dsimp
            erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitIso_inv]
            rfl }
      naturality := fun {X Y} f ↦ by
        ext1 X
        simpa using colimit.w (F ⋙ evaluation R X) f }

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

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

Разделы

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

Аффилиация

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