Theorems · Definition · category theory

HomologicalComplex.alternatingConstScIsoEven

{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)) →
                    {i j k : ℕ} →
                      c.Rel i j →
                        c.Rel j k →
                          Even j →
                            ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k ≅
                              { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven })

The i, j, kth short complex associated to the alternating constant complex on φ, ψ : A ⟶ A is A --ψ--> A --φ--> A when i ~ j, j ~ k and j is even.

Defined in

Mathlib.Algebra.Homology.AlternatingConst

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsDecidableRel