Documentation

Mathlib.Algebra.Homology.ShortComplex.Preadditive

Homology of preadditive categories #

In this file, it is shown that if C is a preadditive category, then ShortComplex C is a preadditive category.

Equations
  • CategoryTheory.ShortComplex.instAddHom = { add := fun (φ φ' : S₁ S₂) => { τ₁ := φ.τ₁ + φ'.τ₁, τ₂ := φ.τ₂ + φ'.τ₂, τ₃ := φ.τ₃ + φ'.τ₃, comm₁₂ := , comm₂₃ := } }
Equations
  • CategoryTheory.ShortComplex.instSubHom = { sub := fun (φ φ' : S₁ S₂) => { τ₁ := φ.τ₁ - φ'.τ₁, τ₂ := φ.τ₂ - φ'.τ₂, τ₃ := φ.τ₃ - φ'.τ₃, comm₁₂ := , comm₂₃ := } }
Equations
  • CategoryTheory.ShortComplex.instNegHom = { neg := fun (φ : S₁ S₂) => { τ₁ := -φ.τ₁, τ₂ := -φ.τ₂, τ₃ := -φ.τ₃, comm₁₂ := , comm₂₃ := } }
@[simp]
theorem CategoryTheory.ShortComplex.add_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ + φ').τ₁ = φ.τ₁ + φ'.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.add_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ + φ').τ₂ = φ.τ₂ + φ'.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.add_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ + φ').τ₃ = φ.τ₃ + φ'.τ₃
@[simp]
theorem CategoryTheory.ShortComplex.sub_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ - φ').τ₁ = φ.τ₁ - φ'.τ₁
@[simp]
theorem CategoryTheory.ShortComplex.sub_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ - φ').τ₂ = φ.τ₂ - φ'.τ₂
@[simp]
theorem CategoryTheory.ShortComplex.sub_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (φ : S₁ S₂) (φ' : S₁ S₂) :
(φ - φ').τ₃ = φ.τ₃ - φ'.τ₃
Equations
  • CategoryTheory.ShortComplex.instPreadditive = { homGroup := inferInstance, add_comp := , comp_add := }
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) :
γ.neg.φH = -γ.φH
@[simp]
theorem CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) :
γ.neg.φK = -γ.φK

Given a left homology map data for morphism φ, this is the induced left homology map data for .

