Projective dimension of a finite biproduct

A finite biproduct has projective dimension below a fixed bound when every summand does. This small generic lemma is shared by the weak-positivity and Iyama-realization arguments.

theorem MagnitudeConjecture.CategoryTheory.hasProjectiveDimensionLT_biproduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] [CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type u_1} [Fintype J] (F : J → C) (d : ℕ) (hF : ∀ (j : J), CategoryTheory.HasProjectiveDimensionLT (F j) d) : CategoryTheory.HasProjectiveDimensionLT (⨁ F) d

A finite biproduct has projective dimension below d if every summand does.