The Kronecker map from cohomology to morphisms out of homology

Let X be a chain complex in a k-linear abelian category C and let Y : C. A cocycle of the cochain complex Hom(X, Y) (ChainComplex.linearYonedaObj) of degree i is a morphism φ : Xᵢ ⟶ Y vanishing on boundaries, so its restriction to the cycles of X descends to a morphism Hᵢ(X) ⟶ Y; the restriction of a coboundary to the cycles is zero. This gives the k-linear Kronecker map Hⁱ(Hom(X, Y)) →ₗ[k] (Hᵢ(X) ⟶ Y), which evaluates cohomology classes on homology classes. It is natural in both X and Y.

When Y is an injective object the Kronecker map is a k-linear equivalence Hⁱ(Hom(X, Y)) ≃ₗ[k] (Hᵢ(X) ⟶ Y). This is the universal coefficient theorem in the case where its Ext¹-term vanishes, as it does for an injective coefficient object, such as a vector space over a field.

Main definitions and results

• TauCeti.ChainComplex.kronecker: the Kronecker map, with TauCeti.ChainComplex.kronecker_homologyπ computing it on classes of cycles and cocycles and TauCeti.ChainComplex.kronecker_naturality its naturality.
• TauCeti.ChainComplex.homologyClassOfComp: the class of the cocycle f ≫ g for a cochain f : Xᵢ ⟶ A vanishing on boundaries, with TauCeti.ChainComplex.homologyπ_kronecker_homologyClassOfComp computing its Kronecker image.
• TauCeti.ChainComplex.kroneckerSection: a k-linear right inverse of the Kronecker map, built from a retraction of the inclusion of the cycles, with TauCeti.ChainComplex.kronecker_surjective_of_isSplitMono.
• TauCeti.ChainComplex.kronecker_bijective and TauCeti.ChainComplex.kroneckerEquiv: for an injective object Y, the Kronecker map is a k-linear equivalence.

References

• A. Hatcher, Algebraic Topology, Section 3.1, the map h : Hⁿ(C; G) → Hom(Hₙ(C), G) and the universal coefficient theorem.

noncomputable def TauCeti.ChainComplex.kronecker {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Linear k C] (X : ChainComplex C α) (Y : C) (i : α) : ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i) →ₗ[k] HomologicalComplex.homology X i ⟶ Y

The Kronecker map Hⁱ(Hom(X, Y)) →ₗ[k] (Hᵢ(X) ⟶ Y): the class of a cocycle φ is sent to the morphism which on the class of a cycle is φ evaluated on that cycle (TauCeti.ChainComplex.kronecker_homologyπ).

Equations

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

@[simp]

theorem TauCeti.ChainComplex.kronecker_homologyπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} (i : α) (φ : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ X i) ((kronecker k X Y i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) φ)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles X i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) φ)

The Kronecker map on classes: evaluating the class of a cocycle φ on the class of a cycle is evaluating φ on the cycle.

@[simp]

theorem TauCeti.ChainComplex.kronecker_homologyπ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} (i : α) (φ : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ X i) (CategoryTheory.CategoryStruct.comp ((kronecker k X Y i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) φ)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles X i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) φ)) h

The Kronecker map on classes: evaluating the class of a cocycle φ on the class of a cycle is evaluating φ on the cycle.

theorem TauCeti.ChainComplex.kronecker_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} {X' : ChainComplex C α} (f : X' ⟶ X) (i : α) (x : ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i)) : (kronecker k X' Y i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k Y).map f.op) i)) x) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) ((kronecker k X Y i) x)

Naturality of the Kronecker map: evaluating the pull-back of a class along a chain map f : X' ⟶ X is evaluating the class after pushing forward along f.

theorem TauCeti.ChainComplex.kronecker_coefficient_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y Z : C} (g : Y ⟶ Z) (i : α) (x : ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i)) : (kronecker k X Z i) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (ChainComplex.linearYonedaObjMap k X g) i)) x) = CategoryTheory.CategoryStruct.comp ((kronecker k X Y i) x) g

Evaluation of cohomology on homology commutes with changing the coefficient object.

noncomputable def TauCeti.ChainComplex.cocycleOfComp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} (Y : C) {i : α} {A : C} (f : X.X i ⟶ A) (hf : CategoryTheory.CategoryStruct.comp (X.d ((ComplexShape.up α).next i) i) f = 0) : (A ⟶ Y) →ₗ[k] ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)

For a morphism f : Xᵢ ⟶ A vanishing on the boundaries coming from Xᵢ₊₁, the k-linear map sending g : A ⟶ Y to the cocycle f ≫ g of Hom(X, Y).

Equations

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

@[simp]

theorem TauCeti.ChainComplex.iCycles_cocycleOfComp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} {i : α} {A : C} (f : X.X i ⟶ A) (hf : CategoryTheory.CategoryStruct.comp (X.d ((ComplexShape.up α).next i) i) f = 0) (g : A ⟶ Y) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) ((cocycleOfComp k Y f hf) g) = CategoryTheory.CategoryStruct.comp f g

The cocycle cocycleOfComp k Y f hf g has underlying cochain f ≫ g.

noncomputable def TauCeti.ChainComplex.homologyClassOfComp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} (Y : C) {i : α} {A : C} (f : X.X i ⟶ A) (hf : CategoryTheory.CategoryStruct.comp (X.d ((ComplexShape.up α).next i) i) f = 0) : (A ⟶ Y) →ₗ[k] ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i)

For a morphism f : Xᵢ ⟶ A vanishing on the boundaries coming from Xᵢ₊₁, the k-linear map sending g : A ⟶ Y to the cohomology class of the cocycle f ≫ g of Hom(X, Y).

Equations

