Theorems · Definition · category theory
CategoryTheory.Idempotents.Karoubi.Biproducts.bicone
{C : Type u_1} →
[inst : CategoryTheory.Category.{v, u_1} C] →
[inst_1 : CategoryTheory.Preadditive C] →
[CategoryTheory.Limits.HasFiniteBiproducts C] →
{J : Type} → [Finite J] → (F : J → CategoryTheory.Idempotents.Karoubi C) → CategoryTheory.Limits.Bicone FThe Bicone used in order to obtain the existence of
the biproduct of a functor J ⥤ Karoubi C when the category C is additive.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 43 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.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.CategoryStruct.compproof · cited by 17,999
- CategoryTheory.Preadditivestatement and proof · cited by 3,309
- Finitestatement and proof · cited by 3,029
- CategoryTheory.Idempotents.Karoubistatement and proof · cited by 233
- CategoryTheory.Limits.biproductproof · cited by 188
- CategoryTheory.Idempotents.Karoubi.Xproof · cited by 163
- CategoryTheory.Limits.HasFiniteBiproductsstatement and proof · cited by 106
- CategoryTheory.Idempotents.Karoubi.pproof · cited by 94
- CategoryTheory.Limits.biproduct.ιproof · cited by 86
- CategoryTheory.Limits.Biconestatement · cited by 75
- CategoryTheory.Limits.Bicone.πproof · cited by 40
Cited by4
Results whose statement or proof uses this declaration.
- CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_Xstatement and proof · cited by 0
- CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_pstatement and proof · cited by 0
- CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_ι_fstatement and proof · cited by 0
- CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_π_fstatement and proof · cited by 0