Theorems · Theorem · category theory

MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {x y y' : (j : J) × ↑(F.obj j)},
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) y y' →
    MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x y'

Multiplication in the colimit is well-defined in the right argument.

Defined in

Mathlib.Algebra.Category.MonCat.FilteredColimits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered