Cap products of chains and cochains along a diagonal

Let C be a k-linear preadditive monoidal category, let A, B, B' and E be chain complexes in C indexed by ℕ such that the tensor product A ⊗ B exists, let D : E ⟶ A ⊗ B be a chain map (a diagonal), and let a : M ⊗ B ⟶ B' be a chain map from the complex B tensored on the left by an object M (an action of the coefficient object M on B). A cochain φ : A_p ⟶ M then caps a chain of E of degree n = p + q to a chain of B' of degree q: the cap product E_n ⟶ B'_q is the degree-n component of D, followed by the projection of (A ⊗ B)_n onto its summand A_p ⊗ B_q, by φ ▷ B_q and by a. In terms of the tensor product of cochains TauCeti.ChainComplex.tensorCochain, it is D ≫ tensorCochain a φ (𝟙 B_q).

Since D and a are chain maps and the tensor product carries the Koszul signs, the cap product satisfies the boundary formula ∂(x ⌢ φ) = (-1)^p (∂x ⌢ φ - x ⌢ δφ), where δφ = φ ∘ ∂. When C is moreover abelian, capping with a cocycle sends cycles to cycles and boundaries to boundaries, capping with a coboundary is zero on homology, and the cap product descends to a k-linear map Hᵖ(Hom(A, M)) ⟶ (Hₙ(E) ⟶ H_q(B')) from the cohomology of ChainComplex.linearYonedaObj. It is natural along maps of diagonals and actions.

The singular cap product is the case where D is the Alexander–Whitney map precomposed with the diagonal of a space, and a lets a coefficient pairing act on singular chains; there x ⌢ φ evaluates φ on the front p-face of a singular simplex and keeps its back q-face.

Main definitions and results

• TauCeti.ChainComplex.capChain: the cap product of a chain and a cochain.
• TauCeti.ChainComplex.capChain_comp_d: the boundary formula.
• TauCeti.ChainComplex.capChain_naturality: naturality along maps of diagonals and actions.
• TauCeti.ChainComplex.capCycles: the cap product of a cycle and a cocycle.
• TauCeti.ChainComplex.cap: the cap product on homology, with TauCeti.ChainComplex.cap_homologyπ computing it on classes of cycles and cocycles and TauCeti.ChainComplex.cap_naturality its naturality.

References

• A. Hatcher, Algebraic Topology, Section 3.3, the cap product and its boundary formula.

noncomputable def TauCeti.ChainComplex.capChain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} (k : Type u_2) [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) : p + q = n → (A.X p ⟶ M) →ₗ[k] E.X n ⟶ B'.X q

The cap product of chains and cochains along the diagonal D : E ⟶ A ⊗ B and the action a : M ⊗ B ⟶ B': for p + q = n, the k-linear map sending a cochain φ : A_p ⟶ M to the morphism E_n ⟶ (A ⊗ B)_n ⟶ B'_q, the component of D followed by the projection onto the summand A_p ⊗ B_q, by φ ▷ B_q and by the component of a.

@[simp]

theorem TauCeti.ChainComplex.capChain_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) (φ : A.X p ⟶ M) : (capChain k D a p q n h) φ = CategoryTheory.CategoryStruct.comp (D.f n) (tensorCochain (a.f q) φ (CategoryTheory.CategoryStruct.id (B.X q)) n)

The cap product is the component of the diagonal followed by the tensor product of cochains of φ and the identity of B_q, along the action a.

theorem TauCeti.ChainComplex.capChain_comp_d {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) (φ : A.X p ⟶ M) : CategoryTheory.CategoryStruct.comp ((capChain k D a p (q + 1) (n + 1) ⋯) φ) (B'.d (q + 1) q) = (-1) ^ p • (CategoryTheory.CategoryStruct.comp (E.d (n + 1) n) ((capChain k D a p q n h) φ) - (capChain k D a (p + 1) q (n + 1) ⋯) (CategoryTheory.CategoryStruct.comp (A.d (p + 1) p) φ))

The boundary formula for the cap product: ∂(x ⌢ φ) = (-1)^p (∂x ⌢ φ - x ⌢ (φ ∘ ∂)) for a cochain φ of degree p.

theorem TauCeti.ChainComplex.capChain_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') {A' B₁ B₁' E' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B₁] (D' : E' ⟶ HomologicalComplex.tensorObj A' B₁) (a' : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B₁ ⟶ B₁') (e : E' ⟶ E) (f : A' ⟶ A) (g : B₁ ⟶ B) (g' : B₁' ⟶ B') (hD : CategoryTheory.CategoryStruct.comp e D = CategoryTheory.CategoryStruct.comp D' (HomologicalComplex.tensorHom f g)) (ha : CategoryTheory.CategoryStruct.comp a' g' = CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).map g) a) (p q n : ℕ) (h : p + q = n) (φ : A.X p ⟶ M) : CategoryTheory.CategoryStruct.comp ((capChain k D' a' p q n h) (CategoryTheory.CategoryStruct.comp (f.f p) φ)) (g'.f q) = CategoryTheory.CategoryStruct.comp (e.f n) ((capChain k D a p q n h) φ)

