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 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 short complex that is part of an exact sequence L₁.X₁ ⟶ P ⟶ L₀.X₃ ⟶ 0.

              Equations
              Instances For

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

                Equations
                Instances For
                  @[inline, reducible]

                  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.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 : CategoryTheory.ShortComplex.SnakeInput.Hom S₁ 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 : CategoryTheory.ShortComplex.SnakeInput.Hom S₁ 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
                        @[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 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₃_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 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₁.τ₃

                                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₁'_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₂'_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₃.τ₃

                                      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