Theorems · Definition · category theory

ModuleCat.HasColimit.isColimitColimitCocone

{R : Type w} →
  [inst : Ring R] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : CategoryTheory.Limits.HasColimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat))] →
            CategoryTheory.Limits.IsColimit (ModuleCat.HasColimit.colimitCocone F)

The cocone for F constructed from the colimit of (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) is a colimit cocone.

Defined in

Mathlib.Algebra.Category.ModuleCat.Colimits

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingCategoryTheory.CategoryCategoryTheory.Limits.HasColimit