Documentation

Mathlib.Algebra.Homology.ExactSequence

Exact sequences #

A sequence of n composable arrows S : ComposableArrows C (i.e. a functor S : Fin (n + 1) ⥤ C) is said to be exact (S.Exact) if the composition of two consecutive arrows are zero (S.IsComplex) and the diagram is exact at each i for 1 ≤ i < n.

Together with the inductive construction of composable arrows ComposableArrows.precomp, this is useful in order to state that certain finite sequences of morphisms are exact (e.g the snake lemma), even though in the applications it would usually be more convenient to use individual lemmas expressing the exactness at a particular object.

This implementation is a refactor of exact_seq with appeared in the Liquid Tensor Experiement as a property of lists in Arrow C.

source
@[simp]
theorem CategoryTheory.ShortComplex.toComposableArrows_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) :
∀ {X Y : Fin (1 + 1 + 1)} (g : X ⟶ Y), (CategoryTheory.ShortComplex.toComposableArrows S).toPrefunctor.map g = CategoryTheory.ComposableArrows.Precomp.map (CategoryTheory.ComposableArrows.mk₁ S.g) S.f X Y (_ : X ≤ Y)
source
@[simp]
theorem CategoryTheory.ShortComplex.toComposableArrows_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) :
∀ (a : Fin (1 + 1 + 1)), (CategoryTheory.ShortComplex.toComposableArrows S).toPrefunctor.obj a = CategoryTheory.ComposableArrows.Precomp.obj (CategoryTheory.ComposableArrows.mk₁ S.g) S.X₁ a
source
def CategoryTheory.ShortComplex.toComposableArrows {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) :
CategoryTheory.ComposableArrows C 2

The composable arrows associated to a short complex.

