Theorems · Definition · category theory
AddCommGrpCat.binaryProductLimitCone
(G H : AddCommGrpCat) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
Construct limit data for a binary product in AddCommGrpCat, using
AddCommGrpCat.of (G × H).
- Defined in
- Mathlib.Algebra.Category.Grp.Biproducts
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Discretestatement · cited by 2,447
- CategoryTheory.Limits.WalkingPairstatement · cited by 1,319
- CategoryTheory.Limits.pairstatement · cited by 536
- AddCommGrpCatstatement and proof · cited by 462
- AddCommGrpCat.carrierproof · cited by 407
- CategoryTheory.Limits.BinaryFan.mkproof · cited by 112
- AddCommGrpCat.ofHomproof · cited by 72
- AddCommGrpCat.Hom.homproof · cited by 72
- AddMonoidHom.sndproof · cited by 42
- AddMonoidHom.fstproof · cited by 39
- CategoryTheory.Limits.LimitConestatement · cited by 25
Cited by8
Results whose statement or proof uses this declaration.
- AddCommGrpCat.biprodIsoProdproof · cited by 10
- AddCommGrpCat.cartesianMonoidalCategoryproof · cited by 2
- AddCommGrpCat.biprodIsoProd_inv_comp_fstproof · cited by 1
- AddCommGrpCat.biprodIsoProd_inv_comp_sndproof · cited by 1
- AddCommGrpCat.binaryProductLimitCone_cone_ptstatement and proof · cited by 0
- AddCommGrpCat.binaryProductLimitCone_cone_π_app_leftstatement · cited by 0
- AddCommGrpCat.binaryProductLimitCone_cone_π_app_rightstatement · cited by 0
- AddCommGrpCat.binaryProductLimitCone_isLimit_liftstatement and proof · cited by 0