Theorems · Theorem · category theory

AddCommGrpCat.isColimit_iff_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],
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Bijective ⇑(AddCommGrpCat.Colimits.Quot.desc F 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.LargeColimits

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryDecidableEq