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.ShortExact.map {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.ShortExact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [CategoryTheory.Mono (F.map S.f)] [CategoryTheory.Epi (F.map S.g)] :
    (S.map F).ShortExact

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

    Equations
    • hS.fIsKernel = .fIsKernel
    Instances For

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

      Equations
      • hS.gIsCokernel = .gIsCokernel
      Instances For

        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