Theorems · Definition · category theory

ModuleCat.HasColimit.coconePointSMul

{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))] →
            R →+*
              CategoryTheory.End
                (CategoryTheory.Limits.colimit (F.comp (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)))

The induced scalar multiplication on colimit (F ⋙ forget₂ _ AddCommGrpCat).

Defined in

Mathlib.Algebra.Category.ModuleCat.Colimits

Cited by

3 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.CategoryCategoryTheory.Limits.HasColimit