Theorems · Definition · category theory

CategoryTheory.ShortComplex.Homotopy.unop

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

The homotopy between morphisms in ShortComplex C that is induced by a homotopy between morphisms in ShortComplex Cᵒᵖ.

Defined in

Mathlib.Algebra.Homology.ShortComplex.Preadditive

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive