The Kronecker map of singular cohomology

Let C be a k-linear abelian category with coproducts. For a space X, the Kronecker map of singular cochains is the Kronecker map TauCeti.ChainComplex.kronecker of the singular chain complex of X with coefficients in R: it evaluates a singular cohomology class in Hⁿ(X; R, M) on singular homology classes in Hₙ(X; R), giving a k-linear map Hⁿ(X; R, M) →ₗ[k] (Hₙ(X; R) ⟶ M). On the classes of a cocycle φ and a cycle z it is φ evaluated on z. It is natural in X: evaluating the pull-back f^*α of a class along a continuous map f is evaluating α after pushing forward along f.

For coefficients in modules over a commutative ring k, take C := ModuleCat k and R := k; then this is the evaluation ⟨α, x⟩ ∈ M of a class α ∈ Hⁿ(X; M) on a class x ∈ Hₙ(X; k), which is how cohomology classes are paired with fundamental classes of manifolds. When M is an injective object, for instance a vector space over a field k, the Kronecker map is a k-linear equivalence Hⁿ(X; M) ≃ₗ[k] Hom(Hₙ(X; k), M): the universal coefficient theorem in the case where its Ext¹-term vanishes.

Main definitions and results

• TopCat.singularKronecker: the Kronecker map of singular cohomology, with TopCat.singularKronecker_homologyπ computing it on classes of cocycles and cycles and TopCat.singularKronecker_naturality its naturality.
• TopCat.singularKroneckerEquiv: for an injective coefficient object M, the Kronecker map is a k-linear equivalence.

References

• A. Hatcher, Algebraic Topology, Section 3.1.

noncomputable def TopCat.singularKronecker {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (n : ℕ) : ↑(TopCat.singularCohomology R k M X n) →ₗ[k] ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj X ⟶ M

The Kronecker map of singular cohomology Hⁿ(X; R, M) →ₗ[k] (Hₙ(X; R) ⟶ M): it sends the class of a singular cocycle φ to the morphism which on the class of a singular cycle is φ evaluated on that cycle (TopCat.singularKronecker_homologyπ).

Equations

• X.singularKronecker k n = TauCeti.ChainComplex.kronecker k ((TopCat.toSSet.obj X).chainComplex R) M n

@[simp]

theorem TopCat.singularKronecker_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (n : ℕ) (φ : ↑(HomologicalComplex.cycles (singularCochainComplex R k M X) n)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex R) n) ((X.singularKronecker k n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex R k M X) n)) φ)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((toSSet.obj X).chainComplex R) n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (singularCochainComplex R k M X) n)) φ)

The Kronecker map on the classes of a singular cocycle and a singular cycle is the cocycle evaluated on the cycle.

theorem TopCat.singularKronecker_homologyπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (n : ℕ) (φ : ↑(HomologicalComplex.cycles (singularCochainComplex R k M X) n)) {Z : C} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex R) n) ((X.singularKronecker k n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex R k M X) n)) φ))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles ((toSSet.obj X).chainComplex R) n) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (singularCochainComplex R k M X) n)) φ)) h

The Kronecker map on the classes of a singular cocycle and a singular cycle is the cocycle evaluated on the cycle.

theorem TopCat.singularKronecker_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} {X Y : TopCat} (f : X ⟶ Y) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (n : ℕ) (α : ↑(TopCat.singularCohomology R k M Y n)) : (X.singularKronecker k n) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f n)) α) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C n).obj R).map f) ((Y.singularKronecker k n) α)

Naturality of the Kronecker map, ⟨f^*α, x⟩ = ⟨α, f_*x⟩: for a continuous map f : X ⟶ Y, evaluating the pull-back of a singular cohomology class of Y is evaluating the class after pushing forward along f.

noncomputable def TopCat.singularKroneckerEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Injective M] (n : ℕ) : ↑(TopCat.singularCohomology R k M X n) ≃ₗ[k] ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj X ⟶ M

The universal coefficient theorem for injective coefficients: for an injective object M, the Kronecker map of singular cohomology is a k-linear equivalence Hⁿ(X; R, M) ≃ₗ[k] (Hₙ(X; R) ⟶ M).

Equations

• X.singularKroneckerEquiv k n = TauCeti.ChainComplex.kroneckerEquiv k ((TopCat.toSSet.obj X).chainComplex R) M n

@[simp]

theorem TopCat.singularKroneckerEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Injective M] (n : ℕ) (α : ↑(TopCat.singularCohomology R k M X n)) : (X.singularKroneckerEquiv k n) α = (X.singularKronecker k n) α

The equivalence TopCat.singularKroneckerEquiv is the Kronecker map.