Theorems · Definition · category theory

CochainComplex.of

{V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            [DecidableEq α] →
              (X : α → V) →
                (d : (n : α) → X n ⟶ X (n + 1)) →
                  (∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) → CochainComplex V α

Construct an α-indexed cochain complex from a dependently-typed differential.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

3 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOneDecidableEq