Universal coefficients over a field

Over a field k every module is free, so the singular homology Hₙ(X; k) of a space X is projective in every degree and the universal coefficient theorem with projective homology (TopCat.singularKroneckerEquivOfProjectiveHomology) applies with no hypothesis on X: the Ext¹ term vanishes and the Kronecker map identifies singular cohomology with the dual of singular homology,

Hⁿ(X; k) ≃ₗ[k] Module.Dual k (Hₙ(X; k)).

The identification is the Kronecker pairing, so it is natural in X: the pull-back along a continuous map corresponds to the transpose of the push-forward on homology. Consequently Hⁿ(X; k) is finite-dimensional exactly when Hₙ(X; k) is, and the two have the same finrank (both are zero in the infinite-dimensional case). The same holds for the relative cohomology and homology of a topological pair. For an arbitrary coefficient module M the isomorphism Hⁿ(X; k, M) ≃ₗ[k] (Hₙ(X; k) ⟶ M) is TopCat.singularKroneckerEquivOfProjectiveHomology itself, whose projectivity hypotheses are found by instance search over a field.

Main declarations

• TopCat.singularCohomologyDualEquiv: the natural isomorphism Hⁿ(X; k) ≃ₗ[k] Module.Dual k (Hₙ(X; k)), characterized by TopCat.singularCohomologyDualEquiv_apply and TopCat.singularKronecker_singularCohomologyDualEquiv_symm, with naturality TopCat.singularCohomologyDualEquiv_singularCohomologyMap.
• TopCat.finrank_singularCohomology and TopCat.finite_singularCohomology_iff: cohomology and homology over a field have the same finrank (zero when infinite-dimensional) and are finite-dimensional together.
• TopPair.singularCohomologyDualEquiv, its naturality TopPair.singularCohomologyDualEquiv_singularCohomologyMap, TopPair.finrank_singularCohomology and TopPair.finite_singularCohomology_iff: the same for relative cohomology of a pair.

References

• A. Hatcher, Algebraic Topology, Section 3.1, Theorem 3.2 and the discussion of field coefficients following it.

noncomputable def TopCat.singularCohomologyDualEquiv {k : Type w} [Field k] (X : TopCat) (n : ℕ) : ↑(TopCat.singularCohomology (↧k) k (↧k) X n) ≃ₗ[k] Module.Dual k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).obj X)

The universal coefficient theorem over a field: singular cohomology with coefficients in a field k is the dual of singular homology, Hⁿ(X; k) ≃ₗ[k] Module.Dual k (Hₙ(X; k)). It sends a class to the linear form underlying its Kronecker pairing (TopCat.singularCohomologyDualEquiv_apply).

@[simp]

theorem TopCat.singularCohomologyDualEquiv_apply {k : Type w} [Field k] (X : TopCat) (n : ℕ) (α : ↑(TopCat.singularCohomology (↧k) k (↧k) X n)) : (X.singularCohomologyDualEquiv n) α = ModuleCat.Hom.hom ((X.singularKronecker k n) α)

The equivalence TopCat.singularCohomologyDualEquiv is the Kronecker map.

@[simp]

theorem TopCat.singularKronecker_singularCohomologyDualEquiv_symm {k : Type w} [Field k] (X : TopCat) (n : ℕ) (φ : Module.Dual k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).obj X)) : (X.singularKronecker k n) ((X.singularCohomologyDualEquiv n).symm φ) = ModuleCat.ofHom φ

The inverse of TopCat.singularCohomologyDualEquiv sends a linear form φ to the class whose Kronecker pairing is φ.

theorem TopCat.singularCohomologyDualEquiv_singularCohomologyMap {k : Type w} [Field k] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (α : ↑(TopCat.singularCohomology (↧k) k (↧k) Y n)) : (X.singularCohomologyDualEquiv n) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f n)) α) = (Module.Dual.transpose (ModuleCat.Hom.hom (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).map f))) ((Y.singularCohomologyDualEquiv n) α)

Naturality of the universal coefficient isomorphism over a field: for a continuous map f : X ⟶ Y, the linear form of the pull-back f^*α is the transpose of f_* : Hₙ(X; k) ⟶ Hₙ(Y; k) applied to the linear form of α.

