Theorems · Definition · category theory

CategoryTheory.Mat_.equivalenceSelfOfHasFiniteBiproducts

(C : Type (u₁ + 1)) →
  [inst : CategoryTheory.LargeCategory C] →
    [inst_1 : CategoryTheory.Preadditive C] → [CategoryTheory.Limits.HasFiniteBiproducts C] → CategoryTheory.Mat_ C ≌ C

A preadditive category that already has finite biproducts is equivalent to its additive envelope. Note that we only prove this for a large category; otherwise there are universe issues that I haven't attempted to sort out.

Defined in

Mathlib.CategoryTheory.Preadditive.Mat

Cited by

2 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.LargeCategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasFiniteBiproducts