CategoryTheory.ComposableArrows.exact_of_δ₀
theorem CategoryTheory.ComposableArrows.exact_of_δ₀ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 2)},
(CategoryTheory.ComposableArrows.mk₂ (S.map' 0 1 ⋯ ⋯) (S.map' 1 2 ⋯ ⋯)).Exact → S.δ₀.Exact → S.Exact
The theorem `CategoryTheory.ComposableArrows.exact_of_δ₀` states that for any category `C` with zero morphisms and any functor `S` from the finite category `Fin (n + 2)` to `C` (which is represented as `CategoryTheory.ComposableArrows C (n + 2)`), if the sequence formed by the first two arrows of `S` is exact and the tail `S.δ₀` of the sequence is also exact, then the entire sequence `S` is exact. This theorem is used in the proof of the Snake Lemma in the context of short complexes in homological algebra.
More concisely: If `C` is a category with zero morphisms and `S` is a functor from the finite category `Fin (n + 2)` to `C` with exact sequences `S.0 ⊣ S.1` and `S.δ₀`, then `S` is an exact sequence.
|
CategoryTheory.ComposableArrows.IsComplex.zero
theorem CategoryTheory.ComposableArrows.IsComplex.zero :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{n : ℕ} {S : CategoryTheory.ComposableArrows C n},
S.IsComplex →
∀ (i : ℕ) (hi : autoParam (i + 2 ≤ n) _auto✝),
CategoryTheory.CategoryStruct.comp (S.map' i (i + 1) ⋯ ⋯) (S.map' (i + 1) (i + 2) ⋯ hi) = 0
This theorem, named `CategoryTheory.ComposableArrows.IsComplex.zero`, states the following:
For any category `C` with zero morphisms and any `n`, if `S` is a Functor from the category `Fin (n + 1)` to `C` (referred to as `ComposableArrows`), and it satisfies the `IsComplex` condition, then the composition of two consecutive arrows (morphisms) in this Functor is zero. More specifically, for any natural number `i` under an automatic parameter condition that `i + 2` is less than or equal to `n`, the composition of the morphism from `i` to `i + 1` and the morphism from `i + 1` to `i + 2` equals zero. Note that the `autoParam` here is used for automatic parameter support during elaboration but not during type class resolution.
More concisely: In any category with zero morphisms, if a Functor from the category of length `n+1` satisfying the `IsComplex` condition has consecutive morphisms from `i` to `i+1` and `i+1` to `i+2` (where `i < n`), then their composition is the zero morphism.
|