Theorems · Theorem · category theory

AddCommGrpCat.Colimits.Quot.desc_colimitCocone

∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [inst_1 : DecidableEq J]
  (F : CategoryTheory.Functor J AddCommGrpCat) [inst_2 : Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F)],
  AddCommGrpCat.Colimits.Quot.desc F (AddCommGrpCat.Colimits.colimitCocone F) = Shrink.addEquiv.symm.toAddMonoidHom

Defined in: Mathlib.Algebra.Category.Grp.Colimits
Cited by: 0 results in Mathlib
Foundations: Depth 84 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.

Cites17

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.Functor.objproof · cited by 19,642
CategoryTheory.Functorstatement and proof · cited by 16,252
AddMonoidHomstatement · cited by 3,230
CategoryTheory.Limits.Cocone.ptstatement · cited by 1,354
AddEquiv.symmstatement · cited by 530
AddCommGrpCatstatement and proof · cited by 462
AddCommGrpCat.carrierstatement and proof · cited by 407
Smallstatement and proof · cited by 369
Shrinkstatement · cited by 132
AddEquiv.toAddMonoidHomstatement · cited by 101
AddCommGrpCat.Colimits.Quotstatement and proof · cited by 16

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.