Splitting off the top term of a bounded cochain complex

For a cochain complex K over a category with zero morphisms and a zero object, the brutal truncation K.stupidTrunc (ComplexShape.embeddingUpIntLE n) keeps the terms of K in degrees ≤ n and replaces the others by zero. The differentials of K go up in degree, so this truncation is a quotient complex of K: the projection CochainComplex.πStupidTruncLE K n is an isomorphism in every degree ≤ n.

When K vanishes in degrees > n + 1, its top term K.X (n + 1) placed in degree n + 1 is a subcomplex, and in the preadditive setting the two maps form the short complex CochainComplex.topShortComplex K n

K.X (n + 1)[-(n + 1)] ⟶ K ⟶ K.stupidTrunc (embeddingUpIntLE n),

which is split in each degree (CochainComplex.topShortComplexSplitting). Degreewise split short exact sequences of complexes give distinguished triangles in the homotopy category, so this is the step of an induction on the length of a bounded complex: it expresses a bounded complex as an extension of a shorter one by a complex concentrated in a single degree.

Main definitions

• CochainComplex.πStupidTruncLE K n: the projection of K onto its brutal truncation in degrees ≤ n.
• CochainComplex.ιTop K n: the inclusion of the top term of a complex vanishing in degrees > n.
• CochainComplex.topShortComplex K n and CochainComplex.topShortComplexSplitting K n: the degreewise split short complex splitting off the top term.

noncomputable def CochainComplex.πStupidTruncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) : K ⟶ HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE n)

The projection of a cochain complex onto its brutal truncation in degrees ≤ n. It is a map of complexes because the differentials of a cochain complex go up in degree.

Equations

• K.πStupidTruncLE n = (ComplexShape.embeddingUpIntLE n).liftExtend (CategoryTheory.CategoryStruct.id (HomologicalComplex.restriction K (ComplexShape.embeddingUpIntLE n))) ⋯

@[simp]

theorem CochainComplex.πStupidTruncLE_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) {i : ℤ} (hi : i ≤ n) : (K.πStupidTruncLE n).f i = (HomologicalComplex.stupidTruncXIso K (ComplexShape.embeddingUpIntLE n) ⋯).inv

In a retained degree, the projection is the inverse of the canonical identification with the original complex.

theorem CochainComplex.isZero_stupidTrunc_embeddingUpIntLE_X {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) {i : ℤ} (hi : n < i) : CategoryTheory.Limits.IsZero ((HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE n)).X i)

The brutal truncation in degrees ≤ n vanishes in degrees > n.

@[simp]

theorem CochainComplex.πStupidTruncLE_f_of_lt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) {i : ℤ} (hi : n < i) : (K.πStupidTruncLE n).f i = 0

In a degree above the truncation bound, the projection is zero.

theorem CochainComplex.isIso_πStupidTruncLE_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) {i : ℤ} (hi : i ≤ n) : CategoryTheory.IsIso ((K.πStupidTruncLE n).f i)

The projection onto the brutal truncation in degrees ≤ n is an isomorphism in each degree ≤ n.

noncomputable def CochainComplex.ιTop {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] : (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj (K.X n) ⟶ K

The inclusion of the top term K.X n, placed in degree n, into a cochain complex K vanishing in degrees > n.

Equations

• K.ιTop n = HomologicalComplex.mkHomFromSingle (CategoryTheory.CategoryStruct.id (K.X n)) ⋯

@[simp]

theorem CochainComplex.ιTop_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] : (K.ιTop n).f n = (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) n (K.X n)).hom

The inclusion of the top term is the identity in the top degree.

@[simp]

theorem CochainComplex.ιTop_f_of_ne {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE n] {i : ℤ} (hi : i ≠ n) : (K.ιTop n).f i = 0

Away from the top degree, the inclusion of the top term is zero.

@[simp]

theorem CochainComplex.ιTop_comp_πStupidTruncLE {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : CategoryTheory.CategoryStruct.comp (K.ιTop (n + 1)) (K.πStupidTruncLE n) = 0

The inclusion of the top term followed by the projection onto the brutal truncation below it is zero.

@[simp]

theorem CochainComplex.ιTop_comp_πStupidTruncLE_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTop (n + 1)) (CategoryTheory.CategoryStruct.comp (K.πStupidTruncLE n) h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion of the top term followed by the projection onto the brutal truncation below it is zero.

noncomputable def CochainComplex.topShortComplex {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : CategoryTheory.ShortComplex (CochainComplex C ℤ)

The short complex splitting off the top term of a cochain complex K vanishing in degrees > n + 1: the top term in degree n + 1, then K, then the brutal truncation of K in degrees ≤ n.

Equations

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

theorem CochainComplex.topShortComplex_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : K.topShortComplex n = { X₁ := (HomologicalComplex.single C (ComplexShape.up ℤ) (n + 1)).obj (K.X (n + 1)), X₂ := K, X₃ := HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE n), f := K.ιTop (n + 1), g := K.πStupidTruncLE n, zero := ⋯ }

The short complex splitting off the top term is formed by the inclusion of the top term and the projection onto the brutal truncation below it.

@[simp]

theorem CochainComplex.topShortComplex_X₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : (K.topShortComplex n).X₁ = (HomologicalComplex.single C (ComplexShape.up ℤ) (n + 1)).obj (K.X (n + 1))

The first term of the short complex splitting off the top term is the top term placed in degree n + 1.

@[simp]

theorem CochainComplex.topShortComplex_X₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : (K.topShortComplex n).X₂ = K

The middle term of the short complex splitting off the top term is the complex itself.

@[simp]

theorem CochainComplex.topShortComplex_X₃ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : (K.topShortComplex n).X₃ = HomologicalComplex.stupidTrunc K (ComplexShape.embeddingUpIntLE n)

The last term of the short complex splitting off the top term is the brutal truncation in degrees ≤ n.

@[simp]

theorem CochainComplex.topShortComplex_f {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : (K.topShortComplex n).f ≍ K.ιTop (n + 1)

The first map of the short complex splitting off the top term is the top-term inclusion.

@[simp]

theorem CochainComplex.topShortComplex_g {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] : (K.topShortComplex n).g ≍ K.πStupidTruncLE n

The second map of the short complex splitting off the top term is the truncation projection.

noncomputable def CochainComplex.topShortComplexSplitting {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ) (n : ℤ) [K.IsStrictlyLE (n + 1)] (i : ℤ) : ((K.topShortComplex n).map (HomologicalComplex.eval C (ComplexShape.up ℤ) i)).Splitting

The short complex splitting off the top term is split in each degree: in degree n + 1 its first map is an isomorphism and its third term vanishes, and in every other degree its first term vanishes and its second map is an isomorphism.

Equations

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