Theorems · Definition · category theory

HomologicalComplex.alternatingConst

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          CategoryTheory.CategoryStruct.comp φ ψ = 0 →
            CategoryTheory.CategoryStruct.comp ψ φ = 0 →
              {c : ComplexShape ℕ} →
                [DecidableRel c.Rel] → (∀ (i j : ℕ), c.Rel i j → Odd (i + j)) → HomologicalComplex C c

Let c : ComplexShape ℕ be such that i j : ℕ have opposite parity if they are related by c. Let φ, ψ : A ⟶ A be such that φ ∘ ψ = ψ ∘ φ = 0. This is a complex of shape c whose objects are all A. For all i, j related by c, dᵢⱼ = φ when i is even, and dᵢⱼ = ψ when i is odd.

Defined in

Mathlib.Algebra.Homology.AlternatingConst

Cited by

13 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsDecidableRel