Theorems · Definition · category theory

CategoryTheory.Limits.getBinaryBiproductData

{C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) → [CategoryTheory.Limits.HasBinaryBiproduct P Q] → CategoryTheory.Limits.BinaryBiproductData P Q

Use the axiom of choice to extract explicit BinaryBiproductData F from HasBinaryBiproduct F.

Defined in: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Cited by: 5 results in Mathlib
Foundations: Depth 4 from the axioms · uses Classical.choice
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroMorphisms CategoryTheory.Limits.HasBinaryBiproduct

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
CategoryTheory.Limits.HasBinaryBiproductstatement and proof · cited by 251
CategoryTheory.Limits.BinaryBiproductDatastatement · cited by 8
CategoryTheory.Limits.HasBinaryBiproduct.exists_binary_biproductproof · cited by 0

Cited by10

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.BinaryBiproduct.biconeproof · cited by 68
CategoryTheory.Limits.biprod.opIsoproof · cited by 16
CategoryTheory.Limits.BinaryBiproduct.isLimitproof · cited by 14
CategoryTheory.Limits.BinaryBiproduct.isBilimitproof · cited by 13
CategoryTheory.Limits.BinaryBiproduct.isColimitproof · cited by 8
CategoryTheory.Limits.biprod.opIso_hom_sndproof · cited by 3
CategoryTheory.Limits.biprod.opIso_hom_fstproof · cited by 3
CategoryTheory.Limits.biprod.inl_opIso_invproof · cited by 1
CategoryTheory.Limits.biprod.inr_opIso_invproof · cited by 1
CategoryTheory.Limits.hasBinaryBiproduct_of_isoproof · cited by 0