Cup products of cochains along a diagonal

Let C be a k-linear preadditive monoidal category, let A, B and E be chain complexes in C indexed by ℕ such that the tensor product A ⊗ B exists, and let D : E ⟶ A ⊗ B be a chain map, a diagonal. Given a pairing μ : M ⊗ N ⟶ P of coefficient objects, a cochain φ : A_p ⟶ M and a cochain ψ : B_q ⟶ N have the cup product φ ⌣ ψ : E_n ⟶ P, for p + q = n: the degree-n component of D, followed by the projection of (A ⊗ B)_n onto its summand A_p ⊗ B_q, by φ ⊗ ψ and by μ. Since D is a chain map and the tensor product carries the Koszul signs, it satisfies the Leibniz rule (φ ⌣ ψ) ∘ d = (φ ∘ d) ⌣ ψ + (-1)^p φ ⌣ (ψ ∘ d). When C is moreover abelian, a cocycle cupped with a cocycle is a cocycle, a coboundary cupped with a cocycle (in either order) is a coboundary, and the cup product descends to a k-bilinear map Hᵖ(Hom(A, M)) × H^q(Hom(B, N)) ⟶ Hⁿ(Hom(E, P)) on the cohomology of the complexes ChainComplex.linearYonedaObj. It is natural along maps of diagonals.

The singular cup product is the case where D is the Alexander–Whitney map precomposed with the diagonal of a space; there φ ⌣ ψ evaluates a singular simplex on its front p-face and its back q-face.

Main definitions and results

• TauCeti.ChainComplex.cupCochain: the cup product of cochains.
• TauCeti.ChainComplex.d_comp_cupCochain: the Leibniz rule.
• TauCeti.ChainComplex.cupCochain_naturality: naturality along a map of diagonals.
• TauCeti.ChainComplex.cupCycles: the cup product of cocycles.
• TauCeti.ChainComplex.cup: the cup product on cohomology, with TauCeti.ChainComplex.cup_homologyπ computing it on classes of cocycles and TauCeti.ChainComplex.cup_naturality its naturality.

References

• A. Hatcher, Algebraic Topology, Section 3.2, Lemma 3.6.

noncomputable def TauCeti.ChainComplex.cupCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (k : Type u_2) [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) : p + q = n → (A.X p ⟶ M) →ₗ[k] (B.X q ⟶ N) →ₗ[k] E.X n ⟶ P

The cup product of cochains along the diagonal D : E ⟶ A ⊗ B: for p + q = n, the k-bilinear map sending cochains φ : A_p ⟶ M and ψ : B_q ⟶ N to the cochain E_n ⟶ (A ⊗ B)_n ⟶ P, the component of D followed by the tensor product of cochains TauCeti.ChainComplex.tensorCochain, which projects to A_p ⊗ B_q and applies φ ⊗ ψ and μ.

Equations

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

@[simp]

theorem TauCeti.ChainComplex.cupCochain_apply {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) : ((cupCochain k D μ p q n h) φ) ψ = CategoryTheory.CategoryStruct.comp (D.f n) (tensorCochain μ φ ψ n)

The cup product of cochains is the component of the diagonal followed by the tensor product of cochains.

theorem TauCeti.ChainComplex.d_comp_cupCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) : CategoryTheory.CategoryStruct.comp (E.d (n + 1) n) (((cupCochain k D μ p q n h) φ) ψ) = ((cupCochain k D μ (p + 1) q (n + 1) ⋯) (CategoryTheory.CategoryStruct.comp (A.d (p + 1) p) φ)) ψ + (-1) ^ p • ((cupCochain k D μ p (q + 1) (n + 1) ⋯) φ) (CategoryTheory.CategoryStruct.comp (B.d (q + 1) q) ψ)

The Leibniz rule for the cup product: (φ ⌣ ψ) ∘ d = (φ ∘ d) ⌣ ψ + (-1)^p φ ⌣ (ψ ∘ d) for a cochain φ of degree p.