Equations
Instances For
    source
    structure CategoryTheory.ComposableArrows.IsComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} (S : CategoryTheory.ComposableArrows C n) :
    Prop

    F : ComposableArrows C n is a complex if all compositions of two consecutive arrows are zero.

    Instances For
      source
      theorem CategoryTheory.ComposableArrows.IsComplex.zero_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (self : CategoryTheory.ComposableArrows.IsComplex S) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) {Z : C} (h : S.toPrefunctor.obj { val := i + 2, isLt := (_ : i + 2 < n + 1) } ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S i (i + 1)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S (i + 1) (i + 2)) h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      theorem CategoryTheory.ComposableArrows.IsComplex.zero'_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (hS : CategoryTheory.ComposableArrows.IsComplex S) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) {Z : C} (h : S.toPrefunctor.obj { val := k, isLt := (_ : k < n + 1) } ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S j k) h) = CategoryTheory.CategoryStruct.comp 0 h
      source
      theorem CategoryTheory.ComposableArrows.IsComplex.zero' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (hS : CategoryTheory.ComposableArrows.IsComplex S) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S i j) (CategoryTheory.ComposableArrows.map' S j k) = 0
      source
      theorem CategoryTheory.ComposableArrows.isComplex_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) :
      CategoryTheory.ComposableArrows.IsComplex S₂
      source
      theorem CategoryTheory.ComposableArrows.isComplex_iff_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) :
      CategoryTheory.ComposableArrows.IsComplex S₁ ↔ CategoryTheory.ComposableArrows.IsComplex S₂
      source
      theorem CategoryTheory.ComposableArrows.isComplex₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 0) :
      CategoryTheory.ComposableArrows.IsComplex S
      source
      theorem CategoryTheory.ComposableArrows.isComplex₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 1) :
      CategoryTheory.ComposableArrows.IsComplex S
      source
      @[reducible]
      def CategoryTheory.ComposableArrows.sc' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} (S : CategoryTheory.ComposableArrows C n) (hS : CategoryTheory.ComposableArrows.IsComplex S) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
      CategoryTheory.ShortComplex C

      The short complex consisting of maps S.map' i j and S.map' j k when we know that S : ComposableArrows C n satisfies S.IsComplex.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[inline, reducible]
        abbrev CategoryTheory.ComposableArrows.sc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} (S : CategoryTheory.ComposableArrows C n) (hS : CategoryTheory.ComposableArrows.IsComplex S) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
        CategoryTheory.ShortComplex C

        The short complex consisting of maps S.map' i (i + 1) and S.map' (i + 1) (i + 2) when we know that S : ComposableArrows C n satisfies S.IsComplex.

        Equations
        Instances For
          source
          structure CategoryTheory.ComposableArrows.Exact {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} (S : CategoryTheory.ComposableArrows C n) extends CategoryTheory.ComposableArrows.IsComplex :
          Prop

          F : ComposableArrows C n is exact if it is a complex and that all short complexes consisting of two consecutive arrows are exact.

          Instances For
            source
            theorem CategoryTheory.ComposableArrows.Exact.exact' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C n} (hS : CategoryTheory.ComposableArrows.Exact S) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
            CategoryTheory.ShortComplex.Exact (CategoryTheory.ComposableArrows.sc' S (_ : CategoryTheory.ComposableArrows.IsComplex S) i j k)
            source
            @[simp]
            theorem CategoryTheory.ComposableArrows.sc'Map_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
            (CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k).τ₃ = φ.app { val := k, isLt := (_ : k < n + 1) }
            source
            @[simp]
            theorem CategoryTheory.ComposableArrows.sc'Map_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
            (CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k).τ₁ = φ.app { val := i, isLt := (_ : i < n + 1) }
            source
            @[simp]
            theorem CategoryTheory.ComposableArrows.sc'Map_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
            (CategoryTheory.ComposableArrows.sc'Map φ h₁ h₂ i j k).τ₂ = φ.app { val := j, isLt := (_ : j < n + 1) }
            source
            def CategoryTheory.ComposableArrows.sc'Map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
            CategoryTheory.ComposableArrows.sc' S₁ h₁ i j k ⟶ CategoryTheory.ComposableArrows.sc' S₂ h₂ i j k

            Functoriality maps for ComposableArrows.sc'.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.ComposableArrows.scMap_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
              (CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i).τ₂ = φ.app { val := i + 1, isLt := (_ : i + 1 < n + 1) }
              source
              @[simp]
              theorem CategoryTheory.ComposableArrows.scMap_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
              (CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i).τ₃ = φ.app { val := i + 2, isLt := (_ : i + 2 < n + 1) }
              source
              @[simp]
              theorem CategoryTheory.ComposableArrows.scMap_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
              (CategoryTheory.ComposableArrows.scMap φ h₁ h₂ i).τ₁ = φ.app { val := i, isLt := (_ : i < n + 1) }
              source
              def CategoryTheory.ComposableArrows.scMap {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (φ : S₁ ⟶ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
              CategoryTheory.ComposableArrows.sc S₁ h₁ i ⟶ CategoryTheory.ComposableArrows.sc S₂ h₂ i

              Functoriality maps for ComposableArrows.sc.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.ComposableArrows.sc'MapIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
                (CategoryTheory.ComposableArrows.sc'MapIso e h₁ h₂ i j k).hom = CategoryTheory.ComposableArrows.sc'Map e.hom h₁ h₂ i j k
                source
                @[simp]
                theorem CategoryTheory.ComposableArrows.sc'MapIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
                (CategoryTheory.ComposableArrows.sc'MapIso e h₁ h₂ i j k).inv = CategoryTheory.ComposableArrows.sc'Map e.inv h₂ h₁ i j k
                source
                def CategoryTheory.ComposableArrows.sc'MapIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (j : ℕ) (k : ℕ) (hij : autoParam (i + 1 = j) _auto✝) (hjk : autoParam (j + 1 = k) _auto✝) (hk : autoParam (k ≤ n) _auto✝) :
                CategoryTheory.ComposableArrows.sc' S₁ h₁ i j k ≅ CategoryTheory.ComposableArrows.sc' S₂ h₂ i j k

                The isomorphism S₁.sc' _ i j k ≅ S₂.sc' _ i j k induced by an isomorphism S₁ ≅ S₂ in ComposableArrows C n.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.ComposableArrows.scMapIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
                  (CategoryTheory.ComposableArrows.scMapIso e h₁ h₂ i).inv = CategoryTheory.ComposableArrows.scMap e.inv h₂ h₁ i
                  source
                  @[simp]
                  theorem CategoryTheory.ComposableArrows.scMapIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
                  (CategoryTheory.ComposableArrows.scMapIso e h₁ h₂ i).hom = CategoryTheory.ComposableArrows.scMap e.hom h₁ h₂ i
                  source
                  def CategoryTheory.ComposableArrows.scMapIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.IsComplex S₁) (h₂ : CategoryTheory.ComposableArrows.IsComplex S₂) (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝) :
                  CategoryTheory.ComposableArrows.sc S₁ h₁ i ≅ CategoryTheory.ComposableArrows.sc S₂ h₂ i

                  The isomorphism S₁.sc _ i ≅ S₂.sc _ i induced by an isomorphism S₁ ≅ S₂ in ComposableArrows C n.

                  Equations
                  Instances For
                    source
                    theorem CategoryTheory.ComposableArrows.exact_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : CategoryTheory.ComposableArrows.Exact S₁) :
                    CategoryTheory.ComposableArrows.Exact S₂
                    source
                    theorem CategoryTheory.ComposableArrows.exact_iff_of_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S₁ : CategoryTheory.ComposableArrows C n} {S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂) :
                    CategoryTheory.ComposableArrows.Exact S₁ ↔ CategoryTheory.ComposableArrows.Exact S₂
                    source
                    theorem CategoryTheory.ComposableArrows.exact₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 0) :
                    CategoryTheory.ComposableArrows.Exact S
                    source
                    theorem CategoryTheory.ComposableArrows.exact₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 1) :
                    CategoryTheory.ComposableArrows.Exact S
                    source
                    theorem CategoryTheory.ComposableArrows.isComplex₂_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 2) :
                    CategoryTheory.ComposableArrows.IsComplex S ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S 0 1) (CategoryTheory.ComposableArrows.map' S 1 2) = 0
                    source
                    theorem CategoryTheory.ComposableArrows.isComplex₂_mk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 2) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S 0 1) (CategoryTheory.ComposableArrows.map' S 1 2) = 0) :
                    CategoryTheory.ComposableArrows.IsComplex S
                    source
                    theorem CategoryTheory.ShortComplex.isComplex_toComposableArrows {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) :
                    CategoryTheory.ComposableArrows.IsComplex (CategoryTheory.ShortComplex.toComposableArrows S)
                    source
                    theorem CategoryTheory.ComposableArrows.exact₂_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 2) (hS : CategoryTheory.ComposableArrows.IsComplex S) :
                    CategoryTheory.ComposableArrows.Exact S ↔ CategoryTheory.ShortComplex.Exact (CategoryTheory.ComposableArrows.sc' S hS 0 1 2)
                    source
                    theorem CategoryTheory.ComposableArrows.exact₂_mk {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ComposableArrows C 2) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.map' S 0 1) (CategoryTheory.ComposableArrows.map' S 1 2) = 0) (h : CategoryTheory.ShortComplex.Exact (CategoryTheory.ShortComplex.mk (CategoryTheory.ComposableArrows.map' S 0 1) (CategoryTheory.ComposableArrows.map' S 1 2) w)) :
                    CategoryTheory.ComposableArrows.Exact S
                    source
                    theorem CategoryTheory.ShortComplex.Exact.exact_toComposableArrows {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (hS : CategoryTheory.ShortComplex.Exact S) :
                    CategoryTheory.ComposableArrows.Exact (CategoryTheory.ShortComplex.toComposableArrows S)
                    source
                    theorem CategoryTheory.ShortComplex.exact_iff_exact_toComposableArrows {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) :
                    CategoryTheory.ShortComplex.Exact S ↔ CategoryTheory.ComposableArrows.Exact (CategoryTheory.ShortComplex.toComposableArrows S)
                    source
                    theorem CategoryTheory.ComposableArrows.exact_iff_δ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} (S : CategoryTheory.ComposableArrows C (n + 2)) :
                    CategoryTheory.ComposableArrows.Exact S ↔ CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' S 0 1) (CategoryTheory.ComposableArrows.map' S 1 2)) ∧ CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.δ₀ S)
                    source
                    theorem CategoryTheory.ComposableArrows.exact_of_δ₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 2)} (h : CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' S 0 1) (CategoryTheory.ComposableArrows.map' S 1 2))) (h₀ : CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.δ₀ S)) :
                    CategoryTheory.ComposableArrows.Exact S

                    If S : ComposableArrows C (n + 2) is such that the first two arrows form an exact sequence and that the tail S.δ₀ is exact, then S is also exact. See ShortComplex.SnakeInput.snake_lemma in Algebra.Homology.ShortComplex.SnakeLemma for a use of this lemma.

                    source
                    theorem CategoryTheory.ComposableArrows.exact_iff_δlast {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {n : ℕ} (S : CategoryTheory.ComposableArrows C (n + 2)) :
                    CategoryTheory.ComposableArrows.Exact S ↔ CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.δlast S) ∧ CategoryTheory.ComposableArrows.Exact (CategoryTheory.ComposableArrows.mk₂ (CategoryTheory.ComposableArrows.map' S n (n + 1)) (CategoryTheory.ComposableArrows.map' S (n + 1) (n + 2)))