Theorems · Definition · category theory

AddCommGrpCat.Colimits.colimitCoconeIsColimit

{J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : DecidableEq J] →
        [inst_2 : Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F)] →
          CategoryTheory.Limits.IsColimit (AddCommGrpCat.Colimits.colimitCocone F)

(internal implementation) The fact that the candidate colimit cocone constructed in colimitCocone is the colimit.

Defined in: Mathlib.Algebra.Category.Grp.Colimits
Cited by: 1 results in Mathlib
Foundations: Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category DecidableEq Small

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorstatement and proof · cited by 16,252
CategoryTheory.Limits.IsColimitstatement · cited by 773
AddCommGrpCatstatement and proof · cited by 462
Smallstatement and proof · cited by 369
AddCommGrpCat.Colimits.Quotstatement and proof · cited by 16
AddCommGrpCat.Colimits.colimitCoconestatement and proof · cited by 4
AddCommGrpCat.Colimits.isColimit_of_bijective_descproof · cited by 1

Cited by1

Results whose statement or proof uses this declaration.

AddCommGrpCat.hasColimit_of_small_quotproof · cited by 1