• TauCeti.ChainComplex.homologyClassOfComp k Y f hf = ModuleCat.Hom.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i) ∘ₗ TauCeti.ChainComplex.cocycleOfComp k Y f hf

theorem TauCeti.ChainComplex.homologyClassOfComp_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} {i : α} {A : C} (f : X.X i ⟶ A) (hf : CategoryTheory.CategoryStruct.comp (X.d ((ComplexShape.up α).next i) i) f = 0) (g : A ⟶ Y) (φ : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) (hφ : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) φ = CategoryTheory.CategoryStruct.comp f g) : (homologyClassOfComp k Y f hf) g = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) φ

homologyClassOfComp k Y f hf g is the class of any cocycle with underlying cochain f ≫ g.

@[simp]

theorem TauCeti.ChainComplex.homologyπ_kronecker_homologyClassOfComp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} {i : α} {A : C} (f : X.X i ⟶ A) (hf : CategoryTheory.CategoryStruct.comp (X.d ((ComplexShape.up α).next i) i) f = 0) (g : A ⟶ Y) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ X i) ((kronecker k X Y i) ((homologyClassOfComp k Y f hf) g)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles X i) (CategoryTheory.CategoryStruct.comp f g)

The Kronecker map sends homologyClassOfComp k Y f hf g to the morphism Hᵢ(X) ⟶ Y which on cycles is f ≫ g.

@[simp]

theorem TauCeti.ChainComplex.homologyπ_kronecker_homologyClassOfComp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} {i : α} {A : C} (f : X.X i ⟶ A) (hf : CategoryTheory.CategoryStruct.comp (X.d ((ComplexShape.up α).next i) i) f = 0) (g : A ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ X i) (CategoryTheory.CategoryStruct.comp ((kronecker k X Y i) ((homologyClassOfComp k Y f hf) g)) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles X i) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))

The Kronecker map sends homologyClassOfComp k Y f hf g to the morphism Hᵢ(X) ⟶ Y which on cycles is f ≫ g.

theorem TauCeti.ChainComplex.kronecker_bijective {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} [CategoryTheory.Injective Y] (i : α) : Function.Bijective ⇑(kronecker k X Y i)

The universal coefficient theorem for injective coefficients: for an injective object Y, the Kronecker map Hⁱ(Hom(X, Y)) →ₗ[k] (Hᵢ(X) ⟶ Y) is bijective.

noncomputable def TauCeti.ChainComplex.kroneckerEquiv {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Linear k C] (X : ChainComplex C α) (Y : C) [CategoryTheory.Injective Y] (i : α) : ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i) ≃ₗ[k] HomologicalComplex.homology X i ⟶ Y

The Kronecker map as a k-linear equivalence Hⁱ(Hom(X, Y)) ≃ₗ[k] (Hᵢ(X) ⟶ Y), for an injective object Y.

Equations

• TauCeti.ChainComplex.kroneckerEquiv k X Y i = LinearEquiv.ofBijective (TauCeti.ChainComplex.kronecker k X Y i) ⋯

@[simp]

theorem TauCeti.ChainComplex.kroneckerEquiv_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} [CategoryTheory.Injective Y] (i : α) (x : ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i)) : (kroneckerEquiv k X Y i) x = (kronecker k X Y i) x

The equivalence TauCeti.ChainComplex.kroneckerEquiv is the Kronecker map.

noncomputable def TauCeti.ChainComplex.kroneckerSection {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] (k : Type u_3) [Ring k] [CategoryTheory.Linear k C] (X : ChainComplex C α) (Y : C) (i : α) [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X i)] : (HomologicalComplex.homology X i ⟶ Y) →ₗ[k] ↑(HomologicalComplex.homology (X.linearYonedaObj k Y) i)

The splitting of the universal coefficient sequence: given a retraction of the inclusion of the cycles Zᵢ ⟶ Xᵢ, the k-linear right inverse of the Kronecker map sending g : Hᵢ(X) ⟶ Y to the class of the cocycle Xᵢ ⟶ Zᵢ ⟶ Hᵢ(X) ⟶ Y. It depends on the chosen retraction.

Equations

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

theorem TauCeti.ChainComplex.kroneckerSection_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} (i : α) [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X i)] (g : HomologicalComplex.homology X i ⟶ Y) (φ : ↑(HomologicalComplex.cycles (X.linearYonedaObj k Y) i)) (hφ : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (X.linearYonedaObj k Y) i)) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.retraction (HomologicalComplex.iCycles X i)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ X i) g)) : (kroneckerSection k X Y i) g = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (X.linearYonedaObj k Y) i)) φ

kroneckerSection k X Y i g is the class of the cocycle Xᵢ ⟶ Zᵢ ⟶ Hᵢ(X) ⟶ Y built from the chosen retraction of the cycles.

@[simp]

theorem TauCeti.ChainComplex.kronecker_kroneckerSection {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} (i : α) [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X i)] (g : HomologicalComplex.homology X i ⟶ Y) : (kronecker k X Y i) ((kroneckerSection k X Y i) g) = g

TauCeti.ChainComplex.kroneckerSection is a right inverse of the Kronecker map.

theorem TauCeti.ChainComplex.kronecker_surjective_of_isSplitMono {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {α : Type u_2} [AddRightCancelSemigroup α] [One α] {k : Type u_3} [Ring k] [CategoryTheory.Linear k C] {X : ChainComplex C α} {Y : C} (i : α) [CategoryTheory.IsSplitMono (HomologicalComplex.iCycles X i)] : Function.Surjective ⇑(kronecker k X Y i)

If the inclusion of the cycles Zᵢ ⟶ Xᵢ is a split monomorphism, then every morphism Hᵢ(X) ⟶ Y is the evaluation of a cohomology class of Hom(X, Y).