Theorems · Definition · category theory

ChainComplex.of.d

{V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] → [DecidableEq α] → (X : α → V) → ((n : α) → X (n + 1) ⟶ X n) → (i j : α) → X i ⟶ X j

Auxiliary definition for differentials for ChainComplex.of.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

16 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOneDecidableEq