Theorems · Definition · category theory

SemiRingCat.FilteredColimits.R

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    CategoryTheory.Functor J SemiRingCat → [CategoryTheory.IsFiltered J] → MonCat

The colimit of F ⋙ forget₂ SemiRingCat MonCat in the category MonCat. In the following, we will show that this has the structure of a semiring.

Defined in

Mathlib.Algebra.Category.Ring.FilteredColimits

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered