# Documentation

Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

# Exactness of short complexes in concrete abelian categories #

If an additive concrete category C has an additive forgetful functor to Ab which preserves homology, then a short complex S in C is exact if and only if it is so after applying the functor forget₂ C Ab.

@[simp]
theorem CategoryTheory.ShortComplex.zero_apply {C : Type u} (S : ) (x : (.obj S.X₁)) :
(.map S.g) ((.map S.f) x) = 0
theorem CategoryTheory.Preadditive.mono_iff_injective {C : Type u} {X : C} {Y : C} (f : X Y) :
Function.Injective (.map f)
theorem CategoryTheory.Preadditive.mono_iff_injective' {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Preadditive.epi_iff_injective {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.Preadditive.epi_iff_surjective' {C : Type u} {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.ShortComplex.exact_iff_of_concreteCategory {C : Type u} (S : ) :
∀ (x₂ : (.obj S.X₂)), (.map S.g) x₂ = 0∃ (x₁ : (.obj S.X₁)), (.map S.f) x₁ = x₂
theorem CategoryTheory.ShortComplex.SnakeInput.δ_apply {C : Type u} (x₃ : .obj D.L₀.X₃) (x₂ : .obj D.L₁.X₂) (x₁ : .obj D.L₂.X₁) (h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃) (h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂) :
= D.v₂₃.τ₁ x₁

This lemma allows the computation of the connecting homomorphism D.δ when D : SnakeInput C and C is a concrete category.