Short exact sequences

Contents

• Definitions
  • ShortShortExact sequences
  • Remark on monics, epis, kernels, and cokernels
  • LeftShortExact sequences
  • RightShortExact sequences
  • ShortExact sequences
• Opposite category and (short/left/right)exacts
• A criteria for ShortShortExact
  • Cokernel from ShortShortExact
  • isCoequalizer to ShortShortExact
• Correspondence between ShortExact and ShortShortExact
  • ShortExact from ShortShortExact
  • ShortShortExact criteria

Introduction

Short exact sequences consist of three objects and two morphisms such that the first morphism is a monic, the second morphism is an epi, and an image of the first morphism gives a kernel of the second morphism. These sequences are classically denoted by a diagram 0 -> A -> B -> C -> 0 We call such diagrams ShortExact. To define short exact sequences we first define short short exact sequences, ShortShortExact, left short exact sequences, LeftShortExact, and right short exact sequences, RightShortExact. These correspond to the diagrams A -> B -> C, 0 -> A -> B -> C, and, A -> B -> C -> 0, respectively. The definition of ShortShortExact says that the image of A -> B is the kernel of B -> C. This is equivalent to saying that the coimage of B -> C is the cokernel of A -> B. We prove this correspondence in the Section shortshortexact_coequalizer. Next, in the section shortexact_correspondence we prove a correspondence between ShortShortExact and ShortExact by using the factorization formula for morphisms in abelian precategories. We construct ShortExact from ShortShortExact and we give a criteria to construct ShortShortExact from properties similar to ShortExact.

Definition of short exact sequences

Image of the first morphism and equality of morphisms associated to it.

Coimage of the second morphism and equality of morphisms associated to it.

Transform isExact to isExact' and isExact' to isExact

Short Short Exact

ShortShortData such that the image of the first morphism is the kernel of the second morphism. Informally, an exact sequence A -> B -> C

Accessor functions

Remark

In Abelian.v we have already shown that a morphism is a monic if and only if its kernel is zero, and dually is an epi if and only if its cokernel is zero. See the results

• Abelian_MonicKernelZero_isEqualizer, Abelian_MonicKernelZero
• Abelian_EpiCokernelZero_isCoequalizer, Abelian_EpiCokernelZero
• Abelian_KernelZeroisMonic, Abelian_KernelZeroMonic
• Abelian_CokernelZeroisEpi, Abelian_CokernelZeroEpi

in CategoryTheory/Abelian.v. Thus, to define short exact sequeces, it suffices to assume that the first morphism is a monic and the second morphism is an epi. Similarly for left short exact and right short exact.

LeftShortExact

ShortShortExact such that the first morphism is a monic. Informally, an exact sequence 0 -> A -> B -> C

Accessor functions

RightShortExact

ShortShortExact such that the second morphism is an epi. Informally, an exact sequece A -> B -> C -> 0

Accessor functions

ShortExact

ShortShortExact such that the first morphism is monic and the second morphism is an epi. Informally, an exact sequece 0 -> A -> B -> C -> 0

LeftShortExact and RightShortExact from ShortExact

ShortShortExact criteria

In this section we show that for ShortShortExact a coimage of the second morphism is a cokernel of the first morphism and give a way to construct ShortShortExact from certain isCokernel.

ShortShortExact implies isCoequalizer.

Note that in the definition of ShortShortExact we use isEqualizer to say that an image of the first morphism is a kernel of the second morphism. We show that also the coimage of the second morphism is a cokernel of the first morphism. Informally, this follows directly from the fact that the opposite category of an abelian category is an abelian category and that taking the opposite category twice, we get the same category.

From isCokernel to ShortShortExact

We show that we can construct ShortShortExact from the isCokernel property proved above.

Correspondence of shortexact in A an A^op

LeftShortExact and RightShortExact from a ShortShortExact with extra properties

Correspondence between ShortShortExact and ShortExact

In this section we prove correspondence between ShortShortExact and ShortExact.

Construction of ShortExact from ShortShortExact

By using the factorization property of morphisms in abelian categories, we show that we can construct a ShortExact from ShortShortExact in a canonical way. More precisely, such ShortExact is given by taking the first morphism to be the image of the first morphism of the ShortShortExact and the second morphism to be the coimage of the second morphism of the ShortShortExact.

ShortShortExact from data of ShortExact

We construct a ShortShortExact from data corresponding to ShortExact. For a more precise statement, see the comment above ShortShortExact_from_isShortExact.

To see how the assumptions correspond to ShortExact note that every kernel is a monic and every cokernel is an epi. Also, the assumption H says that an image of f is the kernel of a coimage of g. In abelian categories every monic is the kernel of its cokernel, and thus one can show that in isE the kernelarrow can be "replaced" by the kernelarrow of the image of the kernelarrow. Thus the assumptions are similar to assumptions of ShortExact.

ShortShortExact from isKernel and isCokernel

Introduction

In this section we construct ShortShortExact from a pair of morphisms where the first morphism is the kernel of the second morphisms and where the second morphism is the cokernel of the first morphism.

LeftShortExact (resp. RightShortExact) construction for derived functors

Introduction

Let f : A --> B and g : A --> C be morphisms. In this section we construct a right short exact sequence of the form A --(f · i_1 - g · i_2)--> B ⊕ C --> W --> 0 where B ⊕ C --> W is the coequalizer of f · i_1 and g · i_2. Similarly for left short exact sequences and equalizers.

LeftShortExact containing an equalizer

RightShortExact containing a coequalizer