The exact sequence attached to a pushout square

Consider a pushout square in an abelian category:

X₁ ⟶ X₂
|    |
v    v
X₃ ⟶ X₄

We study the associated exact sequence X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0.

theorem CategoryTheory.IsPushout.exact_shortComplex {C : Type u} [Category.{v, u} C] [Abelian C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h : IsPushout t l r b) : ⋯.shortComplex.Exact

theorem CategoryTheory.IsPushout.hom_eq_add_up_to_refinements {C : Type u} [Category.{v, u} C] [Abelian C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h : IsPushout t l r b) {T : C} (x₄ : T ⟶ X₄) : ∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), CategoryStruct.comp π x₄ = CategoryStruct.comp x₂ r + CategoryStruct.comp x₃ b

Given a pushout square in an abelian category

X₁ ⟶ X₂
|    |
v    v
X₃ ⟶ X₄

the morphism X₂ ⊞ X₃ ⟶ X₄ is an epimorphism. This lemma translates this as the existence of liftings up to refinements: a morphism z : T ⟶ X₄ can be written as a sum of a morphism to X₂ and a morphism to X₃, at least if we allow a precomposition with an epimorphism π : T' ⟶ T.

theorem CategoryTheory.IsPushout.mono_of_isPullback_of_mono {C : Type u} [Category.{v, u} C] [Abelian C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h₁ : IsPushout t l r b) {X₅ : C} {r' : X₂ ⟶ X₅} {b' : X₃ ⟶ X₅} (h₂ : IsPullback t l r' b') (k : X₄ ⟶ X₅) (fac₁ : CategoryStruct.comp r k = r') (fac₂ : CategoryStruct.comp b k = b') [Mono r'] : Mono k

Given a commutative diagram in an abelian category

X₁ ⟶ X₂
|    |  \
v    v   \
X₃ ⟶ X₄   \
 \     \   v
  \     \> X₅
   \_____>

where the top/left square is a pushout square, the outer square involving X₁, X₂, X₃ and X₅ is a pullback square, and X₂ ⟶ X₅ is mono, then X₄ ⟶ X₅ is a mono.

theorem CategoryTheory.IsPullback.exact_shortComplex' {C : Type u} [Category.{v, u} C] [Abelian C] {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} (h : IsPullback t l r b) : ⋯.shortComplex'.Exact

Note: if h : IsPullback t l r b, then X₁ ⟶ X₂ ⊞ X₃ is a monomorphism, which can be translated in concrete terms thanks to the lemma IsPullback.hom_ext: if a morphism f : Z ⟶ X₁ becomes zero after composing with X₁ ⟶ X₂ and X₁ ⟶ X₃, then f = 0. This is the reason why we do not state the dual statement to IsPushout.hom_eq_add_up_to_refinements.