theorem TauCeti.ChainComplex.cupCochain_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {A' B' E' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B'] (D' : E' ⟶ HomologicalComplex.tensorObj A' B') (e : E' ⟶ E) (f : A' ⟶ A) (g : B' ⟶ B) (hD : CategoryTheory.CategoryStruct.comp e D = CategoryTheory.CategoryStruct.comp D' (HomologicalComplex.tensorHom f g)) (p q n : ℕ) (h : p + q = n) (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) : ((cupCochain k D' μ p q n h) (CategoryTheory.CategoryStruct.comp (f.f p) φ)) (CategoryTheory.CategoryStruct.comp (g.f q) ψ) = CategoryTheory.CategoryStruct.comp (e.f n) (((cupCochain k D μ p q n h) φ) ψ)

Naturality of the cup product of cochains along a map of diagonals: if chain maps e : E' ⟶ E, f : A' ⟶ A and g : B' ⟶ B satisfy e ≫ D = D' ≫ (f ⊗ g), then cupping the pulled-back cochains along D' is pulling back their cup product along D.

noncomputable def TauCeti.ChainComplex.cupCycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (k : Type u_2) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p) →ₗ[k] ↑(HomologicalComplex.cycles (B.linearYonedaObj k N) q) →ₗ[k] ↑(HomologicalComplex.cycles (E.linearYonedaObj k P) n)

The cup product of cocycles: the cup product TauCeti.ChainComplex.cupCochain of the underlying cochains, which is a cocycle by the Leibniz rule (TauCeti.ChainComplex.iCycles_cupCycles).

Equations

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

@[simp]

theorem TauCeti.ChainComplex.iCycles_cupCycles {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p)) (b : ↑(HomologicalComplex.cycles (B.linearYonedaObj k N) q)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (E.linearYonedaObj k P) n)) (((cupCycles k D μ p q n h) a) b) = ((cupCochain k D μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (A.linearYonedaObj k M) p)) a)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (B.linearYonedaObj k N) q)) b)

On underlying cochains, the cup product of cocycles is the cup product of cochains.

noncomputable def TauCeti.ChainComplex.cup {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (k : Type u_2) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p) →ₗ[k] ↑(HomologicalComplex.homology (B.linearYonedaObj k N) q) →ₗ[k] ↑(HomologicalComplex.homology (E.linearYonedaObj k P) n)

The cup product on cohomology, Hᵖ(Hom(A, M)) × H^q(Hom(B, N)) ⟶ Hⁿ(Hom(E, P)) for p + q = n, along the diagonal D : E ⟶ A ⊗ B and the pairing μ : M ⊗ N ⟶ P: the class of a ⌣ b on the classes of cocycles a and b (TauCeti.ChainComplex.cup_homologyπ).

Equations

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

@[simp]

theorem TauCeti.ChainComplex.cup_homologyπ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(HomologicalComplex.cycles (A.linearYonedaObj k M) p)) (b : ↑(HomologicalComplex.cycles (B.linearYonedaObj k N) q)) : ((cup k D μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (A.linearYonedaObj k M) p)) a)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (B.linearYonedaObj k N) q)) b) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (E.linearYonedaObj k P) n)) (((cupCycles k D μ p q n h) a) b)

The cup product on classes: the cup product of the classes of two cocycles is the class of their cup product.

theorem TauCeti.ChainComplex.cup_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {A' B' E' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B'] (D' : E' ⟶ HomologicalComplex.tensorObj A' B') (e : E' ⟶ E) (f : A' ⟶ A) (g : B' ⟶ B) (hD : CategoryTheory.CategoryStruct.comp e D = CategoryTheory.CategoryStruct.comp D' (HomologicalComplex.tensorHom f g)) (p q n : ℕ) (h : p + q = n) (α : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p)) (β : ↑(HomologicalComplex.homology (B.linearYonedaObj k N) q)) : ((cup k D' μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k M).map f.op) p)) α)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k N).map g.op) q)) β) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k P).map e.op) n)) (((cup k D μ p q n h) α) β)

Naturality of the cup product on cohomology along a map of diagonals: if chain maps e : E' ⟶ E, f : A' ⟶ A and g : B' ⟶ B satisfy e ≫ D = D' ≫ (f ⊗ g), then the cup product along D' of the pulled-back classes is the pull-back of the cup product along D.

theorem TauCeti.ChainComplex.cup_precomp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {E' : ChainComplex C ℕ} (e : E' ⟶ E) (p q n : ℕ) (h : p + q = n) (a : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p)) (b : ↑(HomologicalComplex.homology (B.linearYonedaObj k N) q)) : ((cup k (CategoryTheory.CategoryStruct.comp e D) μ p q n h) a) b = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((linearYonedaFunctor k P).map e.op) n)) (((cup k D μ p q n h) a) b)

Precomposing a diagonal with a chain map pulls back its cup product on cohomology.

theorem TauCeti.ChainComplex.cup_eq_of_homotopy {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B E : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} {k : Type u_2} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (D : E ⟶ HomologicalComplex.tensorObj A B) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {D' : E ⟶ HomologicalComplex.tensorObj A B} (H : Homotopy D D') (p q n : ℕ) (h : p + q = n) (a : ↑(HomologicalComplex.homology (A.linearYonedaObj k M) p)) (b : ↑(HomologicalComplex.homology (B.linearYonedaObj k N) q)) : ((cup k D μ p q n h) a) b = ((cup k D' μ p q n h) a) b

Chain-homotopic diagonals give the same cup product on cohomology.