The tensor product of cochains

Let C be a preadditive monoidal category, let A and B be chain complexes in C indexed by ℕ such that the tensor product A ⊗ B exists, and let μ : M ⊗ N ⟶ P be a pairing of coefficient objects. Cochains φ : A_p ⟶ M and ψ : B_q ⟶ N have a tensor product (A ⊗ B)_n ⟶ P, which on the summand A_p ⊗ B_q is φ ⊗ ψ followed by μ and vanishes on every other summand. Since the differential of A ⊗ B carries the Koszul signs, it satisfies the Leibniz rule (φ ⊗ ψ) ∘ d = (φ ∘ d) ⊗ ψ + (-1)^p φ ⊗ (ψ ∘ d).

This is the common chain-level ingredient of the cup product of cochains (TauCeti.ChainComplex.cupCochain) and of the cap product of chains and cochains (TauCeti.ChainComplex.capChain), both of which precompose it with a diagonal E ⟶ A ⊗ B.

Main definitions and results

• TauCeti.ChainComplex.tensorCochain: the morphism (A ⊗ B)_n ⟶ P given on the summand A_p ⊗ B_q by φ ⊗ ψ and μ.
• TauCeti.ChainComplex.d_comp_tensorCochain: its Leibniz rule.
• TauCeti.ChainComplex.tensorHom_f_comp_tensorCochain: its naturality in the complexes.
• TauCeti.ChainComplex.tensorCochain_comp, TauCeti.ChainComplex.tensorCochain_whiskerLeft_comp and TauCeti.ChainComplex.tensorCochain_whiskerRight_comp: changing the pairing.

noncomputable def TauCeti.ChainComplex.tensorCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : (HomologicalComplex.tensorObj A B).X n ⟶ P

The tensor product of cochains: for cochains φ : A_p ⟶ M and ψ : B_q ⟶ N, the morphism (A ⊗ B)_n ⟶ P which on the summand A_p ⊗ B_q is φ ⊗ ψ followed by the pairing μ (TauCeti.ChainComplex.ιTensorObj_tensorCochain) and vanishes on every other summand (TauCeti.ChainComplex.ιTensorObj_tensorCochain_of_ne_left and TauCeti.ChainComplex.ιTensorObj_tensorCochain_of_ne_right).

Equations

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

@[simp]

theorem TauCeti.ChainComplex.ιTensorObj_tensorCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) (h : p + q = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B p q n h) (tensorCochain μ φ ψ n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom φ ψ) μ

The tensor product of cochains φ : A_p ⟶ M and ψ : B_q ⟶ N is φ ⊗ ψ followed by μ on the summand A_p ⊗ B_q.

@[simp]

theorem TauCeti.ChainComplex.ιTensorObj_tensorCochain_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) (h : p + q = n) {Z : C} (h✝ : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B p q n h) (CategoryTheory.CategoryStruct.comp (tensorCochain μ φ ψ n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom φ ψ) (CategoryTheory.CategoryStruct.comp μ h✝)

The tensor product of cochains φ : A_p ⟶ M and ψ : B_q ⟶ N is φ ⊗ ψ followed by μ on the summand A_p ⊗ B_q.

@[simp]

theorem TauCeti.ChainComplex.ιTensorObj_tensorCochain_of_ne_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) {i j n : ℕ} (h : i + j = n) (hi : i ≠ p) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B i j n h) (tensorCochain μ φ ψ n) = 0

The tensor product of cochains φ : A_p ⟶ M and ψ : B_q ⟶ N vanishes on the summands A_i ⊗ B_j with i ≠ p.

@[simp]

theorem TauCeti.ChainComplex.ιTensorObj_tensorCochain_of_ne_left_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) {i j n : ℕ} (h : i + j = n) (hi : i ≠ p) {Z : C} (h✝ : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B i j n h) (CategoryTheory.CategoryStruct.comp (tensorCochain μ φ ψ n) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The tensor product of cochains φ : A_p ⟶ M and ψ : B_q ⟶ N vanishes on the summands A_i ⊗ B_j with i ≠ p.

@[simp]

theorem TauCeti.ChainComplex.ιTensorObj_tensorCochain_of_ne_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) {i j n : ℕ} (h : i + j = n) (hj : j ≠ q) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B i j n h) (tensorCochain μ φ ψ n) = 0

The tensor product of cochains φ : A_p ⟶ M and ψ : B_q ⟶ N vanishes on the summands A_i ⊗ B_j with j ≠ q.

@[simp]

theorem TauCeti.ChainComplex.ιTensorObj_tensorCochain_of_ne_right_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) {i j n : ℕ} (h : i + j = n) (hj : j ≠ q) {Z : C} (h✝ : P ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj A B i j n h) (CategoryTheory.CategoryStruct.comp (tensorCochain μ φ ψ n) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The tensor product of cochains φ : A_p ⟶ M and ψ : B_q ⟶ N vanishes on the summands A_i ⊗ B_j with j ≠ q.

theorem TauCeti.ChainComplex.d_comp_tensorCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.tensorObj A B).d (n + 1) n) (tensorCochain μ φ ψ n) = tensorCochain μ (CategoryTheory.CategoryStruct.comp (A.d (p + 1) p) φ) ψ (n + 1) + (-1) ^ p • tensorCochain μ φ (CategoryTheory.CategoryStruct.comp (B.d (q + 1) q) ψ) (n + 1)

