Reflecting exact binary-biproduct complexes

This file packages the bookkeeping needed to move an explicit exact complex through a faithful additive inclusion. The inclusion need not preserve the chosen binary biproduct definitionally: its canonical mapBiprod isomorphism identifies the mapped complex with the explicit target complex.

noncomputable def MagnitudeConjecture.CategoryTheory.binaryBiproductShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {X A B Y : C} (fA : X ⟶ A) (fB : X ⟶ B) (gA : A ⟶ Y) (gB : B ⟶ Y) (hzero : CategoryTheory.CategoryStruct.comp fA gA + CategoryTheory.CategoryStruct.comp fB gB = 0) : CategoryTheory.ShortComplex C

A three-term complex whose middle object is a binary biproduct.

theorem MagnitudeConjecture.CategoryTheory.binaryBiproductShortComplex_exact_of_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Faithful] {X A B Y : C} [CategoryTheory.Limits.PreservesBinaryBiproduct A B F] (fA : X ⟶ A) (fB : X ⟶ B) (gA : A ⟶ Y) (gB : B ⟶ Y) (hzero : CategoryTheory.CategoryStruct.comp fA gA + CategoryTheory.CategoryStruct.comp fB gB = 0) (hmap : (binaryBiproductShortComplex (F.map fA) (F.map fB) (F.map gA) (F.map gB) ⋯).Exact) : (binaryBiproductShortComplex fA fB gA gB hzero).Exact

Exactness of an explicit mapped binary-biproduct complex reflects through a faithful additive functor, even though the functor's image of the chosen biproduct is only canonically isomorphic to the target biproduct.