Theorems · Definition · category theory

ModuleCat.FilteredColimits.colimitDesc

{R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) →
            (t : CategoryTheory.Limits.Cocone F) → ModuleCat.FilteredColimits.colimit F ⟶ t.pt

Given a cocone t of F, the induced monoid linear map from the colimit to the cocone point. We already know that this is a morphism between additive groups. The only thing left to see is that it is a linear map, i.e. preserves scalar multiplication.

Defined in

Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Cited by

2 results in Mathlib

Foundations

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

Assumes

RingCategoryTheory.SmallCategoryCategoryTheory.IsFiltered