Theorems · Definition · category theory

MonCat.FilteredColimits.colimitDesc

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

Given a cocone t of F, the induced monoid homomorphism from the colimit to the cocone point. As a function, this is simply given by the induced map of the corresponding cocone in Type. The only thing left to see is that it is a monoid homomorphism.

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered