# Documentation

Mathlib.Algebra.Homology.ShortComplex.Ab

# Homology and exactness of short complexes of abelian groups #

In this file, the homology of a short complex S of abelian groups is identified with the quotient of AddMonoidHom.ker S.g by the image of the morphism S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g induced by S.f.

The definitions are made in the ShortComplex namespace so as to enable dot notation. The names contain the prefix ab in order to allow similar constructions for other categories like ModuleCat.

## Main definitions #

• ShortComplex.abHomologyIso identifies the homology of a short complex of abelian groups to an explicit quotient.
• ShortComplex.ab_exact_iff expresses that a short complex of abelian groups S is exact iff any element in the kernel of S.g belongs to the image of S.f.
@[simp]
theorem CategoryTheory.ShortComplex.ab_zero_apply (x : S.X₁) :
S.g (S.f x) = 0
@[simp]
theorem CategoryTheory.ShortComplex.abToCycles_apply_coe (x : S.X₁) :
= S.f x

The canonical additive morphism S.X₁ →+ AddMonoidHom.ker S.g induced by S.f.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]

The explicit left homology data of a short complex of abelian group that is given by a kernel and a quotient given by the AddMonoidHom API.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a short complex S of abelian groups, this is the isomorphism between the abstract S.cycles of the homology API and the more concrete description as AddMonoidHom.ker S.g.

Equations
Instances For

Given a short complex S of abelian groups, this is the isomorphism between the abstract S.homology of the homology API and the more explicit quotient of AddMonoidHom.ker S.g by the image of S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g.

Equations
Instances For
theorem CategoryTheory.ShortComplex.ab_exact_iff :
∀ (x₂ : S.X₂), S.g x₂ = 0∃ (x₁ : S.X₁), S.f x₁ = x₂