Theorems · Definition · category theory

HomologicalComplex.alternatingConstHomologyIsoOdd

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) →
            (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) →
              {c : ComplexShape ℕ} →
                [inst_2 : DecidableRel c.Rel] →
                  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) →
                    [inst_3 : CategoryTheory.CategoryWithHomology C] →
                      {j : ℕ} →
                        c.Rel (c.prev j) j →
                          c.Rel j (c.next j) →
                            Odd j →
                              ((HomologicalComplex.alternatingConst A hOdd hEven hc).homology j ≅
                                { X₁ := A, X₂ := A, X₃ := A, f := φ, g := ψ, zero := hOdd }.homology)

The jth homology of the alternating constant complex on φ, ψ : A ⟶ A is the homology of A --φ--> A --ψ--> A when prev(j) ~ j, j ~ next(j) and j is odd.

Defined in

Mathlib.Algebra.Homology.AlternatingConst

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsDecidableRelCategoryTheory.CategoryWithHomology