Theorems · Definition · category theory

ChainComplex.ofHom

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

A constructor for chain maps between α-indexed chain complexes built using ChainComplex.of, from a dependently typed collection of morphisms.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOne