HomologicalComplex.exactAt_single_obj

theorem HomologicalComplex.exactAt_single_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι) (A : C) (i : ι), i ≠ j → ((HomologicalComplex.single C c j).obj A).ExactAt i

The theorem `HomologicalComplex.exactAt_single_obj` states that for any category `C` that has zero morphisms and a zero object, and any complex shape `c` indexed by a type `ι` with decidable equality, if `i` and `j` are indices such that `i` is not equal to `j`, and `A` is an object of `C`, then the homological complex created by taking the single object indexed by `j` from `C` and applying it to `A` is exact at `i`. This means that in the short complex formed from this homological complex at `i`, the image of the morphism from the `i-1`th object to the `i`th object is equal to the kernel of the morphism from the `i`th object to the `i+1`th object, according to the definition of exactness in category theory.

More concisely: For any category with zero morphisms and a zero object, and any complex over a decidably equated type index, the homological complex formed by a single object application is exact at indices not equal to that object's index.