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.

Constructor for cycles of short complexes in a concrete category.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem CategoryTheory.ShortComplex.SnakeInput.δ_apply {C : Type u} [Category.{v, u} C] [HasForget C] [HasForget₂ C Ab] [Abelian C] [(forget₂ C Ab).Additive] [(forget₂ C Ab).PreservesHomology] (D : SnakeInput C) (x₃ : (forget C).obj D.L₀.X₃) (x₂ : (forget C).obj D.L₁.X₂) (x₁ : (forget C).obj D.L₂.X₁) (h₂ : D.L₁.g x₂ = D.v₀₁.τ₃ x₃) (h₁ : D.L₂.f x₁ = D.v₁₂.τ₂ x₂) :
    D.δ x₃ = D.v₂₃.τ₁ x₁

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

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