Documentation

Mathlib.Algebra.Homology.ShortComplex.ShortExact

Short exact short complexes #

A short complex S : ShortComplex C is short exact (S.ShortExact) when it is exact, S.f is a mono and S.g is an epi.

A short complex S is short exact if it is exact, S.f is a mono and S.g is an epi.

Instances For

    If S is a short exact short complex in a balanced category, then S.X₁ is the kernel of S.g.

    Equations
    Instances For

      If S is a short exact short complex in a balanced category, then S.X₃ is the cokernel of S.f.

      Equations
      Instances For

        A split short complex is short exact.

        A choice of splitting for a short exact short complex S in a balanced category such that S.X₁ is injective.

        Equations
        Instances For

          A choice of splitting for a short exact short complex S in a balanced category such that S.X₃ is projective.

          Equations
          Instances For