Equations
  • γ.neg = { φK := -γ.φK, φH := -γ.φH, commi := , commf' := , commπ := }
Instances For
    @[simp]
    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂) :
    (γ.add γ').φK = γ.φK + γ'.φK
    @[simp]
    theorem CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂) :
    (γ.add γ').φH = γ.φH + γ'.φH
    def CategoryTheory.ShortComplex.LeftHomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.LeftHomologyMapData φ' h₁ h₂) :

    Given left homology map data for morphisms φ and φ', this is the induced left homology map data for φ + φ'.

    Equations
    • γ.add γ' = { φK := γ.φK + γ'.φK, φH := γ.φH + γ'.φH, commi := , commf' := , commπ := }
    Instances For
      @[simp]
      theorem CategoryTheory.ShortComplex.cyclesMap'_neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
      @[simp]
      theorem CategoryTheory.ShortComplex.leftHomologyMap'_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
      @[simp]
      theorem CategoryTheory.ShortComplex.cyclesMap'_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
      @[simp]
      theorem CategoryTheory.ShortComplex.leftHomologyMap'_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
      @[simp]
      theorem CategoryTheory.ShortComplex.cyclesMap'_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
      @[simp]
      theorem CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) :
      γ.neg.φQ = -γ.φQ
      @[simp]
      theorem CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) :
      γ.neg.φH = -γ.φH

      Given a right homology map data for morphism φ, this is the induced right homology map data for .

      Equations
      • γ.neg = { φQ := -γ.φQ, φH := -γ.φH, commp := , commg' := , commι := }
      Instances For
        @[simp]
        theorem CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂) :
        (γ.add γ').φQ = γ.φQ + γ'.φQ
        @[simp]
        theorem CategoryTheory.ShortComplex.RightHomologyMapData.add_φH {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂) :
        (γ.add γ').φH = γ.φH + γ'.φH
        def CategoryTheory.ShortComplex.RightHomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData} (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.RightHomologyMapData φ' h₁ h₂) :

        Given right homology map data for morphisms φ and φ', this is the induced right homology map data for φ + φ'.

        Equations
        • γ.add γ' = { φQ := γ.φQ + γ'.φQ, φH := γ.φH + γ'.φH, commp := , commg' := , commι := }
        Instances For
          @[simp]
          theorem CategoryTheory.ShortComplex.opcyclesMap'_neg {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
          @[simp]
          @[simp]
          theorem CategoryTheory.ShortComplex.opcyclesMap'_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
          @[simp]
          @[simp]
          theorem CategoryTheory.ShortComplex.opcyclesMap'_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
          @[simp]
          theorem CategoryTheory.ShortComplex.HomologyMapData.neg_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) :
          γ.neg.left = γ.left.neg
          @[simp]
          theorem CategoryTheory.ShortComplex.HomologyMapData.neg_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) :
          γ.neg.right = γ.right.neg

          Given a homology map data for a morphism φ, this is the induced homology map data for .

          Equations
          • γ.neg = { left := γ.left.neg, right := γ.right.neg }
          Instances For
            @[simp]
            theorem CategoryTheory.ShortComplex.HomologyMapData.add_left {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂) :
            (γ.add γ').left = γ.left.add γ'.left
            @[simp]
            theorem CategoryTheory.ShortComplex.HomologyMapData.add_right {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂) :
            (γ.add γ').right = γ.right.add γ'.right
            def CategoryTheory.ShortComplex.HomologyMapData.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData} (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂) :

            Given homology map data for morphisms φ and φ', this is the induced homology map data for φ + φ'.

            Equations
            • γ.add γ' = { left := γ.left.add γ'.left, right := γ.right.add γ'.right }
            Instances For
              @[simp]
              theorem CategoryTheory.ShortComplex.homologyMap'_add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
              @[simp]
              theorem CategoryTheory.ShortComplex.homologyMap'_sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ : S₁ S₂} {φ' : S₁ S₂} (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
              theorem CategoryTheory.ShortComplex.Homotopy.ext {C : Type u_1} :
              ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ S₂} (x y : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂), x.h₀ = y.h₀x.h₁ = y.h₁x.h₂ = y.h₂x.h₃ = y.h₃x = y
              theorem CategoryTheory.ShortComplex.Homotopy.ext_iff {C : Type u_1} :
              ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ S₂} (x y : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂), x = y x.h₀ = y.h₀ x.h₁ = y.h₁ x.h₂ = y.h₂ x.h₃ = y.h₃

              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.

              Instances For
                theorem CategoryTheory.ShortComplex.Homotopy.comm₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) :
                φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f self.h₁ + self.h₀ + φ₂.τ₁
                theorem CategoryTheory.ShortComplex.Homotopy.comm₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) :
                φ₁.τ₃ = self.h₃ + CategoryTheory.CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃
                @[simp]
                theorem CategoryTheory.ShortComplex.nullHomotopic_τ₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = CategoryTheory.CategoryStruct.comp h₁ S₂.f + CategoryTheory.CategoryStruct.comp S₁.g h₂
                @[simp]
                theorem CategoryTheory.ShortComplex.nullHomotopic_τ₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = h₀ + CategoryTheory.CategoryStruct.comp S₁.f h₁
                @[simp]
                theorem CategoryTheory.ShortComplex.nullHomotopic_τ₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₃ = CategoryTheory.CategoryStruct.comp h₂ S₂.g + h₃
                def CategoryTheory.ShortComplex.nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                S₁ S₂

                Constructor for null homotopic morphisms, see also Homotopy.ofNullHomotopic and Homotopy.eq_add_nullHomotopic.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The obvious homotopy between two equal morphisms of short complexes.

                  Equations
                  Instances For
                    @[simp]
                    @[simp]
                    @[simp]
                    @[simp]

                    The symmetry of homotopy between morphisms of short complexes.

                    Equations
                    • h.symm = { h₀ := -h.h₀, h₀_f := , h₁ := -h.h₁, h₂ := -h.h₂, h₃ := -h.h₃, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                    Instances For
                      @[simp]
                      @[simp]
                      @[simp]
                      @[simp]

                      If two maps of short complexes are homotopic, their opposites also are.

                      Equations
                      • h.neg = { h₀ := -h.h₀, h₀_f := , h₁ := -h.h₁, h₂ := -h.h₂, h₃ := -h.h₃, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                      Instances For
                        @[simp]
                        theorem CategoryTheory.ShortComplex.Homotopy.trans_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃) :
                        (h₁₂.trans h₂₃).h₀ = h₁₂.h₀ + h₂₃.h₀
                        @[simp]
                        theorem CategoryTheory.ShortComplex.Homotopy.trans_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃) :
                        (h₁₂.trans h₂₃).h₂ = h₁₂.h₂ + h₂₃.h₂
                        @[simp]
                        theorem CategoryTheory.ShortComplex.Homotopy.trans_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃) :
                        (h₁₂.trans h₂₃).h₁ = h₁₂.h₁ + h₂₃.h₁
                        @[simp]
                        theorem CategoryTheory.ShortComplex.Homotopy.trans_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} (h₁₂ : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₂₃ : CategoryTheory.ShortComplex.Homotopy φ₂ φ₃) :
                        (h₁₂.trans h₂₃).h₃ = h₁₂.h₃ + h₂₃.h₃

                        The transitivity of homotopy between morphisms of short complexes.

                        Equations
                        • h₁₂.trans h₂₃ = { h₀ := h₁₂.h₀ + h₂₃.h₀, h₀_f := , h₁ := h₁₂.h₁ + h₂₃.h₁, h₂ := h₁₂.h₂ + h₂₃.h₂, h₃ := h₁₂.h₃ + h₂₃.h₃, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                        Instances For
                          @[simp]
                          theorem CategoryTheory.ShortComplex.Homotopy.add_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                          (h.add h').h₁ = h.h₁ + h'.h₁
                          @[simp]
                          theorem CategoryTheory.ShortComplex.Homotopy.add_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                          (h.add h').h₂ = h.h₂ + h'.h₂
                          @[simp]
                          theorem CategoryTheory.ShortComplex.Homotopy.add_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                          (h.add h').h₃ = h.h₃ + h'.h₃
                          @[simp]
                          theorem CategoryTheory.ShortComplex.Homotopy.add_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                          (h.add h').h₀ = h.h₀ + h'.h₀
                          def CategoryTheory.ShortComplex.Homotopy.add {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                          CategoryTheory.ShortComplex.Homotopy (φ₁ + φ₃) (φ₂ + φ₄)

                          Homotopy between morphisms of short complexes is compatible with addition.

                          Equations
                          • h.add h' = { h₀ := h.h₀ + h'.h₀, h₀_f := , h₁ := h.h₁ + h'.h₁, h₂ := h.h₂ + h'.h₂, h₃ := h.h₃ + h'.h₃, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                          Instances For
                            @[simp]
                            theorem CategoryTheory.ShortComplex.Homotopy.sub_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                            (h.sub h').h₂ = h.h₂ - h'.h₂
                            @[simp]
                            theorem CategoryTheory.ShortComplex.Homotopy.sub_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                            (h.sub h').h₀ = h.h₀ - h'.h₀
                            @[simp]
                            theorem CategoryTheory.ShortComplex.Homotopy.sub_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                            (h.sub h').h₃ = h.h₃ - h'.h₃
                            @[simp]
                            theorem CategoryTheory.ShortComplex.Homotopy.sub_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                            (h.sub h').h₁ = h.h₁ - h'.h₁
                            def CategoryTheory.ShortComplex.Homotopy.sub {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} {φ₃ : S₁ S₂} {φ₄ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h' : CategoryTheory.ShortComplex.Homotopy φ₃ φ₄) :
                            CategoryTheory.ShortComplex.Homotopy (φ₁ - φ₃) (φ₂ - φ₄)

                            Homotopy between morphisms of short complexes is compatible with substraction.

                            Equations
                            • h.sub h' = { h₀ := h.h₀ - h'.h₀, h₀_f := , h₁ := h.h₁ - h'.h₁, h₂ := h.h₂ - h'.h₂, h₃ := h.h₃ - h'.h₃, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                            Instances For
                              @[simp]
                              theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₃ S₁) :
                              (h.compLeft ψ).h₃ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₃
                              @[simp]
                              theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₃ S₁) :
                              (h.compLeft ψ).h₁ = CategoryTheory.CategoryStruct.comp ψ.τ₂ h.h₁
                              @[simp]
                              theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₃ S₁) :
                              (h.compLeft ψ).h₂ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₂
                              @[simp]
                              theorem CategoryTheory.ShortComplex.Homotopy.compLeft_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₃ S₁) :
                              (h.compLeft ψ).h₀ = CategoryTheory.CategoryStruct.comp ψ.τ₁ h.h₀

                              Homotopy between morphisms of short complexes is compatible with precomposition.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₂ S₃) :
                                (h.compRight ψ).h₀ = CategoryTheory.CategoryStruct.comp h.h₀ ψ.τ₁
                                @[simp]
                                theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₂ S₃) :
                                (h.compRight ψ).h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ.τ₂
                                @[simp]
                                theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₂ S₃) :
                                (h.compRight ψ).h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ.τ₁
                                @[simp]
                                theorem CategoryTheory.ShortComplex.Homotopy.compRight_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (ψ : S₂ S₃) :
                                (h.compRight ψ).h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ.τ₃

                                Homotopy between morphisms of short complexes is compatible with postcomposition.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.Homotopy.comp_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂) :
                                  (h.comp h').h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ₁.τ₂ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₂
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.Homotopy.comp_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂) :
                                  (h.comp h').h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ₁.τ₁ + CategoryTheory.CategoryStruct.comp φ₂.τ₂ h'.h₁
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.Homotopy.comp_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂) :
                                  (h.comp h').h₀ = CategoryTheory.CategoryStruct.comp h.h₀ ψ₁.τ₁ + CategoryTheory.CategoryStruct.comp φ₂.τ₁ h'.h₀
                                  @[simp]
                                  theorem CategoryTheory.ShortComplex.Homotopy.comp_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {ψ₁ : S₂ S₃} {ψ₂ : S₂ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂) :
                                  (h.comp h').h₃ = CategoryTheory.CategoryStruct.comp h.h₃ ψ₁.τ₃ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₃

                                  Homotopy between morphisms of short complexes is compatible with composition.

                                  Equations
                                  • h.comp h' = (h.compRight ψ₁).trans (h'.compLeft φ₂)
                                  Instances For
                                    @[simp]
                                    @[simp]
                                    @[simp]
                                    @[simp]

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

                                    Equations
                                    • h.op = { h₀ := h.h₃.op, h₀_f := , h₁ := h.h₂.op, h₂ := h.h₁.op, h₃ := h.h₀.op, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                                    Instances For

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

                                      Equations
                                      • h.unop = { h₀ := h.h₃.unop, h₀_f := , h₁ := h.h₂.unop, h₂ := h.h₁.unop, h₃ := h.h₀.unop, g_h₃ := , comm₁ := , comm₂ := , comm₃ := }
                                      Instances For

                                        Equivalence expressing that two morphisms are homotopic iff their difference is homotopic to zero.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) :
                                          φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ h.h₁ h.h₂ h.h₃
                                          @[simp]
                                          theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                          (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₁ = h₁
                                          @[simp]
                                          theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                          (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₃ = h₃
                                          @[simp]
                                          theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₀ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                          (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₀ = h₀
                                          @[simp]
                                          theorem CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                          (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₂ = h₂
                                          def CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                          CategoryTheory.ShortComplex.Homotopy (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) 0

                                          A morphism constructed with nullHomotopic is homotopic to zero.

                                          Equations
                                          Instances For
                                            def CategoryTheory.ShortComplex.LeftHomologyMapData.ofNullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                            CategoryTheory.ShortComplex.LeftHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂

                                            The left homology map data expressing that null homotopic maps induce the zero morphism in left homology.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def CategoryTheory.ShortComplex.RightHomologyMapData.ofNullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                              CategoryTheory.ShortComplex.RightHomologyMapData (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂

                                              The right homology map data expressing that null homotopic maps induce the zero morphism in right homology.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.LeftHomologyData) (H₂ : S₂.LeftHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                                CategoryTheory.ShortComplex.leftHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
                                                @[simp]
                                                theorem CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.RightHomologyData) (H₂ : S₂.RightHomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                                CategoryTheory.ShortComplex.rightHomologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
                                                @[simp]
                                                theorem CategoryTheory.ShortComplex.homologyMap'_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData) (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                                CategoryTheory.ShortComplex.homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0
                                                @[simp]
                                                theorem CategoryTheory.ShortComplex.leftHomologyMap_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [S₁.HasLeftHomology] [S₂.HasLeftHomology] (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                                CategoryTheory.ShortComplex.leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
                                                @[simp]
                                                theorem CategoryTheory.ShortComplex.rightHomologyMap_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [S₁.HasRightHomology] [S₂.HasRightHomology] (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                                CategoryTheory.ShortComplex.rightHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
                                                @[simp]
                                                theorem CategoryTheory.ShortComplex.homologyMap_nullHomotopic {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S₁ : CategoryTheory.ShortComplex C) (S₂ : CategoryTheory.ShortComplex C) [S₁.HasHomology] [S₂.HasHomology] (h₀ : S₁.X₁ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ S₂.X₁) (h₂ : S₁.X₃ S₂.X₂) (h₃ : S₁.X₃ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) :
                                                CategoryTheory.ShortComplex.homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
                                                theorem CategoryTheory.ShortComplex.Homotopy.leftHomologyMap'_congr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
                                                theorem CategoryTheory.ShortComplex.Homotopy.rightHomologyMap'_congr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
                                                theorem CategoryTheory.ShortComplex.Homotopy.homologyMap'_congr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {φ₁ : S₁ S₂} {φ₂ : S₁ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData) :
                                                theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext_iff {C : Type u_1} :
                                                ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} (x y : S₁.HomotopyEquiv S₂), x = y x.hom = y.hom x.inv = y.inv HEq x.homotopyHomInvId y.homotopyHomInvId HEq x.homotopyInvHomId y.homotopyInvHomId
                                                theorem CategoryTheory.ShortComplex.HomotopyEquiv.ext {C : Type u_1} :
                                                ∀ {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Preadditive C} {S₁ S₂ : CategoryTheory.ShortComplex C} (x y : S₁.HomotopyEquiv S₂), x.hom = y.homx.inv = y.invHEq x.homotopyHomInvId y.homotopyHomInvIdHEq x.homotopyInvHomId y.homotopyInvHomIdx = y

                                                An homotopy equivalence between two short complexes S₁ and S₂ consists of morphisms hom : S₁ ⟶ S₂ and inv : S₂ ⟶ S₁ such that both compositions hominv and invhom are homotopic to the identity.

                                                Instances For

                                                  The homotopy equivalence from a short complex to itself that is induced by the identity.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyHomInvId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) :
                                                    e.symm.homotopyHomInvId = e.homotopyInvHomId
                                                    @[simp]
                                                    theorem CategoryTheory.ShortComplex.HomotopyEquiv.symm_homotopyInvHomId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) :
                                                    e.symm.homotopyInvHomId = e.homotopyHomInvId

                                                    The inverse of a homotopy equivalence.

                                                    Equations
                                                    • e.symm = { hom := e.inv, inv := e.hom, homotopyHomInvId := e.homotopyInvHomId, homotopyInvHomId := e.homotopyHomInvId }
                                                    Instances For
                                                      @[simp]
                                                      theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
                                                      (e.trans e').homotopyHomInvId = (CategoryTheory.ShortComplex.Homotopy.ofEq ).trans (((e'.homotopyHomInvId.compRight e.inv).compLeft e.hom).trans ((CategoryTheory.ShortComplex.Homotopy.ofEq ).trans e.homotopyHomInvId))
                                                      @[simp]
                                                      theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
                                                      (e.trans e').inv = CategoryTheory.CategoryStruct.comp e'.inv e.inv
                                                      @[simp]
                                                      theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
                                                      (e.trans e').homotopyInvHomId = (CategoryTheory.ShortComplex.Homotopy.ofEq ).trans (((e.homotopyInvHomId.compRight e'.hom).compLeft e'.inv).trans ((CategoryTheory.ShortComplex.Homotopy.ofEq ).trans e'.homotopyInvHomId))
                                                      @[simp]
                                                      theorem CategoryTheory.ShortComplex.HomotopyEquiv.trans_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
                                                      (e.trans e').hom = CategoryTheory.CategoryStruct.comp e.hom e'.hom
                                                      def CategoryTheory.ShortComplex.HomotopyEquiv.trans {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {S₁ : CategoryTheory.ShortComplex C} {S₂ : CategoryTheory.ShortComplex C} {S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃) :
                                                      S₁.HomotopyEquiv S₃

                                                      The composition of homotopy equivalences.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For