Documentation

Mathlib.CategoryTheory.Abelian.Exact

Exact sequences in abelian categories #

In an abelian category, we get several interesting results related to exactness which are not true in more general settings.

Main results #

In an abelian category, a short complex S is exact iff imageSubobject S.f = kernelSubobject S.g.

If (f, g) is exact, then Abelian.image.ι S.f is a kernel of S.g.

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

    If (f, g) is exact, then Abelian.coimage.π g is a cokernel of f.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[deprecated CategoryTheory.ShortComplex.Exact.map]
      theorem CategoryTheory.Functor.CategoryTheory.Functor.map_exact {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.Exact) (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
      (S.map F).Exact

      Alias of CategoryTheory.ShortComplex.Exact.map.

      theorem CategoryTheory.Functor.preservesMonomorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : CategoryTheory.ShortComplex A), S.Exact(S.map L).Exact) :
      L.PreservesMonomorphisms

      A functor which preserves exactness preserves monomorphisms.

      theorem CategoryTheory.Functor.preservesEpimorphisms_of_map_exact {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : CategoryTheory.ShortComplex A), S.Exact(S.map L).Exact) :
      L.PreservesEpimorphisms

      A functor which preserves exactness preserves epimorphisms.

      def CategoryTheory.Functor.preservesHomologyOfMapExact {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Abelian A] [CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B) [L.PreservesZeroMorphisms] (hL : ∀ (S : CategoryTheory.ShortComplex A), S.Exact(S.map L).Exact) :
      L.PreservesHomology

      A functor which preserves the exactness of short complexes preserves homology.

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

        A functor preserving zero morphisms, monos, and cokernels preserves homology.

        Equations
        • L.preservesHomologyOfPreservesMonosAndCokernels = L.preservesHomologyOfMapExact
        Instances For

          A functor preserving zero morphisms, epis, and kernels preserves homology.

          Equations
          • L.preservesHomologyOfPreservesEpisAndKernels = L.preservesHomologyOfMapExact
          Instances For