Documentation

Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

The mapping cone of a monomorphism, up to a quasi-isomorphism #

If S is a short exact short complex of cochain complexes in an abelian category, we construct a quasi-isomorphism descShortComplex S : mappingCone S.f ⟶ S.X₃.

We obtain this by comparing the homology sequence of S and the homology sequence of the homology functor on the homotopy category, applied to the distinguished triangle attached to the mapping cone of S.f.

source
theorem CochainComplex.homologySequenceδ_quotient_mapTriangle_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
(HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯) ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁))
source
theorem CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : C} (h✝ : ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shift n₁).obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T).obj₁ ⟶ Z) :
CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h) h✝ = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁) h✝))
source
noncomputable def CochainComplex.mappingCone.descShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) :
mappingCone S.f ⟶ S.X₃

The canonical morphism mappingCone S.f ⟶ S.X₃ when S is a short complex of cochain complexes.

Equations
Instances For
    source
    @[simp]
    theorem CochainComplex.mappingCone.inr_descShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) :
    CategoryTheory.CategoryStruct.comp (inr S.f) (descShortComplex S) = S.g
    source
    @[simp]
    theorem CochainComplex.mappingCone.inr_descShortComplex_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) {Z : CochainComplex C ℤ} (h : S.X₃ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (inr S.f) (CategoryTheory.CategoryStruct.comp (descShortComplex S) h) = CategoryTheory.CategoryStruct.comp S.g h
    source
    @[simp]
    theorem CochainComplex.mappingCone.inr_f_descShortComplex_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (n : ℤ) :
    CategoryTheory.CategoryStruct.comp ((inr S.f).f n) ((descShortComplex S).f n) = S.g.f n
    source
    @[simp]
    theorem CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (n : ℤ) {Z : C} (h : S.X₃.X n ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((inr S.f).f n) (CategoryTheory.CategoryStruct.comp ((descShortComplex S).f n) h) = CategoryTheory.CategoryStruct.comp (S.g.f n) h
    source
    @[simp]
    theorem CochainComplex.mappingCone.inl_v_descShortComplex_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) :
    CategoryTheory.CategoryStruct.comp ((inl S.f).v i j h) ((descShortComplex S).f j) = 0
    source
    @[simp]
    theorem CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) {Z : C} (h✝ : S.X₃.X j ⟶ Z) :
    CategoryTheory.CategoryStruct.comp ((inl S.f).v i j h) (CategoryTheory.CategoryStruct.comp ((descShortComplex S).f j) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝
    source
    theorem CochainComplex.mappingCone.map_descShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (f : S₁ ⟶ S₂) :
    CategoryTheory.CategoryStruct.comp (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) (descShortComplex S₂) = CategoryTheory.CategoryStruct.comp (descShortComplex S₁) f.τ₃
    source
    theorem CochainComplex.mappingCone.map_descShortComplex_map {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (f : S₁ ⟶ S₂) {D : Type u_2} [_instD : CategoryTheory.Category.{u_3, u_2} D] (F : CategoryTheory.Functor (CochainComplex C ℤ) D) :
    CategoryTheory.CategoryStruct.comp (F.map (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯)) (F.map (descShortComplex S₂)) = CategoryTheory.CategoryStruct.comp (F.map (descShortComplex S₁)) (F.map f.τ₃)
    source
    theorem CochainComplex.mappingCone.map_descShortComplex_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (f : S₁ ⟶ S₂) {Z : CochainComplex C ℤ} (h : S₂.X₃ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) (CategoryTheory.CategoryStruct.comp (descShortComplex S₂) h) = CategoryTheory.CategoryStruct.comp (descShortComplex S₁) (CategoryTheory.CategoryStruct.comp f.τ₃ h)
    source
    theorem CochainComplex.mappingCone.map_descShortComplex_map_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] (S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (f : S₁ ⟶ S₂) {D : Type u_2} [_instD : CategoryTheory.Category.{u_3, u_2} D] (F : CategoryTheory.Functor (CochainComplex C ℤ) D) {Z : D} (h : F.obj S₂.X₃ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (F.map (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯)) (CategoryTheory.CategoryStruct.comp (F.map (descShortComplex S₂)) h) = CategoryTheory.CategoryStruct.comp (F.map (descShortComplex S₁)) (CategoryTheory.CategoryStruct.comp (F.map f.τ₃) h)
    source
    theorem CochainComplex.mappingCone.homologySequenceδ_triangleh {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) :
    (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ (triangleh S.f) n₀ n₁ h = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app (mappingCone S.f)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (descShortComplex S) n₀) (CategoryTheory.CategoryStruct.comp (hS.δ n₀ n₁ h) ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app S.X₁)))
    source
    theorem CochainComplex.mappingCone.quasiIso_descShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) :
    QuasiIso (descShortComplex S)
    source
    theorem CochainComplex.mappingCone.descShortComplex_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (f : S₁ ⟶ S₂) :
    CategoryTheory.CategoryStruct.comp (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) (descShortComplex S₂) = CategoryTheory.CategoryStruct.comp (descShortComplex S₁) f.τ₃
    source
    theorem CochainComplex.mappingCone.descShortComplex_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (f : S₁ ⟶ S₂) {Z : CochainComplex C ℤ} (h : S₂.X₃ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) (CategoryTheory.CategoryStruct.comp (descShortComplex S₂) h) = CategoryTheory.CategoryStruct.comp (descShortComplex S₁) (CategoryTheory.CategoryStruct.comp f.τ₃ h)
    source
    @[simp]
    theorem CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) :
    CategoryTheory.CategoryStruct.comp (mapHomologicalComplexIso S.f F).hom (descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) = (F.mapHomologicalComplex (ComplexShape.up ℤ)).map (descShortComplex S)
    source
    @[simp]
    theorem CochainComplex.mappingCone.mapHomologicalComplexIso_hom_descShortComplex_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) {Z : HomologicalComplex D (ComplexShape.up ℤ)} (h : (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ))).X₃ ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (mapHomologicalComplexIso S.f F).hom (CategoryTheory.CategoryStruct.comp (descShortComplex (S.map (F.mapHomologicalComplex (ComplexShape.up ℤ)))) h) = CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map (descShortComplex S)) h