Documentation

Mathlib.Algebra.Homology.ShortComplex.Exact

Exact short complexes #

When S : ShortComplex C, this file defines a structure S.Exact which expresses the exactness of S, i.e. there exists a homology data h : S.HomologyData such that h.left.H is zero. When [S.HasHomology], it is equivalent to the assertion IsZero S.homology.

Almost by construction, this notion of exactness is self dual, see Exact.op and Exact.unop.

The assertion that the short complex S : ShortComplex C is exact.

Instances For