Theorems · Definition · category theory

CochainComplex.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 ⟶ X (n + 1)) → (i j : α) → X i ⟶ X j

Auxiliary definition for differentials for CochainComplex.of.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

15 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOneDecidableEq