Documentation

Mathlib.Algebra.Homology.Homotopy

Chain homotopies #

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

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

Instances For

    f (c.next i) i.

    Instances For
      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 : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) {i : ι} {i' : ι} (w : ComplexShape.Rel c i i') :

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

      Instances For

        f j (c.prev j).

        Instances For
          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 : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) {j : ι} {j' : ι} (w : ComplexShape.Rel c j' j) :
          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.

          Instances For
            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.

            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.hom (Homotopy.ofEq h) i j = OfNat.ofNat ((i j : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) 0 Zero.toOfNat0 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.

              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 : ι) :

                Every chain map is homotopic to itself.

                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 : ι) :
                  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.

                  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 : ι) :
                    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.

                    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 : ι) :
                      Homotopy.hom (Homotopy.add h₁ h₂) i j = Homotopy.hom h₁ i j + Homotopy.hom h₂ 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.

                      Instances For

                        homotopy is closed under composition (on the right)

                        Instances For
                          @[simp]

                          homotopy is closed under composition (on the left)

                          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 : ι) :
                            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

                            Instances For

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

                              Instances For

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

                                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.

                                  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.

                                  Instances For

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

                                    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} (hom : (i j : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) (zero : ∀ (i j : ι), ¬ComplexShape.Rel c j ihom i j = 0) (i : ι) (j : ι) :
                                      Homotopy.hom (Homotopy.nullHomotopy hom zero) 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 : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) (zero : ∀ (i j : ι), ¬ComplexShape.Rel c 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.

                                      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 : ι) → ComplexShape.Rel c j i → (HomologicalComplex.X C i HomologicalComplex.X D j)) (i : ι) (j : ι) :
                                        Homotopy.hom (Homotopy.nullHomotopy' h) i j = dite (ComplexShape.Rel c j i) (h i j) fun x => 0

                                        Homotopy to zero for maps constructed with nullHomotopicMap'

                                        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₂₁ : ComplexShape.Rel c k₂ k₁) (r₁₀ : ComplexShape.Rel c k₁ k₀) (hom : (i j : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) :
                                          @[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₂₁ : ComplexShape.Rel c k₂ k₁) (r₁₀ : ComplexShape.Rel c k₁ k₀) (h : (i j : ι) → ComplexShape.Rel c j i → (HomologicalComplex.X C i HomologicalComplex.X D j)) :
                                          @[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₁₀ : ComplexShape.Rel c k₁ k₀) (hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l) (hom : (i j : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) :
                                          @[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₁₀ : ComplexShape.Rel c k₁ k₀) (hk₀ : ∀ (l : ι), ¬ComplexShape.Rel c k₀ l) (h : (i j : ι) → ComplexShape.Rel c j i → (HomologicalComplex.X C i HomologicalComplex.X D j)) :
                                          @[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₁₀ : ComplexShape.Rel c k₁ k₀) (hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁) (hom : (i j : ι) → HomologicalComplex.X C i HomologicalComplex.X D j) :
                                          @[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₁₀ : ComplexShape.Rel c k₁ k₀) (hk₁ : ∀ (l : ι), ¬ComplexShape.Rel c l k₁) (h : (i j : ι) → ComplexShape.Rel c j i → (HomologicalComplex.X C i HomologicalComplex.X D 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 : ι), ¬ComplexShape.Rel c k₀ l) (hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀) (hom : (i j : ι) → HomologicalComplex.X C i HomologicalComplex.X D 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 : ι), ¬ComplexShape.Rel c k₀ l) (hk₀' : ∀ (l : ι), ¬ComplexShape.Rel c l k₀) (h : (i j : ι) → ComplexShape.Rel c j i → (HomologicalComplex.X C i HomologicalComplex.X D 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.

                                          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 = { fst := zero, snd := { fst := one, snd := comm_one } }
                                          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 : HomologicalComplex.X P 0 HomologicalComplex.X Q 1) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 1 0)) (one : HomologicalComplex.X P 1 HomologicalComplex.X Q 2) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero + CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 2 1)) (succ : (n : ) → (p : (f : HomologicalComplex.X P n HomologicalComplex.X Q (n + 1)) ×' (f' : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 2) (n + 1))) → (f'' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 3)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 3) (n + 2))) (n : ) :

                                            An auxiliary construction for mkInductive.

                                            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 : HomologicalComplex.X P 0 HomologicalComplex.X Q 1) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 1 0)) (one : HomologicalComplex.X P 1 HomologicalComplex.X Q 2) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero + CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 2 1)) (succ : (n : ) → (p : (f : HomologicalComplex.X P n HomologicalComplex.X Q (n + 1)) ×' (f' : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 2) (n + 1))) → (f'' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 3)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 3) (n + 2))) :
                                              @[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 : HomologicalComplex.X P 0 HomologicalComplex.X Q 1) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 1 0)) (one : HomologicalComplex.X P 1 HomologicalComplex.X Q 2) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero + CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 2 1)) (succ : (n : ) → (p : (f : HomologicalComplex.X P n HomologicalComplex.X Q (n + 1)) ×' (f' : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 2) (n + 1))) → (f'' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 3)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (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; { fst := CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P (_ : n + 1 = n + 1)).hom I.fst, snd := { fst := CategoryTheory.CategoryStruct.comp I.snd.fst (HomologicalComplex.xPrevIso Q (_ : n + 1 + 1 = n + 1 + 1)).inv, snd := (_ : HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.dFrom P (n + 1)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P (_ : n + 1 = n + 1)).hom (Homotopy.mkInductiveAux₁ e zero one comm_one succ n).fst) + CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Homotopy.mkInductiveAux₁ e zero one comm_one succ n).snd.fst (HomologicalComplex.xPrevIso Q (_ : n + 1 + 1 = n + 1 + 1)).inv) (HomologicalComplex.dTo Q (n + 1))) } }
                                              theorem Homotopy.mkInductiveAux₃ {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] {P : ChainComplex V } {Q : ChainComplex V } (e : P Q) (zero : HomologicalComplex.X P 0 HomologicalComplex.X Q 1) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 1 0)) (one : HomologicalComplex.X P 1 HomologicalComplex.X Q 2) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 0) zero + CategoryTheory.CategoryStruct.comp one (HomologicalComplex.d Q 2 1)) (succ : (n : ) → (p : (f : HomologicalComplex.X P n HomologicalComplex.X Q (n + 1)) ×' (f' : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) n) f + CategoryTheory.CategoryStruct.comp f' (HomologicalComplex.d Q (n + 2) (n + 1))) → (f'' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 3)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 1)) p.snd.fst + CategoryTheory.CategoryStruct.comp f'' (HomologicalComplex.d Q (n + 3) (n + 2))) (i : ) (j : ) (h : i + 1 = j) :

                                              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.

                                              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.

                                                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
                                                • One or more equations did not get rendered due to their size.
                                                • Homotopy.mkCoinductiveAux₁ e zero one comm_one succ 0 = { fst := zero, snd := { fst := one, snd := comm_one } }
                                                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 : HomologicalComplex.X P 1 HomologicalComplex.X Q 0) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) zero) (one : HomologicalComplex.X P 2 HomologicalComplex.X Q 1) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 2) one) (succ : (n : ) → (p : (f : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q n) ×' (f' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 1)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f') → (f'' : HomologicalComplex.X P (n + 3) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 3)) f'') (n : ) :

                                                  An auxiliary construction for mkInductive.

                                                  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 : HomologicalComplex.X P 1 HomologicalComplex.X Q 0) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) zero) (one : HomologicalComplex.X P 2 HomologicalComplex.X Q 1) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 2) one) (succ : (n : ) → (p : (f : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q n) ×' (f' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 1)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f') → (f'' : HomologicalComplex.X P (n + 3) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 3)) f'') :
                                                    @[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 : HomologicalComplex.X P 1 HomologicalComplex.X Q 0) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) zero) (one : HomologicalComplex.X P 2 HomologicalComplex.X Q 1) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 2) one) (succ : (n : ) → (p : (f : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q n) ×' (f' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 1)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f') → (f'' : HomologicalComplex.X P (n + 3) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (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; { fst := CategoryTheory.CategoryStruct.comp I.fst (HomologicalComplex.xPrevIso Q (_ : n + 1 = n + 1)).inv, snd := { fst := CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P (_ : n + 1 + 1 = n + 1 + 1)).hom I.snd.fst, snd := (_ : HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n).fst (HomologicalComplex.xPrevIso Q (_ : n + 1 = n + 1)).inv) (HomologicalComplex.dTo Q (n + 1)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.dFrom P (n + 1)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.xNextIso P (_ : n + 1 + 1 = n + 1 + 1)).hom (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ n).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 : HomologicalComplex.X P 1 HomologicalComplex.X Q 0) (comm_zero : HomologicalComplex.Hom.f e 0 = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 0 1) zero) (one : HomologicalComplex.X P 2 HomologicalComplex.X Q 1) (comm_one : HomologicalComplex.Hom.f e 1 = CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.d Q 0 1) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P 1 2) one) (succ : (n : ) → (p : (f : HomologicalComplex.X P (n + 1) HomologicalComplex.X Q n) ×' (f' : HomologicalComplex.X P (n + 2) HomologicalComplex.X Q (n + 1)) ×' HomologicalComplex.Hom.f e (n + 1) = CategoryTheory.CategoryStruct.comp f (HomologicalComplex.d Q n (n + 1)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 1) (n + 2)) f') → (f'' : HomologicalComplex.X P (n + 3) HomologicalComplex.X Q (n + 2)) ×' HomologicalComplex.Hom.f e (n + 2) = CategoryTheory.CategoryStruct.comp p.snd.fst (HomologicalComplex.d Q (n + 1) (n + 2)) + CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P (n + 2) (n + 3)) f'') (i : ) (j : ) (h : i + 1 = j) :

                                                    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.

                                                    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

                                                        Any complex is homotopy equivalent to itself.

                                                        Instances For

                                                          Being homotopy equivalent is a symmetric relation.

                                                          Instances For

                                                            Homotopy equivalence is a transitive relation.

                                                            Instances For

                                                              An isomorphism of complexes induces a homotopy equivalence.

                                                              Instances For