colimitCocone — Mathlib

English

The cocone constructed from the colimit of F ⋙ forget₂ (ModuleCat R) AddCommGrpCat is an actual colimit for F, i.e., it satisfies the universal property.

Русский

Кокон, построенный из колимита F ⋙ forget₂ (ModuleCat R) AddCommGrpCat, является колимитом для F, то есть удовлетворяет всепроникающему свойству.

LaTeX

$$$$ \text{IsColimit}(\text{colimitCocone}(F)) $$$$

Lean4

/-- The cocone for `F` constructed from the colimit of
`(F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)`. -/
@[simps]
noncomputable def colimitCocone : Cocone F
    where
  pt := mkOfSMul (coconePointSMul F)
  ι :=
    { app := fun j =>
        homMk (colimit.ι (F ⋙ forget₂ _ AddCommGrpCat) j)
          (fun r =>
            by
            dsimp
              -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

            erw [mkOfSMul_smul]
            simp)
      naturality := fun i j f => by
        apply (forget₂ _ AddCommGrpCat).map_injective
        simp only [Functor.map_comp, forget₂_map_homMk]
        dsimp
        erw [colimit.w (F ⋙ forget₂ _ AddCommGrpCat), comp_id] }

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