Theorems · Definition · category theory

HomologicalComplex.HomologySequence.snakeInput

{C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            S.ShortExact → (i j : ι) → c.Rel i j → CategoryTheory.ShortComplex.SnakeInput C

Given a short exact short complex S : HomologicalComplex C c, and degrees i and j such that c.Rel i j, this is the snake diagram whose four lines are respectively obtained by applying the functors homologyFunctor C c i, opcyclesFunctor C c i, cyclesFunctor C c j, homologyFunctor C c j to S. Applying the snake lemma to this gives the homology sequence of S.

Defined in

Mathlib.Algebra.Homology.HomologySequence

Cited by

27 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian