The even and odd parts of a contractible complex

A cochain complex K is contractible when its identity is null-homotopic, that is, when there is a homotopy h : Homotopy (𝟙 K) 0. If moreover the terms of K vanish outside a finite set s of degrees, then the biproduct of the terms of K in the even degrees of s is isomorphic to the biproduct of the terms in the odd degrees of s:

⨁_{n ∈ s, n even} Kⁿ ≅ ⨁_{n ∈ s, n odd} Kⁿ.

This is the mechanism behind the vanishing of every additive invariant on contractible bounded complexes, and hence behind the homotopy invariance of Euler characteristics.

The isomorphism is the operator d + h. It squares to d h + h d + h h = 1 + h h, so it is an involution exactly when the contracting homotopy squares to zero. A null-homotopy of the identity is a contraction of K onto the zero complex, and TauCeti.Contraction.normalize replaces its homotopy by one which squares to zero (Homotopy.normalize). For that normalized homotopy, d + h, read as a matrix between the even and the odd terms, is inverse to itself; the only bookkeeping is that the entries d h + h d sum to the identity on each term and to zero between distinct terms, which is where the finite support of K enters.

Main definitions

• Homotopy.normalize: a null-homotopy of the identity whose components compose to zero, Homotopy.normalize_hom_comp_hom.
• Homotopy.biproductEvenIsoBiproductOdd: the isomorphism between the even and the odd parts of a contractible complex supported on a finite set of degrees.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Exercise 9.15, where this isomorphism underlies the comparison of K₀ of an additive category with K₀ of its bounded homotopy category.
• Bernhard Keller, Introduction to A-infinity algebras and modules, Section 3.3, for the normalization of a contracting homotopy to one squaring to zero, carried out in TauCeti/Algebra/Homology/Contraction/Basic.lean.

noncomputable def Homotopy.toContractionZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : TauCeti.Contraction K 0

A null-homotopy of the identity of K, as a contraction of K onto the zero complex.

Equations

• h.toContractionZero = { incl := 0, proj := 0, homotopy := CochainComplex.HomComplex.Cochain.ofHomotopy h, incl_comp_proj := ⋯, δ_homotopy := ⋯ }

@[simp]

theorem Homotopy.toContractionZero_incl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : h.toContractionZero.incl = 0

@[simp]

theorem Homotopy.toContractionZero_proj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : h.toContractionZero.proj = 0

noncomputable def Homotopy.normalize {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) : Homotopy (CategoryTheory.CategoryStruct.id K) 0

The null-homotopy of the identity of K obtained by normalizing h: its components compose to zero, Homotopy.normalize_hom_comp_hom.

Equations

• h.normalize = (CochainComplex.HomComplex.Cochain.equivHomotopy (CategoryTheory.CategoryStruct.id K) 0).symm ⟨h.toContractionZero.normalize.homotopy, ⋯⟩

@[simp]

theorem Homotopy.normalize_hom_comp_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasZeroObject C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) (i j k : ℤ) : CategoryTheory.CategoryStruct.comp (h.normalize.hom i j) (h.normalize.hom j k) = 0

The components of the normalized null-homotopy compose to zero.

The operator d + h and the identities satisfied by its square, for a null-homotopy H of the identity whose components compose to zero.

noncomputable def Homotopy.biproductEvenIsoBiproductOdd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {K : CochainComplex C ℤ} [CategoryTheory.Limits.HasFiniteBiproducts C] (h : Homotopy (CategoryTheory.CategoryStruct.id K) 0) {s : Finset ℤ} (hs : ∀ n ∉ s, CategoryTheory.Limits.IsZero (K.X n)) : (⨁ fun (n : ↥({n ∈ s | n % 2 = 0})) => K.X ↑n) ≅ ⨁ fun (n : ↥({n ∈ s | ¬n % 2 = 0})) => K.X ↑n

The even and odd parts of a contractible complex are isomorphic. If the identity of K is null-homotopic and the terms of K vanish outside the finite set s of degrees, then the biproduct of the terms of K in the even degrees of s is isomorphic to the biproduct of its terms in the odd degrees of s. The isomorphism is the operator d + h for the normalized homotopy h, which is its own inverse.

Equations

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