Theorems · Inductive type · category theory

CategoryTheory.ShortComplex.Homotopy

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {S₁ S₂ : CategoryTheory.ShortComplex C} → (S₁ ⟶ S₂) → (S₁ ⟶ S₂) → Type v_1

A homotopy between two morphisms of short complexes S₁ ⟶ S₂ consists of various maps and conditions which will be sufficient to show that they induce the same morphism in homology.

Defined in

Mathlib.Algebra.Homology.ShortComplex.Preadditive

Cited by

77 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive