Theorems · Definition · category theory

AddCommGrpCat.Colimits.isColimit_of_bijective_desc

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      (c : CategoryTheory.Limits.Cocone F) →
        [inst_1 : DecidableEq J] →
          Function.Bijective ⇑(AddCommGrpCat.Colimits.Quot.desc F c) → CategoryTheory.Limits.IsColimit c

If c is a cocone of F such that Quot.desc F c is bijective, then c is a colimit cocone of F.

Defined in

Mathlib.Algebra.Category.Grp.Colimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryDecidableEq