isColimitColimitCocone — Mathlib

English

For a diagram F: J ⥤ ModuleCat R, there exists a colimit object in ModuleCat R and a canonical cocone exhibiting it.

Русский

Для диаграммы F: J ⥤ ModuleCat R существует колимитный объект и каноничный кокон, демонстрирующий его.

LaTeX

$$$$ \exists \text{ colimit object for } F \quad\text{and a cocone } colimitCocone(F). $$$$

Lean4

/-- The cocone for `F` constructed from the colimit of
`(F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)` is a colimit cocone. -/
noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F)
    where
  desc
    s :=
    homMk (colimit.desc _ ((forget₂ _ AddCommGrpCat).mapCocone s))
      (fun r => by
        apply colimit.hom_ext
        intro j
        dsimp
        rw [colimit.ι_desc_assoc]
          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

        erw [mkOfSMul_smul]
        dsimp
        simp only [ι_colimMap_assoc, Functor.comp_obj, forget₂_obj, colimit.ι_desc, Functor.mapCocone_pt,
          Functor.mapCocone_ι_app, forget₂_map]
        exact smul_naturality (s.ι.app j) r)
  fac s
    j := by
    apply (forget₂ _ AddCommGrpCat).map_injective
    exact colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j
  uniq s m
    hm := by
    apply (forget₂ _ AddCommGrpCat).map_injective
    apply colimit.hom_ext
    intro j
    erw [colimit.ι_desc ((forget₂ _ AddCommGrpCat).mapCocone s) j]
    dsimp
    rw [← hm]
    rfl

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