Theorems · Definition · category theory

HomologicalComplex.HomologySequence.mapSnakeInput

{C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            (S₁ ⟶ S₂) →
              (hS₁ : S₁.ShortExact) →
                (hS₂ : S₂.ShortExact) →
                  (i j : ι) →
                    (hij : c.Rel i j) →
                      HomologicalComplex.HomologySequence.snakeInput hS₁ i j hij ⟶
                        HomologicalComplex.HomologySequence.snakeInput hS₂ i j hij

The morphism snakeInput hS₁ i j hij ⟶ snakeInput hS₂ i j hij induced by a morphism φ : S₁ ⟶ S₂ of short complexes of homological complexes, that are short exact (hS₁ : S₁.ShortExact and hS₂ : S₁.ShortExact).

Defined in

Mathlib.Algebra.Homology.HomologySequenceLemmas

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian