The universal coefficient sequence for cohomology

Let X be a chain complex in a k-linear abelian category C, with k commutative, and let Y : C. In degree i = j + 1, write Zⱼ for the cycles of X, Bⱼ = ker(Zⱼ ⟶ Hⱼ(X)) for the boundaries, and Hⁱ(Hom(X, Y)) for the cohomology of the cochain complex ChainComplex.linearYonedaObj. This file proves that

0 ⟶ Ext¹(Hⱼ(X), Y) ⟶ Hⁱ(Hom(X, Y)) ⟶ (Hᵢ(X) ⟶ Y) ⟶ 0

is exact and split when the inclusions of the cycles Zᵢ ⟶ Xᵢ and Zⱼ ⟶ Xⱼ are split monomorphisms and Zⱼ is projective. The second map is the Kronecker map TauCeti.ChainComplex.kronecker, which TauCeti.ChainComplex.kroneckerSection splits (in TauCeti.Algebra.Homology.Kronecker). This is the universal coefficient theorem for cohomology. Over a hereditary ring, such as a principal ideal domain, these hypotheses hold for a degreewise projective complex: the cycles and the boundaries are submodules of projective modules, hence projective, and a surjection onto the projective boundaries splits.

The first map is built from the extension class of 0 ⟶ Bⱼ ⟶ Zⱼ ⟶ Hⱼ(X) ⟶ 0. A morphism β : Bⱼ ⟶ Y gives the cocycle Xᵢ ⟶ Bⱼ ⟶ Y of Hom(X, Y), through the corestriction of the differential Xᵢ ⟶ Xⱼ to the boundaries. Its class depends only on the image of β in Ext¹(Hⱼ(X), Y), and every element of Ext¹(Hⱼ(X), Y) is such an image: the map factors through the identification TauCeti.homCokernelEquivExt of Ext¹(Hⱼ(X), Y) with Hom(Bⱼ, Y) modulo the morphisms extending to Zⱼ.

Main declarations

• TauCeti.ChainComplex.extToHomology: the map Ext¹(Hⱼ(X), Y) →ₗ[k] Hⁱ(Hom(X, Y)), characterized by TauCeti.ChainComplex.extToHomology_extClass_comp_mk₀.
• TauCeti.ChainComplex.extToHomology_injective and TauCeti.ChainComplex.exact_extToHomology_kronecker: exactness at the first two places.

References

• A. Hatcher, Algebraic Topology, Section 3.1, Theorem 3.2.
• C. A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Theorem 3.6.5.

noncomputable def TauCeti.ChainComplex.extToHomology {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (X : ChainComplex C α) (Y : C) (i j : α) [CategoryTheory.Projective (HomologicalComplex.cycles X j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)] : CategoryTheory.Abelian.Ext (HomologicalComplex.homology X j) Y 1 →ₗ[k] ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i)

The Ext term of the universal coefficient sequence: the k-linear map Ext¹(Hⱼ(X), Y) →ₗ[k] Hⁱ(Hom(X, Y)). The image of β : Bⱼ ⟶ Y under precomposition with the extension class of 0 ⟶ Bⱼ ⟶ Zⱼ ⟶ Hⱼ(X) ⟶ 0 goes to the class of the cocycle Xᵢ ⟶ Bⱼ ⟶ Y (TauCeti.ChainComplex.extToHomology_extClass_comp_mk₀). It is defined when the cycles Zⱼ are projective and their inclusion Zⱼ ⟶ Xⱼ is split, and is injective when i = j + 1.

Equations

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

theorem TauCeti.ChainComplex.extToHomology_extClass_comp_mk₀ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X : ChainComplex C α} {Y : C} (i j : α) [CategoryTheory.Projective (HomologicalComplex.cycles X j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)] (β : CategoryTheory.Limits.kernel (HomologicalComplex.homologyπ X j) ⟶ Y) (φ : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) (hφ : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift (HomologicalComplex.homologyπ X j) (HomologicalComplex.toCycles X i j) ⋯) β) : (extToHomology k X Y i j) (⋯.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ β) ⋯) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) φ

The characterization of TauCeti.ChainComplex.extToHomology: the class in Ext¹(Hⱼ(X), Y) of a morphism β : Bⱼ ⟶ Y from the boundaries goes to the class of the cocycle Xᵢ ⟶ Bⱼ ⟶ Y.

theorem TauCeti.ChainComplex.extToHomology_injective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X : ChainComplex C α} {Y : C} {i j : α} (hij : j + 1 = i) [CategoryTheory.Projective (HomologicalComplex.cycles X j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)] : Function.Injective ⇑(extToHomology k X Y i j)

Injectivity in the universal coefficient sequence: in degree i = j + 1, the map Ext¹(Hⱼ(X), Y) →ₗ[k] Hⁱ(Hom(X, Y)) is injective. If the cocycle Xᵢ ⟶ Bⱼ ⟶ Y is the coboundary of ψ : Xⱼ ⟶ Y, then β is the restriction of ψ to Bⱼ, so it extends to Zⱼ and its class in Ext¹(Hⱼ(X), Y) vanishes.

theorem TauCeti.ChainComplex.exact_extToHomology_kronecker {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X : ChainComplex C α} {Y : C} {i j : α} (hij : j + 1 = i) [CategoryTheory.Projective (HomologicalComplex.cycles X j)] [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X j)] : Function.Exact ⇑(extToHomology k X Y i j) ⇑(kronecker k X Y i)

Exactness in the middle of the universal coefficient sequence: in degree i = j + 1, a cohomology class of Hom(X, Y) evaluates to zero on homology exactly when it comes from Ext¹(Hⱼ(X), Y). A cocycle vanishing on the cycles Zᵢ factors through the corestriction Xᵢ ⟶ Bⱼ of the differential, which is the cokernel of Zᵢ ⟶ Xᵢ.