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
    theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃ {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) [IsIso φ.τ₁] [IsIso φ.τ₃] :
    theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ S₂) (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) :
    IsIso φ.τ₁IsIso φ.τ₃IsIso φ.τ₂

    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