Bicartesian squares in exact categories

A pushout of an inflation in an exact category is also a pullback. Dually, a pullback of a deflation is also a pushout. Thus the base-change squares supplied by Quillen's E2 and E2op axioms are bicartesian.

The proof uses the standard biproduct criterion for a commutative square. For a square

W --f--> X
|        |
g        h
v        v
Y --i--> Z,

Mathlib identifies the pushout property with Z being the cokernel in the sequence

W --(f,-g)--> X ⊞ Y --(h,i)--> Z.

When f is an inflation, (f,-g) is an inflation as well: it factors as the split graph inclusion (1,-g) followed by f ⊞ 1. Its distinguished cokernel is uniquely isomorphic to the pushout cokernel, so the displayed sequence is a conflation. Its kernel property is exactly the pullback property. The statement for deflations follows by passing to the opposite exact category.

Main results

• TauCeti.ExactStructure.conflation_shortComplex_of_isPushout_of_isInflation packages a pushout of an inflation as its associated conflation.
• TauCeti.ExactStructure.isPullback_of_isPushout_of_isInflation proves that such a pushout is also a pullback.
• TauCeti.ExactStructure.isPushout_of_isPullback_of_isDeflation is the dual statement.
• TauCeti.ExactStructure.bicartesianSq_of_isPushout_of_isInflation and TauCeti.ExactStructure.bicartesianSq_of_isPullback_of_isDeflation bundle the conclusions as CategoryTheory.BicartesianSq.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, https://arxiv.org/abs/0811.1480, Proposition 2.12.

theorem TauCeti.ExactStructure.conflation_shortComplex_of_isPushout_of_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {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) : E.Conflation ⋯.shortComplex

The biproduct short complex associated to a pushout square of an inflation is a conflation.

Its maps are (f,-g) : W ⟶ X ⊞ Y and (h,i) : X ⊞ Y ⟶ Z. This is the kernel--cokernel sequence underlying the bicartesian-square criterion.

theorem TauCeti.ExactStructure.isPullback_of_isPushout_of_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {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.IsPullback f g h i

A pushout square of an inflation in an exact category is a pullback square.

theorem TauCeti.ExactStructure.bicartesianSq_of_isPushout_of_isInflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {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.BicartesianSq f g h i

A pushout square of an inflation, bundled as a bicartesian square.

theorem TauCeti.ExactStructure.isPushout_of_isPullback_of_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {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.IsPushout f g h i

A pullback square of a deflation in an exact category is a pushout square.

theorem TauCeti.ExactStructure.bicartesianSq_of_isPullback_of_isDeflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {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.BicartesianSq f g h i

A pullback square of a deflation, bundled as a bicartesian square.