The cap product of singular homology and cohomology

Let C be a k-linear monoidal category with coproducts. For a space X, the cap product of singular chains and cochains is the cap product of chains and cochains TauCeti.ChainComplex.capChain along the Alexander–Whitney diagonal X.alexanderWhitneyDiagonal u : C(X; T) ⟶ C(X; R) ⊗ C(X; S) of a coefficient morphism u : T ⟶ R ⊗ S, and along the chain map M ⊗ C(X; S) ⟶ C(X; P) induced by a coefficient pairing μ : M ⊗ S ⟶ P (SSet.chainComplexPairing, which needs M ⊗ - to preserve coproducts). A cochain φ of degree p with values in M caps a singular simplex σ of degree n = p + q to the singular q-simplex given by the back q-face of σ, with coefficient φ of the front p-face of σ paired with S through μ, after the coefficient morphism u (TopCat.ιChainComplex_capChain_alexanderWhitneyDiagonal). It satisfies the boundary formula TauCeti.ChainComplex.capChain_comp_d, ∂(σ ⌢ φ) = (-1)^p (∂σ ⌢ φ - σ ⌢ δφ), and so, when C is moreover abelian, descends to the cap product TopCat.singularCap of singular cohomology with singular homology, which is k-linear in the cohomology class and natural in X (the projection formula f_*(x ⌢ f^*α) = f_*x ⌢ α, TopCat.singularCap_naturality).

For coefficients in modules over a commutative ring k, take C := ModuleCat k, R = S = T = 𝟙_ (ModuleCat k) (the module k), u = (λ_ _).inv and μ = (ρ_ M).hom, the action M ⊗ k ⟶ M; then σ ⌢ φ = φ(σ|[0, …, p]) σ|[p, …, n], the cap product of Hatcher, Section 3.3.

Main definitions and results

• TopCat.ιChainComplex_capChain_alexanderWhitneyDiagonal: the cap product of a singular simplex and a singular cochain.
• TopCat.singularCap: the cap product Hᵖ(X; R, M) ⟶ (Hₙ(X; T) ⟶ H_q(X; P)), with TopCat.singularCap_homologyπ computing it on classes of cycles and cocycles and TopCat.singularCap_naturality its naturality.

References

• A. Hatcher, Algebraic Topology, Section 3.3.

theorem TopCat.ιChainComplex_capChain_alexanderWhitneyDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {k : Type u_1} [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {R S T M P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : TopCat) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : ((toSSet.obj X).chainComplex R).X p ⟶ M) (σ : (toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex σ) ((TauCeti.ChainComplex.capChain k (X.alexanderWhitneyDiagonal u) ((toSSet.obj X).chainComplexPairing μ) p q n h) φ) = CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval 0 p ⋯).op)) σ)) φ) S) (CategoryTheory.CategoryStruct.comp μ ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval p q ⋯).op)) σ))))

The cap product of a singular simplex and a singular cochain: for a cochain φ of degree p, the cap product of a singular (p + q)-simplex σ with φ is the back q-face of σ, with coefficient φ of the front p-face of σ paired with S through μ, after the coefficient morphism u.

noncomputable def TopCat.singularCap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) (p q n : ℕ) (h : p + q = n) : ↑(TopCat.singularCohomology R k M X p) →ₗ[k] ((AlgebraicTopology.singularHomologyFunctor C n).obj T).obj X ⟶ ((AlgebraicTopology.singularHomologyFunctor C q).obj P).obj X

The cap product of singular cohomology and singular homology, Hᵖ(X; R, M) ⟶ (Hₙ(X; T) ⟶ H_q(X; P)) for p + q = n: the cap product of homology and cohomology classes along the Alexander–Whitney diagonal X.alexanderWhitneyDiagonal u and the chain map induced by the pairing μ : M ⊗ S ⟶ P, k-linear in the cohomology class and natural in X (TopCat.singularCap_naturality).

Equations

• X.singularCap k u μ p q n h = TauCeti.ChainComplex.cap k (X.alexanderWhitneyDiagonal u) ((TopCat.toSSet.obj X).chainComplexPairing μ) p q n h

@[simp]

theorem TopCat.singularCap_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : ↑(HomologicalComplex.cycles (singularCochainComplex R k M X) p)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex T) n) ((X.singularCap k u μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex R k M X) p)) φ)) = CategoryTheory.CategoryStruct.comp ((TauCeti.ChainComplex.capCycles k (X.alexanderWhitneyDiagonal u) ((toSSet.obj X).chainComplexPairing μ) p q n h) φ) (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex P) q)

The cap product of the class of a singular cycle with the class of a singular cocycle is the class of their cap product.

theorem TopCat.singularCap_homologyπ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] (X : TopCat) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : ↑(HomologicalComplex.cycles (singularCochainComplex R k M X) p)) {Z : C} (h✝ : ((AlgebraicTopology.singularHomologyFunctor C q).obj P).obj X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex T) n) ((X.singularCap k u μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex R k M X) p)) φ))) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((TauCeti.ChainComplex.capCycles k (X.alexanderWhitneyDiagonal u) ((toSSet.obj X).chainComplexPairing μ) p q n h) φ) (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex P) q)) h✝

The cap product of the class of a singular cycle with the class of a singular cocycle is the class of their cap product.

theorem TopCat.singularCap_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M P : C} [∀ (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft M)] {X Y : TopCat} (f : X ⟶ Y) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M S ⟶ P) (p q n : ℕ) (h : p + q = n) (α : ↑(TopCat.singularCohomology R k M Y p)) : CategoryTheory.CategoryStruct.comp ((X.singularCap k u μ p q n h) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f p)) α)) (((AlgebraicTopology.singularHomologyFunctor C q).obj P).map f) = CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C n).obj T).map f) ((Y.singularCap k u μ p q n h) α)

Naturality of the cap product, the projection formula f_*(x ⌢ f^*α) = f_*x ⌢ α: for a continuous map f : X ⟶ Y, capping with the pull-back of a cohomology class of Y and pushing forward along f is pushing forward along f and capping with the class.