Theorems · Theorem · category theory

AddCommGrpCat.Colimits.Quot.desc_toCocone_desc

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  (c : CategoryTheory.Limits.Cocone F) [inst_1 : DecidableEq J] {A : Type w} [inst_2 : AddCommGroup A]
  (f : AddCommGrpCat.Colimits.Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c),
  (AddCommGrpCat.Hom.hom (hc.desc (AddCommGrpCat.Colimits.toCocone F f))).comp (AddCommGrpCat.Colimits.Quot.desc F c) =
    f

Defined in

Mathlib.Algebra.Category.Grp.Colimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryDecidableEqAddCommGroup