Theorems · Theorem · category theory

AddGrpCat.FilteredColimits.colimit_add_mk_eq

∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  AddGrpCat.FilteredColimits.G.mk F x + AddGrpCat.FilteredColimits.G.mk F y =
    AddGrpCat.FilteredColimits.G.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩

Defined in

Mathlib.Algebra.Category.Grp.FilteredColimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.IsFiltered