The Leibniz rule for the tensor product of cochains: precomposed with the differential of A ⊗ B, the tensor product of φ and ψ is the tensor product of φ ∘ d and ψ plus (-1)^p times the tensor product of φ and ψ ∘ d.

theorem TauCeti.ChainComplex.tensorHom_f_comp_tensorCochain {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {A' B' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B'] (f : A' ⟶ A) (g : B' ⟶ B) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.tensorHom f g).f n) (tensorCochain μ φ ψ n) = tensorCochain μ (CategoryTheory.CategoryStruct.comp (f.f p) φ) (CategoryTheory.CategoryStruct.comp (g.f q) ψ) n

The tensor product of cochains is natural: precomposing it with the tensor product of chain maps f : A' ⟶ A and g : B' ⟶ B is the tensor product of the precomposed cochains.

theorem TauCeti.ChainComplex.tensorHom_f_comp_tensorCochain_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {A' B' : ChainComplex C ℕ} [HomologicalComplex.HasTensor A' B'] (f : A' ⟶ A) (g : B' ⟶ B) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) {Z : C} (h : P ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.tensorHom f g).f n) (CategoryTheory.CategoryStruct.comp (tensorCochain μ φ ψ n) h) = CategoryTheory.CategoryStruct.comp (tensorCochain μ (CategoryTheory.CategoryStruct.comp (f.f p) φ) (CategoryTheory.CategoryStruct.comp (g.f q) ψ) n) h

The tensor product of cochains is natural: precomposing it with the tensor product of chain maps f : A' ⟶ A and g : B' ⟶ B is the tensor product of the precomposed cochains.

theorem TauCeti.ChainComplex.tensorCochain_add_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ φ' : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : tensorCochain μ (φ + φ') ψ n = tensorCochain μ φ ψ n + tensorCochain μ φ' ψ n

The tensor product of cochains is additive in the first cochain.

theorem TauCeti.ChainComplex.tensorCochain_add_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ ψ' : B.X q ⟶ N) (n : ℕ) : tensorCochain μ φ (ψ + ψ') n = tensorCochain μ φ ψ n + tensorCochain μ φ ψ' n

The tensor product of cochains is additive in the second cochain.

theorem TauCeti.ChainComplex.tensorCochain_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {P' : C} (g : P ⟶ P') {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : CategoryTheory.CategoryStruct.comp (tensorCochain μ φ ψ n) g = tensorCochain (CategoryTheory.CategoryStruct.comp μ g) φ ψ n

Postcomposing the tensor product of cochains with g : P ⟶ P' is the tensor product of the same cochains along the pairing μ ≫ g.

theorem TauCeti.ChainComplex.tensorCochain_comp_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {P' : C} (g : P ⟶ P') {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) {Z : C} (h : P' ⟶ Z) : CategoryTheory.CategoryStruct.comp (tensorCochain μ φ ψ n) (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (tensorCochain (CategoryTheory.CategoryStruct.comp μ g) φ ψ n) h

Postcomposing the tensor product of cochains with g : P ⟶ P' is the tensor product of the same cochains along the pairing μ ≫ g.

theorem TauCeti.ChainComplex.tensorCochain_whiskerLeft_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P N' : C} (g : N ⟶ N') (μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M N' ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : tensorCochain (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g) μ') φ ψ n = tensorCochain μ' φ (CategoryTheory.CategoryStruct.comp ψ g) n

The tensor product of cochains along the pairing (M ◁ g) ≫ μ' is the tensor product along μ' with the second cochain postcomposed with g.

theorem TauCeti.ChainComplex.tensorCochain_whiskerRight_comp {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P M' : C} (g : M ⟶ M') (μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M' N ⟶ P) {p q : ℕ} (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : tensorCochain (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g N) μ') φ ψ n = tensorCochain μ' (CategoryTheory.CategoryStruct.comp φ g) ψ n

The tensor product of cochains along the pairing (g ▷ N) ≫ μ' is the tensor product along μ' with the first cochain postcomposed with g.

theorem TauCeti.ChainComplex.tensorCochain_smul_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {k : Type u_2} [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {p q : ℕ} (r : k) (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : tensorCochain μ (r • φ) ψ n = r • tensorCochain μ φ ψ n

The tensor product of cochains is k-linear in the first cochain.

theorem TauCeti.ChainComplex.tensorCochain_smul_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {A B : ChainComplex C ℕ} [HomologicalComplex.HasTensor A B] {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) {k : Type u_2} [Semiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {p q : ℕ} (r : k) (φ : A.X p ⟶ M) (ψ : B.X q ⟶ N) (n : ℕ) : tensorCochain μ φ (r • ψ) n = r • tensorCochain μ φ ψ n

The tensor product of cochains is k-linear in the second cochain.