Degreewise split exact sequences of cochain complexes

The main result of this file is the lemma HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit which asserts that a triangle in HomotopyCategory C (ComplexShape.up ℤ) is distinguished iff it is isomorphic to the triangle attached to a degreewise split short exact sequence of cochain complexes.

def CochainComplex.cocycleOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : HomComplex.Cocycle S.X₃ S.X₁ 1

The 1-cocycle attached to a degreewise split short exact sequence of cochain complexes.

def CochainComplex.homOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : S.X₃ ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₁

The canonical morphism S.X₃ ⟶ S.X₁⟦(1 : ℤ)⟧ attached to a degreewise split short exact sequence of cochain complexes.

@[simp]

theorem CochainComplex.homOfDegreewiseSplit_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) (n : ℤ) : (homOfDegreewiseSplit S σ).f n = (↑(cocycleOfDegreewiseSplit S σ)).v n (n + 1) ⋯

def CochainComplex.triangleOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)

The triangle in CochainComplex C ℤ attached to a degreewise split short exact sequence of cochain complexes.

@[simp]

theorem CochainComplex.triangleOfDegreewiseSplit_mor₃ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : (triangleOfDegreewiseSplit S σ).mor₃ = homOfDegreewiseSplit S σ

@[simp]

theorem CochainComplex.triangleOfDegreewiseSplit_obj₁ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : (triangleOfDegreewiseSplit S σ).obj₁ = S.X₁

@[simp]

theorem CochainComplex.triangleOfDegreewiseSplit_mor₂ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : (triangleOfDegreewiseSplit S σ).mor₂ = S.g

@[simp]

theorem CochainComplex.triangleOfDegreewiseSplit_mor₁ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : (triangleOfDegreewiseSplit S σ).mor₁ = S.f

@[simp]

theorem CochainComplex.triangleOfDegreewiseSplit_obj₃ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : (triangleOfDegreewiseSplit S σ).obj₃ = S.X₃

@[simp]

theorem CochainComplex.triangleOfDegreewiseSplit_obj₂ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : (triangleOfDegreewiseSplit S σ).obj₂ = S.X₂

@[reducible, inline]

noncomputable abbrev CochainComplex.trianglehOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))

The (distinguished) triangle in HomotopyCategory C (ComplexShape.up ℤ) attached to a degreewise split short exact sequence of cochain complexes.

noncomputable def CochainComplex.mappingConeHomOfDegreewiseSplitXIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] (p q : ℤ) (hpq : p + 1 = q) : (mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q

The canonical isomorphism (mappingCone (homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q when p + 1 = q.

noncomputable def CochainComplex.mappingConeHomOfDegreewiseSplitIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] : mappingCone (homOfDegreewiseSplit S σ) ≅ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj S.X₂

The canonical isomorphism mappingCone (homOfDegreewiseSplit S σ) ≅ S.X₂⟦(1 : ℤ)⟧.

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] (i : ℤ) : (mappingConeHomOfDegreewiseSplitIso S σ).hom.f i = (mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).hom

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] (i : ℤ) : (mappingConeHomOfDegreewiseSplitIso S σ).inv.f i = (mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).inv

@[simp]

theorem CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f) (mappingConeHomOfDegreewiseSplitIso S σ).inv = -mappingCone.inr (homOfDegreewiseSplit S σ)

@[simp]

theorem CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] {Z : CochainComplex C ℤ} (h : mappingCone (homOfDegreewiseSplit S σ) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f) (CategoryTheory.CategoryStruct.comp (mappingConeHomOfDegreewiseSplitIso S σ).inv h) = CategoryTheory.CategoryStruct.comp (-mappingCone.inr (homOfDegreewiseSplit S σ)) h

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] : CategoryTheory.CategoryStruct.comp (mappingConeHomOfDegreewiseSplitIso S σ).inv (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] {Z : CochainComplex C ℤ} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (mappingCone.triangle (homOfDegreewiseSplit S σ)).obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (mappingConeHomOfDegreewiseSplitIso S σ).inv (CategoryTheory.CategoryStruct.comp (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ h) = CategoryTheory.CategoryStruct.comp (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g) h

noncomputable def CochainComplex.triangleOfDegreewiseSplitRotateRotateIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] : (triangleOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangle (homOfDegreewiseSplit S σ)

The canonical isomorphism of triangles (triangleOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangle (homOfDegreewiseSplit S σ) when S is a degreewise split short exact sequence of cochain complexes.

noncomputable def CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) [CategoryTheory.Limits.HasBinaryBiproducts C] : (trianglehOfDegreewiseSplit S σ).rotate.rotate ≅ mappingCone.triangleh (homOfDegreewiseSplit S σ)

The canonical isomorphism between (trianglehOfDegreewiseSplit S σ).rotate.rotate and mappingCone.triangleh (homOfDegreewiseSplit S σ) when S is a degreewise split short exact sequence of cochain complexes.

noncomputable def CochainComplex.mappingCone.triangleRotateShortComplex {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : CategoryTheory.ShortComplex (CochainComplex C ℤ)

Given a morphism of cochain complexes φ, this is the short complex given by (triangle φ).rotate.

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplex_g {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangleRotateShortComplex φ).g = (triangle φ).rotate.mor₂

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplex_X₂ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangleRotateShortComplex φ).X₂ = (triangle φ).rotate.obj₂

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplex_X₃ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangleRotateShortComplex φ).X₃ = (triangle φ).rotate.obj₃

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplex_f {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangleRotateShortComplex φ).f = (triangle φ).rotate.mor₁

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplex_X₁ {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangleRotateShortComplex φ).X₁ = (triangle φ).rotate.obj₁

noncomputable def CochainComplex.mappingCone.triangleRotateShortComplexSplitting {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : ((triangleRotateShortComplex φ).map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting

triangleRotateShortComplex φ is a degreewise split short exact sequence of cochain complexes.

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : (triangleRotateShortComplexSplitting φ n).r = (snd φ).v n n ⋯

@[simp]

theorem CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : (triangleRotateShortComplexSplitting φ n).s = -(inl φ).v (n + 1) n ⋯

@[simp]

theorem CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p : ℤ) : (↑(cocycleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ))).v p (p + 1) ⋯ = -φ.f (p + { as := 1 }.as)

noncomputable def CochainComplex.mappingCone.triangleRotateIsoTriangleOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangle φ).rotate ≅ triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)

The triangle (triangle φ).rotate is isomorphic to a triangle attached to a degreewise split short exact sequence of cochain complexes.

noncomputable def CochainComplex.mappingCone.trianglehRotateIsoTrianglehOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) : (triangleh φ).rotate ≅ trianglehOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)

The triangle (triangleh φ).rotate is isomorphic to a triangle attached to a degreewise split short exact sequence of cochain complexes.

theorem HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting), Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)