Documentation

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

The snake lemma #

The snake lemma is a standard tool in homological algebra. The basic situation is when we have a diagram as follows in an abelian category C, with exact rows:

L₁.X₁ ⟶ L₁.X₂ ⟶ L₁.X₃ ⟶ 0
  |       |       |
  |v₁₂.τ₁ |v₁₂.τ₂ |v₁₂.τ₃
  v       v       v

0 ⟶ L₂.X₁ ⟶ L₂.X₂ ⟶ L₂.X₃

We shall think of this diagram as the datum of a morphism v₁₂ : L₁L₂ in the category ShortComplex C such that both L₁ and L₂ are exact, and L₁.g is epi and L₂.f is a mono (which is equivalent to saying that L₁.X₃ is the cokernel of L₁.f and L₂.X₁ is the kernel of L₂.g). Then, we may introduce the kernels and cokernels of the vertical maps. In other words, we may introduce short complexes L₀ and L₃ that are respectively the kernel and the cokernel of v₁₂. All these data constitute a SnakeInput C.

Given such a S : SnakeInput C, we define a connecting homomorphism S.δ : L₀.X₃ ⟶ L₃.X₁ and show that it is part of an exact sequence L₀.X₁ ⟶ L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂ ⟶ L₃.X₃. Each of the four exactness statement is first stated separately as lemmas L₀_exact, L₁'_exact, L₂'_exact and L₃_exact and the full 6-term exact sequence is stated as snake_lemma. This sequence can even be extended with an extra 0 on the left (see mono_L₀_f) if L₁.X₁ ⟶ L₁.X₂ is a mono (i.e. L₁ is short exact), and similarly an extra 0 can be added on the right (epi_L₃_g) if L₂.X₂ ⟶ L₂.X₃ is an epi (i.e. L₂ is short exact).

These results were also obtained in the Liquid Tensor Experiment. The code and the proof here are slightly easier because of the use of the category ShortComplex C, the use of duality (which allows to construct only half of the sequence, and deducing the other half by arguing in the opposite category), and the use of "refinements" (see CategoryTheory.Abelian.Refinements) instead of a weak form of pseudo-elements.

A snake input in an abelian category C consists of morphisms of short complexes L₀L₁L₂L₃ (which should be visualized vertically) such that L₀ and L₃ are respectively the kernel and the cokernel of L₁L₂, L₁ and L₂ are exact, L₁.g is epi and L₂.f is mono.

