Documentation

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

The mapping cone of a morphism of cochain complexes #

In this file, we study the homotopy cofiber HomologicalComplex.homotopyCofiber of a morphism φ : F ⟶ G of cochain complexes indexed by . In this case, we redefine it as CochainComplex.mappingCone φ. The API involves definitions

The mapping cone of a morphism of cochain complexes indexed by .

Equations
Instances For

    The left inclusion in the mapping cone, as a cochain of degree -1.

    Equations
    Instances For

      The first projection from the mapping cone, as a cocyle of degree 1.

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

        In order to obtain identities of cochains involving inl, inr, fst and snd, it is often convenient to use an ext lemma, and use simp lemmas like inl_v_f_fst_v, but it is sometimes possible to get identities of cochains by using rewrites of identities of cochains like inl_fst. Then, similarly as in category theory, if we associate the compositions of cochains to the right as much as possible, it is also interesting to have reassoc variants of lemmas, like inl_fst_assoc.

        Given φ : F ⟶ G, this is the cochain in Cochain (mappingCone φ) K n that is constructed from two cochains α : Cochain F K m (with m + 1 = n) and β : Cochain F K n.

        Equations
        Instances For
          @[simp]
          theorem CochainComplex.mappingCone.inl_v_descCochain_v_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n) (p₁ : ) (p₂ : ) (p₃ : ) (h₁₂ : p₁ + -1 = p₂) (h₂₃ : p₂ + n = p₃) {Z : C} (h : K.X p₃ Z) :
          @[simp]
          theorem CochainComplex.mappingCone.inl_v_descCochain_v {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n) (p₁ : ) (p₂ : ) (p₃ : ) (h₁₂ : p₁ + -1 = p₂) (h₂₃ : p₂ + n = p₃) :
          CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p₁ p₂ h₁₂) ((CochainComplex.mappingCone.descCochain φ α β h).v p₂ p₃ h₂₃) = α.v p₁ p₃
          @[simp]

          Given φ : F ⟶ G, this is the cocycle in Cocycle (mappingCone φ) K n that is constructed from α : Cochain F K m (with m + 1 = n) and β : Cocycle F K n, when a suitable cocycle relation is satisfied.

          Equations
          Instances For

            Given φ : F ⟶ G, this is the morphism mappingCone φ ⟶ K that is constructed from a cochain α : Cochain F K (-1) and a morphism β : G ⟶ K such that δ (-1) 0 α = Cochain.ofHom (φ ≫ β).

            Equations
            Instances For

              Given φ : F ⟶ G, this is the cochain in Cochain (mappingCone φ) K n that is constructed from two cochains α : Cochain F K m (with m + 1 = n) and β : Cochain F K n.

              Equations
              Instances For
                @[simp]
                theorem CochainComplex.mappingCone.liftCochain_v_fst_v_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m) (p₁ : ) (p₂ : ) (p₃ : ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃) {Z : C} (h : F.X p₃ Z) :
                @[simp]
                theorem CochainComplex.mappingCone.liftCochain_v_fst_v {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m) (p₁ : ) (p₂ : ) (p₃ : ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + 1 = p₃) :
                CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂) ((↑(CochainComplex.mappingCone.fst φ)).v p₂ p₃ h₂₃) = α.v p₁ p₃
                @[simp]
                theorem CochainComplex.mappingCone.liftCochain_v_snd_v {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m) (p₁ : ) (p₂ : ) (h₁₂ : p₁ + n = p₂) :
                CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂) ((CochainComplex.mappingCone.snd φ).v p₂ p₂ ) = β.v p₁ p₂ h₁₂

                Given φ : F ⟶ G, this is the cocycle in Cocycle K (mappingCone φ) n that is constructed from α : Cochain K F m (with n + 1 = m) and β : Cocycle K G n, when a suitable cocycle relation is satisfied.

                Equations
                Instances For

                  Given φ : F ⟶ G, this is the morphism K ⟶ mappingCone φ that is constructed from a cocycle α : Cochain K F 1 and a cochain β : Cochain K G 0 when a suitable cocycle relation is satisfied.

                  Equations
                  Instances For
                    @[simp]
                    theorem CochainComplex.mappingCone.liftCochain_descCochain {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {L : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) {n' : } {m' : } (α' : CochainComplex.HomComplex.Cochain F L m') (β' : CochainComplex.HomComplex.Cochain G L n') (h : n + 1 = m) (h' : m' + 1 = n') (p : ) (hp : n + n' = p) :
                    (CochainComplex.mappingCone.liftCochain φ α β h).comp (CochainComplex.mappingCone.descCochain φ α' β' h') hp = α.comp α' + β.comp β'
                    theorem CochainComplex.mappingCone.liftCochain_v_descCochain_v {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C } {L : CochainComplex C } {n : } {m : } (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) {n' : } {m' : } (α' : CochainComplex.HomComplex.Cochain F L m') (β' : CochainComplex.HomComplex.Cochain G L n') (h : n + 1 = m) (h' : m' + 1 = n') (p : ) (hp : n + n' = p) (p₁ : ) (p₂ : ) (p₃ : ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + n' = p₃) (q : ) (hq : p₁ + m = q) :
                    CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂) ((CochainComplex.mappingCone.descCochain φ α' β' h').v p₂ p₃ h₂₃) = CategoryTheory.CategoryStruct.comp (α.v p₁ q hq) (α'.v q p₃ ) + CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) (β'.v p₂ p₃ h₂₃)
                    noncomputable def CochainComplex.mappingCone.mapHomologicalComplexXIso' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] {F : CochainComplex C } {G : CochainComplex C } (φ : F G) [HomologicalComplex.HasHomotopyCofiber φ] (H : CategoryTheory.Functor C D) [H.Additive] [HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up )).map φ)] (n : ) (m : ) (hnm : n + 1 = m) :
                    ((H.mapHomologicalComplex (ComplexShape.up )).obj (CochainComplex.mappingCone φ)).X n (CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up )).map φ)).X n

                    If H : C ⥤ D is an additive functor and φ is a morphism of cochain complexes in C, this is the comparison isomorphism (in each degree n) between the image by H of mappingCone φ and the mapping cone of the image by H of φ. It is an auxiliary definition for mapHomologicalComplexXIso and mapHomologicalComplexIso. This definition takes an extra parameter m : ℤ such that n + 1 = m which may help getting better definitional properties. See also the equational lemma mapHomologicalComplexXIso_eq.

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

                      If H : C ⥤ D is an additive functor and φ is a morphism of cochain complexes in C, this is the comparison isomorphism (in each degree) between the image by H of mappingCone φ and the mapping cone of the image by H of φ.

                      Equations
                      Instances For

                        If H : C ⥤ D is an additive functor and φ is a morphism of cochain complexes in C, this is the comparison isomorphism between the image by H of mappingCone φ and the mapping cone of the image by H of φ.

                        Equations
                        Instances For