English
Similarly, the IsPushout structure yields an exact short complex in an Abelian setting.
Русский
Аналогично, структура IsPushout задаёт точную короткую последовательность в абелевой среде.
LaTeX
$$$\\\\text{IsPushout}(t,l,r,b) \\\\Rightarrow \\\\text{ShortComplex}'(t,l,r,b) \\\\text{ is exact }.$$$
Lean4
/-- 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 hom_eq_add_up_to_refinements (h : IsPushout t l r b) {T : C} (x₄ : T ⟶ X₄) :
∃ (T' : C) (π : T' ⟶ T) (_ : Epi π) (x₂ : T' ⟶ X₂) (x₃ : T' ⟶ X₃), π ≫ x₄ = x₂ ≫ r + x₃ ≫ b :=
by
have := h.epi_shortComplex_g
obtain ⟨T', π, _, u, hu⟩ := surjective_up_to_refinements_of_epi h.shortComplex.g x₄
refine ⟨T', π, inferInstance, u ≫ biprod.fst, u ≫ biprod.snd, ?_⟩
simp only [hu, assoc, ← Preadditive.comp_add]
congr
cat_disch
