Theorems · Theorem · category theory

CategoryTheory.Mat_.isoBiproductEmbedding_inv

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C),
  M.isoBiproductEmbedding.inv =
    CategoryTheory.Limits.biproduct.desc fun i x k => if h : i = k then CategoryTheory.eqToHom ⋯ else 0

Defined in

Mathlib.CategoryTheory.Preadditive.Mat

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive