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.{u_2, u_1} C] [CategoryTheory.Preadditive C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting) : CochainComplex.HomComplex.Cocycle S.X₃ S.X₁ 1

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

Equations

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

def CochainComplex.homOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

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

@[simp]

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

def CochainComplex.triangleOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

• CochainComplex.triangleOfDegreewiseSplit S σ = CategoryTheory.Pretriangulated.Triangle.mk S.f S.g (CochainComplex.homOfDegreewiseSplit S σ)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[reducible, inline]

noncomputable abbrev CochainComplex.trianglehOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

• CochainComplex.trianglehOfDegreewiseSplit S σ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.triangleOfDegreewiseSplit S σ)

noncomputable def CochainComplex.mappingConeHomOfDegreewiseSplitXIso {C : Type u_1} [CategoryTheory.Category.{u_2, 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) : (CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ)).X p ≅ S.X₂.X q

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

Equations

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

noncomputable def CochainComplex.mappingConeHomOfDegreewiseSplitIso {C : Type u_1} [CategoryTheory.Category.{u_2, 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] : CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ) ≅ (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj S.X₂

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

Equations

• CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ = HomologicalComplex.Hom.isoOfComponents (fun (p : ℤ) => CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ p (p + { as := 1 }.as) ⋯) ⋯

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f {C : Type u_1} [CategoryTheory.Category.{u_2, 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 : ℤ) : (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).hom.f i = (CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).hom

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f {C : Type u_1} [CategoryTheory.Category.{u_2, 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 : ℤ) : (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv.f i = (CochainComplex.mappingConeHomOfDegreewiseSplitXIso S σ i (i + 1) ⋯).inv

@[simp]

theorem CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, 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) (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv = -CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)

@[simp]

theorem CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, 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 : CochainComplex.mappingCone (CochainComplex.homOfDegreewiseSplit S σ) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.f) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv h) = CategoryTheory.CategoryStruct.comp (-CochainComplex.mappingCone.inr (CochainComplex.homOfDegreewiseSplit S σ)) h

@[simp]

theorem CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃ {C : Type u_1} [CategoryTheory.Category.{u_2, 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 (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv (CochainComplex.mappingCone.triangle (CochainComplex.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.{u_2, 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 : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle (CochainComplex.homOfDegreewiseSplit S σ)).obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeHomOfDegreewiseSplitIso S σ).inv (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle (CochainComplex.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.{u_2, 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] : (CochainComplex.triangleOfDegreewiseSplit S σ).rotate.rotate ≅ CochainComplex.mappingCone.triangle (CochainComplex.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.

Equations

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

noncomputable def CochainComplex.trianglehOfDegreewiseSplitRotateRotateIso {C : Type u_1} [CategoryTheory.Category.{u_2, 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] : (CochainComplex.trianglehOfDegreewiseSplit S σ).rotate.rotate ≅ CochainComplex.mappingCone.triangleh (CochainComplex.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.

Equations

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

noncomputable def CochainComplex.mappingCone.triangleRotateShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, 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.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

Equations

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

theorem HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit {C : Type u_1} [CategoryTheory.Category.{u_2, 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 σ)