Documentation

Mathlib.Algebra.Homology.HomotopyCofiber

The homotopy cofiber of a morphism of homological complexes

In this file, we construct the homotopy cofiber of a morphism φ : F ⟶ G between homological complexes in HomologicalComplex C c. In degree i, it is isomorphic to (F.X j) ⊞ (G.X i) if there is a j such that c.Rel i j, and G.X i otherwise. (This is also known as the mapping cone of φ. Under the name CochainComplex.mappingCone, a specific API shall be developed for the case of cochain complexes indexed by .)

When we assume hc : ∀ j, ∃ i, c.Rel i j (which holds in the case of chain complexes, or cochain complexes indexed by ), then for any homological complex K, there is a bijection HomologicalComplex.homotopyCofiber.descEquiv φ K hc between homotopyCofiber φ ⟶ K and the tuples (α, hα) with α : G ⟶ K and hα : Homotopy (φ ≫ α) 0.

We shall also study the cylinder of a homological complex K: this is the homotopy cofiber of the morphism biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K. Then, a morphism K.cylinder ⟶ M is determined by the data of two morphisms φ₀ φ₁ : K ⟶ M and a homotopy h : Homotopy φ₀ φ₁, see cylinder.desc. There is also a homotopy equivalence cylinder.homotopyEquiv K : HomotopyEquiv K.cylinder K. From the construction of the cylinder, we deduce the lemma Homotopy.map_eq_of_inverts_homotopyEquivalences which assert that if a functor inverts homotopy equivalences, then the image of two homotopic maps are equal.

A morphism of homological complexes φ : F ⟶ G has a homotopy cofiber if for all indices i and j such that c.Rel i j, the binary biproduct F.X j ⊞ G.X i exists.

Instances

    The X field of the homological complex homotopyCofiber φ.

    Equations
    Instances For

      The canonical isomorphism (homotopyCofiber φ).X i ≅ F.X j ⊞ G.X i when c.Rel i j.

      Equations
      Instances For

        The canonical isomorphism (homotopyCofiber φ).X i ≅ G.X i when ¬ c.Rel i (c.next i).

        Equations
        Instances For

          The second projection (homotopyCofiber φ).X i ⟶ G.X i.

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

            The right inclusion G.X i ⟶ (homotopyCofiber φ).X i.

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

              The first projection (homotopyCofiber φ).X i ⟶ F.X j when c.Rel i j.

              Equations
              Instances For

                The left inclusion F.X i ⟶ (homotopyCofiber φ).X j when c.Rel j i.

                Equations
                Instances For

                  The d field of the homological complex homotopyCofiber φ.

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

                    The homotopy cofiber of a morphism of homological complexes, also known as the mapping cone.

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

                      The composition φ ≫ mappingCone.inr φ is homotopic to 0.

                      Equations
                      Instances For
                        theorem HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (i : ι) (j : ι) (hij : c.Rel j i) :
                        theorem HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_eq_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] [DecidableRel c.Rel] (hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j) (i : ι) (j : ι) (hij : ¬c.Rel j i) :

                        The morphism homotopyCofiber φ ⟶ K that is induced by a morphism α : G ⟶ K and a homotopy hα : Homotopy (φ ≫ α) 0.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem HomologicalComplex.homotopyCofiber.descSigma_ext_iff {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {F : HomologicalComplex C c} {G : HomologicalComplex C c} [DecidableRel c.Rel] {φ : F G} {K : HomologicalComplex C c} (x : (α : G K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (y : (α : G K) × Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) :
                          x = y x.fst = y.fst ∀ (i j : ι), c.Rel j ix.snd.hom i j = y.snd.hom i j

                          Morphisms homotopyCofiber φ ⟶ K are uniquely determined by a morphism α : G ⟶ K and a homotopy from φ ≫ α to 0.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[reducible, inline]

                            The cylinder object of a homological complex K is the homotopy cofiber of the morphism biprod.lift (𝟙 K) (-𝟙 K) : K ⟶ K ⊞ K.

                            Equations
                            Instances For

                              The left inclusion K ⟶ K.cylinder.

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

                                The right inclusion K ⟶ K.cylinder.

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

                                  The morphism K.cylinder ⟶ F that is induced by two morphisms φ₀ φ₁ : K ⟶ F and a homotopy h : Homotopy φ₀ φ₁.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[reducible, inline]

                                    The left inclusion K.X i ⟶ K.cylinder.X j when c.Rel j i.

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

                                      A null homotopic map K.cylinder ⟶ K.cylinder which identifies to π K ≫ ι₀ K - 𝟙 _, see nullHomotopicMap_eq.

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

                                        The homotopy equivalence between K.cylinder and K.

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

                                          The homotopy between cylinder.ι₀ K and cylinder.ι₁ K.

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

                                            If a functor inverts homotopy equivalences, it sends homotopic maps to the same map.