Instances For

    The snake input in the opposite category that is deduced from a snake input.

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

      L₀.X₁ is the kernel of v₁₂.τ₁ : L₁.X₁ ⟶ L₂.X₁.

      Equations
      Instances For

        L₀.X₂ is the kernel of v₁₂.τ₂ : L₁.X₂ ⟶ L₂.X₂.

        Equations
        Instances For

          L₀.X₃ is the kernel of v₁₂.τ₃ : L₁.X₃ ⟶ L₂.X₃.

          Equations
          Instances For

            The upper part of the first column of the snake diagram is exact.

            The upper part of the second column of the snake diagram is exact.

            The upper part of the third column of the snake diagram is exact.

            L₃.X₁ is the cokernel of v₁₂.τ₁ : L₁.X₁ ⟶ L₂.X₁.

            Equations
            Instances For

              L₃.X₂ is the cokernel of v₁₂.τ₂ : L₁.X₂ ⟶ L₂.X₂.

              Equations
              Instances For

                L₃.X₃ is the cokernel of v₁₂.τ₃ : L₁.X₃ ⟶ L₂.X₃.

                Equations
                Instances For

                  The lower part of the first column of the snake diagram is exact.

                  The lower part of the second column of the snake diagram is exact.

                  The lower part of the third column of the snake diagram is exact.

                  The fiber product of L₁.X₂ and L₀.X₃ over L₁.X₃. This is an auxiliary object in the construction of the morphism δ : L₀.X₃ ⟶ L₃.X₁.

                  Equations
                  Instances For

                    The canonical map P ⟶ L₂.X₂.

                    Equations
                    Instances For

                      The canonical map P ⟶ L₂.X₁.

                      Equations
                      • S.φ₁ = .lift S.φ₂
                      Instances For

                        The short complex that is part of an exact sequence L₁.X₁ ⟶ P ⟶ L₀.X₃ ⟶ 0.

                        Equations
                        Instances For

                          The connecting homomorphism δ : L₀.X₃ ⟶ L₃.X₁.

                          Equations
                          Instances For

                            The pushout of L₂.X₂ and L₃.X₁ along L₂.X₁.

                            Equations
                            Instances For

                              The canonical morphism L₀.X₂ ⟶ P.

                              Equations
                              Instances For

                                The short complex L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁.

                                Equations
                                Instances For

                                  The short complex L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂.

                                  Equations
                                  Instances For

                                    Exactness of L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁.

                                    The duality isomorphism S.POpposite.unop S.op.P'.

                                    Equations
                                    Instances For

                                      The duality isomorphism S.P'Opposite.unop S.op.P.

                                      Equations
                                      Instances For

                                        The duality isomorphism S.L₂'.op ≅ S.op.L₁'.

                                        Equations
                                        Instances For

                                          Exactness of L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂.

                                          @[reducible, inline]

                                          The diagram S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃ for any S : SnakeInput C.

                                          Equations
                                          Instances For

                                            The diagram S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃ is exact for any S : SnakeInput C.

                                            theorem CategoryTheory.ShortComplex.SnakeInput.δ_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) {A : C} (x₃ : A S.L₀.X₃) (x₂ : A S.L₁.X₂) (x₁ : A S.L₂.X₁) (h₂ : CategoryTheory.CategoryStruct.comp x₂ S.L₁.g = CategoryTheory.CategoryStruct.comp x₃ S.v₀₁.τ₃) (h₁ : CategoryTheory.CategoryStruct.comp x₁ S.L₂.f = CategoryTheory.CategoryStruct.comp x₂ S.v₁₂.τ₂) :
                                            theorem CategoryTheory.ShortComplex.SnakeInput.Hom.ext_iff {C : Type u_1} :
                                            ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Abelian C} {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {x y : S₁.Hom S₂}, x = y x.f₀ = y.f₀ x.f₁ = y.f₁ x.f₂ = y.f₂ x.f₃ = y.f₃
                                            theorem CategoryTheory.ShortComplex.SnakeInput.Hom.ext {C : Type u_1} :
                                            ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Abelian C} {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} {x y : S₁.Hom S₂}, x.f₀ = y.f₀x.f₁ = y.f₁x.f₂ = y.f₂x.f₃ = y.f₃x = y

                                            A morphism of snake inputs involve four morphisms of short complexes which make the obvious diagram commute.

                                            Instances For

                                              The identity morphism of a snake input.

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

                                                The composition of morphisms of snake inputs.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.ShortComplex.SnakeInput.functorL₀_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                  ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₀.map f = f.f₀
                                                  @[simp]
                                                  theorem CategoryTheory.ShortComplex.SnakeInput.functorL₀_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                  CategoryTheory.ShortComplex.SnakeInput.functorL₀.obj S = S.L₀

                                                  The functor which sends S : SnakeInput C to its zeroth line S.L₀.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                    ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₁.map f = f.f₁
                                                    @[simp]
                                                    theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                    CategoryTheory.ShortComplex.SnakeInput.functorL₁.obj S = S.L₁

                                                    The functor which sends S : SnakeInput C to its zeroth line S.L₁.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                      ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₂.map f = f.f₂
                                                      @[simp]
                                                      theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                      CategoryTheory.ShortComplex.SnakeInput.functorL₂.obj S = S.L₂

                                                      The functor which sends S : SnakeInput C to its second line S.L₂.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                        CategoryTheory.ShortComplex.SnakeInput.functorL₃.obj S = S.L₃
                                                        @[simp]
                                                        theorem CategoryTheory.ShortComplex.SnakeInput.functorL₃_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                        ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorL₃.map f = f.f₃

                                                        The functor which sends S : SnakeInput C to its third line S.L₃.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[simp]
                                                          theorem CategoryTheory.ShortComplex.SnakeInput.functorP_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                          ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), CategoryTheory.ShortComplex.SnakeInput.functorP.map f = CategoryTheory.Limits.pullback.map X.L₁.g X.v₀₁.τ₃ Y.L₁.g Y.v₀₁.τ₃ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃
                                                          @[simp]

                                                          The functor which sends S : SnakeInput C to the auxiliary object S.P, which is pullback S.L₁.g S.v₀₁.τ₃.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                            ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₃ = f.f₃.τ₁
                                                            @[simp]
                                                            theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                            ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₂ = f.f₀.τ₃
                                                            @[simp]
                                                            theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                            CategoryTheory.ShortComplex.SnakeInput.functorL₁'.obj S = S.L₁'
                                                            @[simp]
                                                            theorem CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                            ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₁'.map f).τ₁ = f.f₀.τ₂

                                                            The functor which sends S : SnakeInput C to S.L₁' which is S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                              CategoryTheory.ShortComplex.SnakeInput.functorL₂'.obj S = S.L₂'
                                                              @[simp]
                                                              theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                              ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₁ = f.f₀.τ₃
                                                              @[simp]
                                                              theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                              ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₂ = f.f₃.τ₁
                                                              @[simp]
                                                              theorem CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                              ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), (CategoryTheory.ShortComplex.SnakeInput.functorL₂'.map f).τ₃ = f.f₃.τ₂

                                                              The functor which sends S : SnakeInput C to S.L₂' which is S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] :
                                                                ∀ {X Y : CategoryTheory.ShortComplex.SnakeInput C} (f : X Y), CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.map f = CategoryTheory.ComposableArrows.homMk₅ f.f₀.τ₁ f.f₀.τ₂ f.f₀.τ₃ f.f₃.τ₁ f.f₃.τ₂ f.f₃.τ₃
                                                                @[simp]
                                                                theorem CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex.SnakeInput C) :
                                                                CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor.obj S = S.composableArrows

                                                                The functor which maps S : SnakeInput C to the diagram S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃.

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