Naturality of the cap product of chains and cochains along maps of diagonals and actions: if chain maps e : E' ⟶ E, f : A' ⟶ A, g : B₁ ⟶ B and g' : B₁' ⟶ B' satisfy e ≫ D = D' ≫ (f ⊗ g) and a' ≫ g' = (M ◁ g) ≫ a, then pushing forward along g' the cap product along D' and a' with the pulled-back cochain is the cap product along D and a of the pushed-forward chain.

noncomputable def TauCeti.ChainComplex.capCycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} (k : Type u_2) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p) →ₗ[k] HomologicalComplex.cycles E n ⟶ HomologicalComplex.cycles B' q

The cap product of a cycle and a cocycle: capping with a cocycle of degree p sends the cycles of E of degree n = p + q to cycles of B' of degree q, by the boundary formula TauCeti.ChainComplex.capChain_comp_d; this is k-linear in the cocycle.

@[simp]

theorem TauCeti.ChainComplex.capCycles_i {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) (φ : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p)) : CategoryTheory.CategoryStruct.comp ((capCycles k D a p q n h) φ) (HomologicalComplex.iCycles B' q) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles E n) ((capChain k D a p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (A.linearYonedaObj k M) p)) φ))

On underlying chains, the cap product of a cycle and a cocycle is the cap product of the chain and the cochain.

@[simp]

theorem TauCeti.ChainComplex.capCycles_i_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) (φ : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p)) {Z : C} (h✝ : B'.X q ⟶ Z) : CategoryTheory.CategoryStruct.comp ((capCycles k D a p q n h) φ) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles B' q) h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles E n) (CategoryTheory.CategoryStruct.comp ((capChain k D a p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (A.linearYonedaObj k M) p)) φ)) h✝)

On underlying chains, the cap product of a cycle and a cocycle is the cap product of the chain and the cochain.

noncomputable def TauCeti.ChainComplex.cap {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} (k : Type u_2) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p) →ₗ[k] HomologicalComplex.homology E n ⟶ HomologicalComplex.homology B' q

The cap product on homology, Hᵖ(Hom(A, M)) ⟶ (Hₙ(E) ⟶ H_q(B')) for p + q = n, along the diagonal D : E ⟶ A ⊗ B and the action a : M ⊗ B ⟶ B': on the classes of a cocycle φ and a cycle x, the class of x ⌢ φ (TauCeti.ChainComplex.cap_homologyπ).

@[simp]

theorem TauCeti.ChainComplex.cap_homologyπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) (φ : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p)) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ E n) ((cap k D a p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (A.linearYonedaObj k M) p)) φ)) = CategoryTheory.CategoryStruct.comp ((capCycles k D a p q n h) φ) (HomologicalComplex.homologyπ B' q)

The cap product on classes: capping the class of a cycle with the class of a cocycle φ is the class of the cap product of the cycle with φ.

@[simp]

theorem TauCeti.ChainComplex.cap_homologyπ_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') (p q n : ℕ) (h : p + q = n) (φ : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p)) {Z : C} (h✝ : HomologicalComplex.homology B' q ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ E n) (CategoryTheory.CategoryStruct.comp ((cap k D a p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (A.linearYonedaObj k M) p)) φ)) h✝) = CategoryTheory.CategoryStruct.comp ((capCycles k D a p q n h) φ) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ B' q) h✝)

The cap product on classes: capping the class of a cycle with the class of a cocycle φ is the class of the cap product of the cycle with φ.

theorem TauCeti.ChainComplex.cap_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B B' E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M : C} {k : Type u_2} [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (a : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B ⟶ B') {A' B₁ B₁' E' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B₁] (D' : E' ⟶ HomologicalComplex.tensorObj A' B₁) (a' : ((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).obj B₁ ⟶ B₁') (e : E' ⟶ E) (f : A' ⟶ A) (g : B₁ ⟶ B) (g' : B₁' ⟶ B') (hD : CategoryTheory.CategoryStruct.comp e D = CategoryTheory.CategoryStruct.comp D' (HomologicalComplex.tensorHom f g)) (ha : CategoryTheory.CategoryStruct.comp a' g' = CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensorLeft M).mapHomologicalComplex (ComplexShape.down ℕ)).map g) a) (p q n : ℕ) (h : p + q = n) (α : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p)) : CategoryTheory.CategoryStruct.comp ((cap k D' a' p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k M).map f.op) p)) α)) (HomologicalComplex.homologyMap g' q) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap e n) ((cap k D a p q n h) α)

Naturality of the cap product on homology along maps of diagonals and actions: if chain maps e : E' ⟶ E, f : A' ⟶ A, g : B₁ ⟶ B and g' : B₁' ⟶ B' satisfy e ≫ D = D' ≫ (f ⊗ g) and a' ≫ g' = (M ◁ g) ≫ a, then capping with the pulled-back class and pushing forward along g' is pushing forward along e and capping with the class.