@[simp]

theorem TopCat.finrank_singularCohomology {k : Type w} [Field k] (X : TopCat) (n : ℕ) : Module.finrank k ↑(TopCat.singularCohomology (↧k) k (↧k) X n) = Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).obj X)

Over a field, singular cohomology and singular homology have the same finrank in every degree. When Hₙ(X; k) is infinite-dimensional both sides have finrank zero; their cardinal dimensions then need not agree.

theorem TopCat.finite_singularCohomology_iff {k : Type w} [Field k] (X : TopCat) (n : ℕ) : Module.Finite k ↑(TopCat.singularCohomology (↧k) k (↧k) X n) ↔ Module.Finite k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).obj X)

Over a field, singular cohomology is finite-dimensional in a given degree exactly when singular homology is.

noncomputable def TopPair.singularCohomologyDualEquiv {k : Type w} [Field k] (P : TopPair) (n : ℕ) : ↑(P.singularCohomology (↧k) k (↧k) n) ≃ₗ[k] Module.Dual k ↑(P.singularHomology (↧k) n)

The relative universal coefficient theorem over a field: the relative singular cohomology of a pair with coefficients in a field k is the dual of its relative singular homology, Hⁿ(X, A; k) ≃ₗ[k] Module.Dual k (Hₙ(X, A; k)). It sends a class to the linear form underlying its relative Kronecker pairing (TopPair.singularCohomologyDualEquiv_apply).

@[simp]

theorem TopPair.singularCohomologyDualEquiv_apply {k : Type w} [Field k] (P : TopPair) (n : ℕ) (α : ↑(P.singularCohomology (↧k) k (↧k) n)) : (P.singularCohomologyDualEquiv n) α = ModuleCat.Hom.hom ((P.singularKronecker k n) α)

The equivalence TopPair.singularCohomologyDualEquiv is the relative Kronecker map.

@[simp]

theorem TopPair.singularKronecker_singularCohomologyDualEquiv_symm {k : Type w} [Field k] (P : TopPair) (n : ℕ) (φ : Module.Dual k ↑(P.singularHomology (↧k) n)) : (P.singularKronecker k n) ((P.singularCohomologyDualEquiv n).symm φ) = ModuleCat.ofHom φ

The inverse of TopPair.singularCohomologyDualEquiv sends a linear form φ to the class whose Kronecker pairing is φ.

theorem TopPair.singularCohomologyDualEquiv_singularCohomologyMap {k : Type w} [Field k] {P P' : TopPair} (f : P ⟶ P') (n : ℕ) (α : ↑(P'.singularCohomology (↧k) k (↧k) n)) : (P.singularCohomologyDualEquiv n) ((CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap f n)) α) = (Module.Dual.transpose (ModuleCat.Hom.hom (TopPair.singularHomologyMap f (↧k) n))) ((P'.singularCohomologyDualEquiv n) α)

Naturality of the relative universal coefficient isomorphism over a field: for a map of pairs f : P ⟶ P', the linear form of the pull-back f^*α is the transpose of f_* : Hₙ(X, A; k) ⟶ Hₙ(X', A'; k) applied to the linear form of α.

@[simp]

theorem TopPair.finrank_singularCohomology {k : Type w} [Field k] (P : TopPair) (n : ℕ) : Module.finrank k ↑(P.singularCohomology (↧k) k (↧k) n) = Module.finrank k ↑(P.singularHomology (↧k) n)

Over a field, relative singular cohomology and relative singular homology of a pair have the same finrank in every degree. When Hₙ(X, A; k) is infinite-dimensional both sides have finrank zero; their cardinal dimensions then need not agree.

theorem TopPair.finite_singularCohomology_iff {k : Type w} [Field k] (P : TopPair) (n : ℕ) : Module.Finite k ↑(P.singularCohomology (↧k) k (↧k) n) ↔ Module.Finite k ↑(P.singularHomology (↧k) n)

Over a field, relative singular cohomology is finite-dimensional in a given degree exactly when relative singular homology is.