Documentation

Mathlib.Algebra.Homology.Homotopy

Chain homotopies #

We define chain homotopies, and prove that homotopic chain maps induce the same map on homology.

def dNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (i : ι) :
((i j : ι) → C.X i D.X j) →+ (C.X i D.X i)

The composition of C.d i (c.next i) ≫ f (c.next i) i.

Equations
Instances For
    def fromNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (i : ι) :
    ((i j : ι) → C.X i D.X j) →+ (C.xNext i D.X i)

    f (c.next i) i.

    Equations
    Instances For
      @[simp]
      theorem dNext_eq_dFrom_fromNext {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) (i : ι) :
      theorem dNext_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) {i : ι} {i' : ι} (w : c.Rel i i') :
      (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i i') (f i' i)
      theorem dNext_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) (i : ι) (hi : ¬c.Rel i (c.next i)) :
      (dNext i) f = 0
      @[simp]
      theorem dNext_comp_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} (f : C D) (g : (i j : ι) → D.X i E.X j) (i : ι) :
      ((dNext i) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) = CategoryTheory.CategoryStruct.comp (f.f i) ((dNext i) g)
      @[simp]
      theorem dNext_comp_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) (g : D E) (i : ι) :
      ((dNext i) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) = CategoryTheory.CategoryStruct.comp ((dNext i) f) (g.f i)
      def prevD {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (j : ι) :
      ((i j : ι) → C.X i D.X j) →+ (C.X j D.X j)

      The composition f j (c.prev j) ≫ D.d (c.prev j) j.

      Equations
      Instances For
        theorem prevD_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) (i : ι) (hi : ¬c.Rel (c.prev i) i) :
        (prevD i) f = 0
        def toPrev {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (j : ι) :
        ((i j : ι) → C.X i D.X j) →+ (C.X j D.xPrev j)

        f j (c.prev j).

        Equations
        Instances For
          @[simp]
          theorem prevD_eq_toPrev_dTo {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) (j : ι) :
          theorem prevD_eq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) {j : ι} {j' : ι} (w : c.Rel j' j) :
          (prevD j) f = CategoryTheory.CategoryStruct.comp (f j j') (D.d j' j)
          @[simp]
          theorem prevD_comp_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} (f : C D) (g : (i j : ι) → D.X i E.X j) (j : ι) :
          ((prevD j) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) = CategoryTheory.CategoryStruct.comp (f.f j) ((prevD j) g)
          @[simp]
          theorem prevD_comp_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} (f : (i j : ι) → C.X i D.X j) (g : D E) (j : ι) :
          ((prevD j) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (f i j) (g.f j)) = CategoryTheory.CategoryStruct.comp ((prevD j) f) (g.f j)
          theorem dNext_nat {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (C : ChainComplex V ) (D : ChainComplex V ) (i : ) (f : (i j : ) → C.X i D.X j) :
          (dNext i) f = CategoryTheory.CategoryStruct.comp (C.d i (i - 1)) (f (i - 1) i)
          theorem prevD_nat {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] (C : CochainComplex V ) (D : CochainComplex V ) (i : ) (f : (i j : ) → C.X i D.X j) :
          (prevD i) f = CategoryTheory.CategoryStruct.comp (f i (i - 1)) (D.d (i - 1) i)
          theorem Homotopy.ext_iff {ι : Type u_1} {V : Type u} :
          ∀ {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V} {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C D} (x y : Homotopy f g), x = y x.hom = y.hom
          theorem Homotopy.ext {ι : Type u_1} {V : Type u} :
          ∀ {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V} {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C D} (x y : Homotopy f g), x.hom = y.homx = y
          structure Homotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C D) (g : C D) :
          Type (max u_1 v)

          A homotopy h between chain maps f and g consists of components h i j : C.X i ⟶ D.X j which are zero unless c.Rel j i, satisfying the homotopy condition.

          • hom : (i j : ι) → C.X i D.X j
          • zero : ∀ (i j : ι), ¬c.Rel j iself.hom i j = 0
          • comm : ∀ (i : ι), f.f i = (dNext i) self.hom + (prevD i) self.hom + g.f i
          Instances For
            theorem Homotopy.zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} (self : Homotopy f g) (i : ι) (j : ι) :
            ¬c.Rel j iself.hom i j = 0
            theorem Homotopy.comm {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} (self : Homotopy f g) (i : ι) :
            f.f i = (dNext i) self.hom + (prevD i) self.hom + g.f i
            def Homotopy.equivSubZero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} :
            Homotopy f g Homotopy (f - g) 0

            f is homotopic to g iff f - g is homotopic to 0.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Homotopy.ofEq_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} (h : f = g) (i : ι) (j : ι) :
              (Homotopy.ofEq h).hom i j = 0 i j
              def Homotopy.ofEq {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} (h : f = g) :

              Equal chain maps are homotopic.

              Equations
              Instances For
                @[simp]
                theorem Homotopy.refl_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (f : C D) (i : ι) (j : ι) :
                (Homotopy.refl f).hom i j = 0

                Every chain map is homotopic to itself.

                Equations
                Instances For
                  @[simp]
                  theorem Homotopy.symm_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} (h : Homotopy f g) (i : ι) (j : ι) :
                  h.symm.hom i j = -h.hom i j
                  def Homotopy.symm {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} (h : Homotopy f g) :

                  f is homotopic to g iff g is homotopic to f.

                  Equations
                  • h.symm = { hom := -h.hom, zero := , comm := }
                  Instances For
                    @[simp]
                    theorem Homotopy.trans_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {e : C D} {f : C D} {g : C D} (h : Homotopy e f) (k : Homotopy f g) (i : ι) (j : ι) :
                    (h.trans k).hom i j = h.hom i j + k.hom i j
                    def Homotopy.trans {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {e : C D} {f : C D} {g : C D} (h : Homotopy e f) (k : Homotopy f g) :

                    homotopy is a transitive relation.

                    Equations
                    • h.trans k = { hom := h.hom + k.hom, zero := , comm := }
                    Instances For
                      @[simp]
                      theorem Homotopy.add_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f₁ : C D} {g₁ : C D} {f₂ : C D} {g₂ : C D} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) (i : ι) (j : ι) :
                      (h₁.add h₂).hom i j = h₁.hom i j + h₂.hom i j
                      def Homotopy.add {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f₁ : C D} {g₁ : C D} {f₂ : C D} {g₂ : C D} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) :
                      Homotopy (f₁ + f₂) (g₁ + g₂)

                      the sum of two homotopies is a homotopy between the sum of the respective morphisms.

                      Equations
                      • h₁.add h₂ = { hom := h₁.hom + h₂.hom, zero := , comm := }
                      Instances For
                        @[simp]
                        theorem Homotopy.smul_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} {R : Type u_2} [Semiring R] [CategoryTheory.Linear R V] (h : Homotopy f g) (a : R) (i : ι) (j : ι) :
                        (h.smul a).hom i j = a h.hom i j
                        def Homotopy.smul {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C D} {g : C D} {R : Type u_2} [Semiring R] [CategoryTheory.Linear R V] (h : Homotopy f g) (a : R) :
                        Homotopy (a f) (a g)

                        the scalar multiplication of an homotopy

                        Equations
                        • h.smul a = { hom := fun (i j : ι) => a h.hom i j, zero := , comm := }
                        Instances For
                          @[simp]
                          theorem Homotopy.compRight_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} {e : C D} {f : C D} (h : Homotopy e f) (g : D E) (i : ι) (j : ι) :
                          (h.compRight g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)

                          homotopy is closed under composition (on the right)

                          Equations
                          Instances For
                            @[simp]
                            theorem Homotopy.compLeft_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} {f : D E} {g : D E} (h : Homotopy f g) (e : C D) (i : ι) (j : ι) :
                            (h.compLeft e).hom i j = CategoryTheory.CategoryStruct.comp (e.f i) (h.hom i j)

                            homotopy is closed under composition (on the left)

                            Equations
                            Instances For
                              @[simp]
                              theorem Homotopy.comp_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} {C₃ : HomologicalComplex V c} {f₁ : C₁ C₂} {g₁ : C₁ C₂} {f₂ : C₂ C₃} {g₂ : C₂ C₃} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) (i : ι) (j : ι) :
                              (h₁.comp h₂).hom i j = CategoryTheory.CategoryStruct.comp (h₁.hom i j) (f₂.f j) + CategoryTheory.CategoryStruct.comp (g₁.f i) (h₂.hom i j)
                              def Homotopy.comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C₁ : HomologicalComplex V c} {C₂ : HomologicalComplex V c} {C₃ : HomologicalComplex V c} {f₁ : C₁ C₂} {g₁ : C₁ C₂} {f₂ : C₂ C₃} {g₂ : C₂ C₃} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂) :

                              homotopy is closed under composition

                              Equations
                              • h₁.comp h₂ = (h₁.compRight f₂).trans (h₂.compLeft g₁)
                              Instances For
                                @[simp]
                                theorem Homotopy.compRightId_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : C C} (h : Homotopy f (CategoryTheory.CategoryStruct.id C)) (g : C D) (i : ι) (j : ι) :
                                (h.compRightId g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)

                                a variant of Homotopy.compRight useful for dealing with homotopy equivalences.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Homotopy.compLeftId_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {f : D D} (h : Homotopy f (CategoryTheory.CategoryStruct.id D)) (g : C D) (i : ι) (j : ι) :
                                  (h.compLeftId g).hom i j = CategoryTheory.CategoryStruct.comp (g.f i) (h.hom i j)

                                  a variant of Homotopy.compLeft useful for dealing with homotopy equivalences.

                                  Equations
                                  Instances For

                                    Null homotopic maps can be constructed using the formula hd+dh. We show that these morphisms are homotopic to 0 and provide some convenient simplification lemmas that give a degreewise description of hd+dh, depending on whether we have two differentials going to and from a certain degree, only one, or none.

                                    def Homotopy.nullHomotopicMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (hom : (i j : ι) → C.X i D.X j) :
                                    C D

                                    The null homotopic map associated to a family hom of morphisms C_i ⟶ D_j. This is the same datum as for the field hom in the structure Homotopy. For this definition, we do not need the field zero of that structure as this definition uses only the maps C_i ⟶ C_j when c.Rel j i.

                                    Equations
                                    Instances For
                                      def Homotopy.nullHomotopicMap' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :
                                      C D

                                      Variant of nullHomotopicMap where the input consists only of the relevant maps C_i ⟶ D_j such that c.Rel j i.

                                      Equations
                                      Instances For

                                        Compatibility of nullHomotopicMap with the postcomposition by a morphism of complexes.

                                        theorem Homotopy.nullHomotopicMap'_comp {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} (hom : (i j : ι) → c.Rel j i(C.X i D.X j)) (g : D E) :

                                        Compatibility of nullHomotopicMap' with the postcomposition by a morphism of complexes.

                                        Compatibility of nullHomotopicMap with the precomposition by a morphism of complexes.

                                        theorem Homotopy.comp_nullHomotopicMap' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {E : HomologicalComplex V c} (f : C D) (hom : (i j : ι) → c.Rel j i(D.X i E.X j)) :

                                        Compatibility of nullHomotopicMap' with the precomposition by a morphism of complexes.

                                        theorem Homotopy.map_nullHomotopicMap {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [G.Additive] (hom : (i j : ι) → C.X i D.X j) :
                                        (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap hom) = Homotopy.nullHomotopicMap fun (i j : ι) => G.map (hom i j)

                                        Compatibility of nullHomotopicMap with the application of additive functors

                                        theorem Homotopy.map_nullHomotopicMap' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (G : CategoryTheory.Functor V W) [G.Additive] (hom : (i j : ι) → c.Rel j i(C.X i D.X j)) :
                                        (G.mapHomologicalComplex c).map (Homotopy.nullHomotopicMap' hom) = Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) => G.map (hom i j hij)

                                        Compatibility of nullHomotopicMap' with the application of additive functors

                                        @[simp]
                                        theorem Homotopy.nullHomotopy_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (hom : (i j : ι) → C.X i D.X j) (zero : ∀ (i j : ι), ¬c.Rel j ihom i j = 0) (i : ι) (j : ι) :
                                        (Homotopy.nullHomotopy hom zero).hom i j = hom i j
                                        def Homotopy.nullHomotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (hom : (i j : ι) → C.X i D.X j) (zero : ∀ (i j : ι), ¬c.Rel j ihom i j = 0) :

                                        Tautological construction of the Homotopy to zero for maps constructed by nullHomotopicMap, at least when we have the zero condition.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Homotopy.nullHomotopy'_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i(C.X i D.X j)) (i : ι) (j : ι) :
                                          (Homotopy.nullHomotopy' h).hom i j = dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) => 0
                                          def Homotopy.nullHomotopy' {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :

                                          Homotopy to zero for maps constructed with nullHomotopicMap'

                                          Equations
                                          Instances For

                                            This lemma and the following ones can be used in order to compute the degreewise morphisms induced by the null homotopic maps constructed with nullHomotopicMap or nullHomotopicMap'

                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₂ : ι} {k₁ : ι} {k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀) (hom : (i j : ι) → C.X i D.X j) :
                                            (Homotopy.nullHomotopicMap hom).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁) + CategoryTheory.CategoryStruct.comp (hom k₁ k₂) (D.d k₂ k₁)
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap'_f {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₂ : ι} {k₁ : ι} {k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀) (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :
                                            (Homotopy.nullHomotopicMap' h).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (h k₀ k₁ r₁₀) + CategoryTheory.CategoryStruct.comp (h k₁ k₂ r₂₁) (D.d k₂ k₁)
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap_f_of_not_rel_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₁ : ι} {k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hom : (i j : ι) → C.X i D.X j) :
                                            (Homotopy.nullHomotopicMap hom).f k₀ = CategoryTheory.CategoryStruct.comp (hom k₀ k₁) (D.d k₁ k₀)
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap'_f_of_not_rel_left {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₁ : ι} {k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :
                                            (Homotopy.nullHomotopicMap' h).f k₀ = CategoryTheory.CategoryStruct.comp (h k₀ k₁ r₁₀) (D.d k₁ k₀)
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap_f_of_not_rel_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₁ : ι} {k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ (l : ι), ¬c.Rel l k₁) (hom : (i j : ι) → C.X i D.X j) :
                                            (Homotopy.nullHomotopicMap hom).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁)
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap'_f_of_not_rel_right {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₁ : ι} {k₀ : ι} (r₁₀ : c.Rel k₁ k₀) (hk₁ : ∀ (l : ι), ¬c.Rel l k₁) (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :
                                            (Homotopy.nullHomotopicMap' h).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (h k₀ k₁ r₁₀)
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap_f_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₀ : ι} (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hk₀' : ∀ (l : ι), ¬c.Rel l k₀) (hom : (i j : ι) → C.X i D.X j) :
                                            @[simp]
                                            theorem Homotopy.nullHomotopicMap'_f_eq_zero {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {k₀ : ι} (hk₀ : ∀ (l : ι), ¬c.Rel k₀ l) (hk₀' : ∀ (l : ι), ¬c.Rel l k₀) (h : (i j : ι) → c.Rel j i(C.X i D.X j)) :

                                            Homotopy.mkInductive allows us to build a homotopy of chain complexes inductively, so that as we construct each component, we have available the previous two components, and the fact that they satisfy the homotopy condition.

                                            To simplify the situation, we only construct homotopies of the form Homotopy e 0. Homotopy.equivSubZero can provide the general case.

                                            Notice however, that this construction does not have particularly good definitional properties: we have to insert eqToHom in several places. Hopefully this is okay in most applications, where we only need to have the existence of some homotopy.

                                            @[simp]
                                            theorem Homotopy.prevD_chainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (f : (i j : ) → P.X i Q.X j) (j : ) :
                                            (prevD j) f = CategoryTheory.CategoryStruct.comp (f j (j + 1)) (Q.d (j + 1) j)
                                            @[simp]
                                            theorem Homotopy.dNext_succ_chainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (f : (i j : ) → P.X i Q.X j) (i : ) :
                                            (dNext (i + 1)) f = CategoryTheory.CategoryStruct.comp (P.d (i + 1) i) (f i (i + 1))
                                            @[simp]
                                            theorem Homotopy.dNext_zero_chainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (f : (i j : ) → P.X i Q.X j) :
                                            (dNext 0) f = 0
                                            def Homotopy.mkInductiveAux₁ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : P.X 0 Q.X 1) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ) → (p : (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (n : ) :
                                            (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))

                                            An auxiliary construction for mkInductive.

                                            Here we build by induction a family of diagrams, but don't require at the type level that these successive diagrams actually agree. They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy) in mkInductive.

                                            At this stage, we don't check the homotopy condition in degree 0, because it "falls off the end", and is easier to treat using xNext and xPrev, which we do in mkInductiveAux₂.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            • Homotopy.mkInductiveAux₁ e zero one comm_one succ 0 = zero, one, comm_one
                                            • Homotopy.mkInductiveAux₁ e zero one comm_one succ 1 = one, (succ 0 zero, one, comm_one).fst,
                                            Instances For
                                              def Homotopy.mkInductiveAux₂ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ) → (p : (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (n : ) :

                                              An auxiliary construction for mkInductive.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem Homotopy.mkInductiveAux₂_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ) → (p : (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) :
                                                Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ 0 = 0, CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.xPrevIso Q ).inv,
                                                @[simp]
                                                theorem Homotopy.mkInductiveAux₂_add_one {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ) → (p : (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (n : ) :
                                                Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) = let I := Homotopy.mkInductiveAux₁ e zero one comm_one succ n; CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ).hom I.fst, CategoryTheory.CategoryStruct.comp I.snd.fst (HomologicalComplex.xPrevIso Q ).inv,
                                                theorem Homotopy.mkInductiveAux₃ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ) → (p : (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) (i : ) (j : ) (h : i + 1 = j) :
                                                def Homotopy.mkInductive {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : P.X 0 Q.X 1) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 Q.X 2) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1)) (succ : (n : ) → (p : (f : P.X n Q.X (n + 1)) ×' (f' : P.X (n + 1) Q.X (n + 2)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) → (f'' : P.X (n + 2) Q.X (n + 3)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))) :

                                                A constructor for a Homotopy e 0, for e a chain map between -indexed chain complexes, working by induction.

                                                You need to provide the components of the homotopy in degrees 0 and 1, show that these satisfy the homotopy condition, and then give a construction of each component, and the fact that it satisfies the homotopy condition, using as an inductive hypothesis the data and homotopy condition for the previous two components.

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

                                                  Homotopy.mkCoinductive allows us to build a homotopy of cochain complexes inductively, so that as we construct each component, we have available the previous two components, and the fact that they satisfy the homotopy condition.

                                                  @[simp]
                                                  theorem Homotopy.dNext_cochainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (f : (i j : ) → P.X i Q.X j) (j : ) :
                                                  (dNext j) f = CategoryTheory.CategoryStruct.comp (P.d j (j + 1)) (f (j + 1) j)
                                                  @[simp]
                                                  theorem Homotopy.prevD_succ_cochainComplex {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (f : (i j : ) → P.X i Q.X j) (i : ) :
                                                  (prevD (i + 1)) f = CategoryTheory.CategoryStruct.comp (f (i + 1) i) (Q.d i (i + 1))
                                                  @[simp]
                                                  def Homotopy.mkCoinductiveAux₁ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (e : P Q) (zero : P.X 1 Q.X 0) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ) → (p : (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (n : ) :
                                                  (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'

                                                  An auxiliary construction for mkCoinductive.

                                                  Here we build by induction a family of diagrams, but don't require at the type level that these successive diagrams actually agree. They do in fact agree, and we then capture that at the type level (i.e. by constructing a homotopy) in mkCoinductive.

                                                  At this stage, we don't check the homotopy condition in degree 0, because it "falls off the end", and is easier to treat using xNext and xPrev, which we do in mkInductiveAux₂.

                                                  Equations
                                                  Instances For
                                                    def Homotopy.mkCoinductiveAux₂ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ) → (p : (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (n : ) :

                                                    An auxiliary construction for mkInductive.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[simp]
                                                      theorem Homotopy.mkCoinductiveAux₂_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ) → (p : (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') :
                                                      Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ 0 = 0, CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ).hom zero,
                                                      @[simp]
                                                      theorem Homotopy.mkCoinductiveAux₂_add_one {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ) → (p : (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (n : ) :
                                                      Homotopy.mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n + 1) = let I := Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n; CategoryTheory.CategoryStruct.comp I.fst (HomologicalComplex.xPrevIso Q ).inv, CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P ).hom I.snd.fst,
                                                      theorem Homotopy.mkCoinductiveAux₃ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ) → (p : (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') (i : ) (j : ) (h : i + 1 = j) :
                                                      def Homotopy.mkCoinductive {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : CochainComplex V } {Q : CochainComplex V } (e : P Q) (zero : P.X 1 Q.X 0) (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero) (one : P.X 2 Q.X 1) (comm_one : e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one) (succ : (n : ) → (p : (f : P.X (n + 1) Q.X n) ×' (f' : P.X (n + 2) Q.X (n + 1)) ×' e.f (n + 1) = CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) + CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') → (f'' : P.X (n + 3) Q.X (n + 2)) ×' e.f (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') :

                                                      A constructor for a Homotopy e 0, for e a chain map between -indexed cochain complexes, working by induction.

                                                      You need to provide the components of the homotopy in degrees 0 and 1, show that these satisfy the homotopy condition, and then give a construction of each component, and the fact that it satisfies the homotopy condition, using as an inductive hypothesis the data and homotopy condition for the previous two components.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        structure HomotopyEquiv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} (C : HomologicalComplex V c) (D : HomologicalComplex V c) :
                                                        Type (max u_1 v)

                                                        A homotopy equivalence between two chain complexes consists of a chain map each way, and homotopies from the compositions to the identity chain maps.

                                                        Note that this contains data; arguably it might be more useful for many applications if we truncated it to a Prop.

                                                        Instances For

                                                          The morphism property on HomologicalComplex V c given by homotopy equivalences.

                                                          Equations
                                                          Instances For

                                                            Any complex is homotopy equivalent to itself.

                                                            Equations
                                                            Instances For
                                                              Equations

                                                              Being homotopy equivalent is a symmetric relation.

                                                              Equations
                                                              • f.symm = { hom := f.inv, inv := f.hom, homotopyHomInvId := f.homotopyInvHomId, homotopyInvHomId := f.homotopyHomInvId }
                                                              Instances For

                                                                Homotopy equivalence is a transitive relation.

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

                                                                  An isomorphism of complexes induces a homotopy equivalence.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem CategoryTheory.Functor.mapHomotopy_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] {f : C D} {g : C D} (h : Homotopy f g) (i : ι) (j : ι) :
                                                                    (F.mapHomotopy h).hom i j = F.map (h.hom i j)
                                                                    def CategoryTheory.Functor.mapHomotopy {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] {f : C D} {g : C D} (h : Homotopy f g) :
                                                                    Homotopy ((F.mapHomologicalComplex c).map f) ((F.mapHomologicalComplex c).map g)

                                                                    An additive functor takes homotopies to homotopies.

                                                                    Equations
                                                                    • F.mapHomotopy h = { hom := fun (i j : ι) => F.map (h.hom i j), zero := , comm := }
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem CategoryTheory.Functor.mapHomotopyEquiv_inv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) :
                                                                      (F.mapHomotopyEquiv h).inv = (F.mapHomologicalComplex c).map h.inv
                                                                      @[simp]
                                                                      theorem CategoryTheory.Functor.mapHomotopyEquiv_hom {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) :
                                                                      (F.mapHomotopyEquiv h).hom = (F.mapHomologicalComplex c).map h.hom
                                                                      @[simp]
                                                                      theorem CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) :
                                                                      (F.mapHomotopyEquiv h).homotopyHomInvId = .mpr (.mpr (F.mapHomotopy h.homotopyHomInvId))
                                                                      @[simp]
                                                                      theorem CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) :
                                                                      (F.mapHomotopyEquiv h).homotopyInvHomId = .mpr (.mpr (F.mapHomotopy h.homotopyInvHomId))
                                                                      def CategoryTheory.Functor.mapHomotopyEquiv {ι : Type u_1} {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {c : ComplexShape ι} {C : HomologicalComplex V c} {D : HomologicalComplex V c} {W : Type u_2} [CategoryTheory.Category.{u_3, u_2} W] [CategoryTheory.Preadditive W] (F : CategoryTheory.Functor V W) [F.Additive] (h : HomotopyEquiv C D) :
                                                                      HomotopyEquiv ((F.mapHomologicalComplex c).obj C) ((F.mapHomologicalComplex c).obj D)

                                                                      An additive functor preserves homotopy equivalences.

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

                                                                        A homotopy between morphisms of homological complexes K ⟶ L induces a homotopy between morphisms of short complexes K.sc i ⟶ L.sc i.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          theorem Homotopy.homologyMap_eq {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] {ι : Type u_4} {c : ComplexShape ι} [DecidableRel c.Rel] {K : HomologicalComplex C c} {L : HomologicalComplex C c} {f : K L} {g : K L} (ho : Homotopy f g) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                                          noncomputable def HomotopyEquiv.toHomologyIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Preadditive C] {ι : Type u_4} {c : ComplexShape ι} [DecidableRel c.Rel] {K : HomologicalComplex C c} {L : HomologicalComplex C c} (h : HomotopyEquiv K L) (i : ι) [K.HasHomology i] [L.HasHomology i] :
                                                                          K.homology i L.homology i

                                                                          The isomorphism in homology induced by an homotopy equivalence.

                                                                          Equations
                                                                          Instances For