Theorems · Definition · category theory

AddCommGrpCat.Colimits.Quot.desc

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      (c : CategoryTheory.Limits.Cocone F) → [inst_1 : DecidableEq J] → AddCommGrpCat.Colimits.Quot F →+ ↑c.pt

(implementation detail) Part of the universal property of the colimit cocone, but without assuming that Quot F lives in the correct universe.

Defined in

Mathlib.Algebra.Category.Grp.Colimits

Cited by

7 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryDecidableEq