FiveLemma

Contents

• Definition of structures for five lemma
• Five Lemma structure to opposite category
• Five Lemma
• Five Lemma for short exact sequences, ShortExact

FiveLemma

Five lemma says that if you have the following commutative diagram in an abelian category C_1 --> C_2 --> C_3 --> C_4 --> C_5 f_1 | f_2 | f_3 | f_4 | f_5 | D_1 --> D_2 --> D_3 --> D_4 --> D_5 where the rows are exact and the morphisms f_1, f_2, f_4, and f_5 are isomorphisms, then f_3 is an isomorphism. Exactness of the first row means that an image of C_1 --> C_2 is a kernel of C_2 --> C_3, an image of C_2 --> C_3 is a kernel of C_3 --> C_4, and an image of C_3 --> C_4 is a kernel of C_4 --> C_5. The idea of the proof is to show that f_3 is monic and epi, and thus is an isomorphism by monic_epi_is_iso. To show that f_3 is monic, we use pseudo elements, PseudoElem. By PEq_isMonic it suffices to show that if a is a pseudo element of C_3 is mapped to PZero by f_3, then a is pseudo equal to PZero. We construct a pseudo element a' of C_1 which is mapped to a by the composite C_1 --> C_2 --> C_3. Since the first row is exact, this composite is Zero, and thus the pseudo image is PZero. We construct such a pseudo element a' as follows. First, by using exactness at C_3, and the fact that a is mapped to Pzero by C_3 --> C_4 (because of commutativity of f_3 f_4 square and the fact that f_4 is a monic), we obtain by PEq_isExact a pseudo element b' of C_2 which is mapped to a. The image of b' under f_2 · D_2 --> D_3 is PZero by commutativity and the assumption that a is mapped to PZero. By PEq_isExact we obtain aa pseudo element b'' of D_1 which is mapped to the image of b' under f_2. By the fact that f_1 is an epi, we get a pseudo element a' which is mapped to b''. Now, using commutativity of the square f_1 f_2, and the fact that f_2 is a monic, we get that the image of a' under C_1 --> C_2 is b'. Hence a' is mapped to a, under C_1 --> C_2 --> C_3, and the proof is complete. See FiveLemma_isMonic for formalization of the above. To show that f_3 is an epi we use opposite categories. First we transform the above diagram to the following diagram in the opposite category D_5 --> D_4 --> D_3 --> D_2 --> D_1 f_1 | f_2 | f_3 | f_4 | f_5 | C_5 --> D_2 --> D_3 --> D_4 --> C_5 Thus, we need to show that f_3 is monic (here f_3 is the opposite morphism of f_3 in the first diagram), to show that the original f_3 is epi! But this follows from the above proof. See FiveLemma_isEpi. Finally, in FiveLemma we put FiveLemma_isMonic and FiveLemma_isEpi together, and prove the lemma. Five lemma is sometimes used for short exact sequences in which case C_1, C_5, D_1, and D_5 are Zeros. Thus, f_1 and f_5 are automatically isomorphisms, and one only needs to show that f_2 and f_4 are isomorphisms. This is proved in ShortExactFiveLemma.

Introduction

In this section we define the data needed to state the five lemma. The main definitions are FiveRow and FiveRowMorphism. The first contains the data of a row in the five lemma, and the second contains the data for a morphism between two rows. FiveRow consists of Objects of the row, FiveRowObs, differentials of the row FiveRowDiffs, equations that composition of consecutive differentials is zero, FiveRowDiffsEq, and the fact that the row is exact, FiveRowExacts. FiveRowMorphism takes arguments two FiveRow and consists of morphisms between the objects in the rows, FiveRowMors, and commutativity of the squares, FiveRowMorsComm.

Rows

Objects for a row

Differentials for a row

Composition of consecutive differentials is 0

Row is exact

Define row for FiveLemma

Morphism of FiveRows

Morphisms in the morphism

Commutativity of the squares

Morphism of rows

Introduction

In this section we translate the definitions in the previous section five_lemma_data to opposite categories, so that FiveLemma_isEpi can use these.

Introduction

In this section we prove the five lemma following the sketch of a proof on top of this file.

Introduction

Five lemma for short exact sequences. Suppose you have a morphism of short exact sequences represented by the following diagram 0 --> C_1 --> C_2 --> C_3 --> 0 | f_2 | f_3 | f_4 | | 0 --> D_1 --> D_2 --> D_3 --> 0 If f_2 and f_4 are isomorphisms, then f_3 is an isomorphism. This is proved in ShortExactFiveLemma.

Construction of the first row

Construction of the second row

Construction of the morphism between rows

FiveLemma for short exact sequences