Exact functors preserve admissible base change

A conflation-exact additive functor preserves pushout squares whose specified map is an inflation, and dually pullback squares whose specified map is a deflation. The pushout statement follows by expressing an admissible pushout as a distinguished kernel--cokernel pair on a biproduct. Additive functors preserve this biproduct, and the image conflation supplies the cokernel universal property of the image square. The pullback statement follows by duality.

These results let constructions made by Quillen's base-change axioms pass through exact functors without assuming preservation of arbitrary finite limits or colimits.

See Theo Bühler, Exact categories, Section 5, for the exact-functor calculus.

theorem TauCeti.ExactStructure.IsConflationExact.map_isPushout {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (hf : E.IsInflation f) (hsq : CategoryTheory.IsPushout f g h i) : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

A conflation-exact functor preserves a pushout square of an inflation. The square may be formed along an arbitrary morphism; no preservation of arbitrary pushouts is assumed.

theorem TauCeti.ExactStructure.IsConflationExact.map_isPullback {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (hh : E.IsDeflation h) (hsq : CategoryTheory.IsPullback f g h i) : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

A conflation-exact functor preserves a pullback square of a deflation. The square may be formed along an arbitrary morphism; no preservation of arbitrary pullbacks is assumed.