Gluing a pullback of a deflation with a pushout of an inflation

In a commutative diagram

A --f--> B --g--> C
|a       |b       |c
A' -f'-> B' -g'-> C'

whose left square is a pullback along a deflation f' and whose right square is a pushout along an inflation g, both squares are bicartesian, so the outer rectangle is a pullback. Its biproduct short complex A ⟶ C ⊞ A' ⟶ C' is a conflation: it is a kernel by the pullback property, and its deflation (c, -(f' ≫ g')) is the composite of (𝟙, -f') with the deflation (c, g') of the pushout square (Bühler, Corollary 3.6). This is the step that makes the mapping cone of a map of acyclic complexes acyclic.

Main results

• TauCeti.ExactStructure.conflation_shortComplex'_of_isPullback_of_isPushout: gluing a pullback along a deflation with a pushout along an inflation.

References

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

theorem TauCeti.ExactStructure.conflation_shortComplex'_of_isPullback_of_isPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {A B C' A' B' C'' : C} {f : A ⟶ B} {g : B ⟶ C'} {a : A ⟶ A'} {b : B ⟶ B'} {c : C' ⟶ C''} {f' : A' ⟶ B'} {g' : B' ⟶ C''} (hl : CategoryTheory.IsPullback f a b f') (hr : CategoryTheory.IsPushout g b c g') (hf' : E.IsDeflation f') (hg : E.IsInflation g) : E.Conflation ⋯.shortComplex'

Gluing a pullback with a pushout (Bühler, Corollary 3.6). In a commutative diagram

A --f--> B --g--> C
|a       |b       |c
A' -f'-> B' -g'-> C'

whose left square is a pullback, with f' a deflation, and whose right square is a pushout, with g an inflation, the outer rectangle is a pullback and the short complex A ⟶ C ⊞ A' ⟶ C', with maps (f ≫ g, a) and (c, -(f' ≫ g')), is a conflation.