The Künneth map and the interchange of factors

For nonnegative chain complexes K and L in a braided preadditive monoidal category, the Koszul interchange K ⊗ L ⟶ L ⊗ K (TauCeti.NatChainComplex.koszulBraidingHom) sends the tensor product x ⊗ y of cycles of degrees p and q to (-1)^(p * q) • y ⊗ x. So on homology it sends the cross product x × y to (-1)^(p * q) • y × x (TauCeti.NatChainComplex.homologyCross_comp_homologyMap_koszulBraidingHom).

In a braided category, the signed interchange of the summands Hₚ(K) ⊗ H_q(L) is an isomorphism of the sources of the Künneth maps, so the Künneth map of K and L is an isomorphism exactly when that of L and K is (TauCeti.NatChainComplex.isIso_homologyKunneth_comm). In particular the Künneth theorem for a factor with zero differentials and flat terms holds with that factor on either side (HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat_right). With the factor on the right, it computes the homology of K ⊗ Z(L) for the complex of cycles Z(L), as the Künneth short exact sequence requires (HomologicalComplex.homologyKunnethShortComplex_shortExact).

Main results

• TauCeti.NatChainComplex.cyclesCross_comp_cyclesMap_koszulBraidingHom and TauCeti.NatChainComplex.homologyCross_comp_homologyMap_koszulBraidingHom: interchange on tensor products of cycles and on cross products.
• TauCeti.NatChainComplex.isIso_homologyKunneth_comm: symmetry of the Künneth theorem.
• HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat_right: the Künneth theorem when the second complex of modules has zero differentials and flat terms.

References

• C. Weibel, An Introduction to Homological Algebra, Section 3.6, the Künneth formula.

theorem TauCeti.NatChainComplex.cyclesCross_comp_cyclesMap_koszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K L : ChainComplex C ℕ) [HomologicalComplex.HasTensor K L] [HomologicalComplex.HasTensor L K] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : p + q = n) [HomologicalComplex.HasHomology K p] [HomologicalComplex.HasHomology L q] [(HomologicalComplex.tensorObj K L).HasHomology n] [(HomologicalComplex.tensorObj L K).HasHomology n] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesCross K L p q n h) (HomologicalComplex.cyclesMap (koszulBraidingHom K L) n) = (-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (HomologicalComplex.cycles K p) (HomologicalComplex.cycles L q)).hom (HomologicalComplex.cyclesCross L K q p n ⋯)

Koszul interchange sends the tensor product of cycles x ⊗ y to (-1)^(p*q) • y ⊗ x.

theorem TauCeti.NatChainComplex.cyclesCross_comp_cyclesMap_koszulBraidingHom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K L : ChainComplex C ℕ) [HomologicalComplex.HasTensor K L] [HomologicalComplex.HasTensor L K] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : p + q = n) [HomologicalComplex.HasHomology K p] [HomologicalComplex.HasHomology L q] [(HomologicalComplex.tensorObj K L).HasHomology n] [(HomologicalComplex.tensorObj L K).HasHomology n] {Z : C} (h✝ : (HomologicalComplex.tensorObj L K).cycles n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesCross K L p q n h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (koszulBraidingHom K L) n) h✝) = CategoryTheory.CategoryStruct.comp ((-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (HomologicalComplex.cycles K p) (HomologicalComplex.cycles L q)).hom (HomologicalComplex.cyclesCross L K q p n ⋯)) h✝

Koszul interchange sends the tensor product of cycles x ⊗ y to (-1)^(p*q) • y ⊗ x.

theorem TauCeti.NatChainComplex.homologyCross_comp_homologyMap_koszulBraidingHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K L : ChainComplex C ℕ) [HomologicalComplex.HasTensor K L] [HomologicalComplex.HasTensor L K] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : p + q = n) [HomologicalComplex.HasHomology K p] [HomologicalComplex.HasHomology L q] [(HomologicalComplex.tensorObj K L).HasHomology n] [(HomologicalComplex.tensorObj L K).HasHomology n] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology K p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles L q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (L.X ((ComplexShape.down ℕ).prev q)))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology L q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles K p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (K.X ((ComplexShape.down ℕ).prev p)))] : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyCross K L p q n h) (HomologicalComplex.homologyMap (koszulBraidingHom K L) n) = (-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (HomologicalComplex.homology K p) (HomologicalComplex.homology L q)).hom (HomologicalComplex.homologyCross L K q p n ⋯)

Koszul interchange on homology: the cross product x × y is sent to (-1)^(p*q) • y × x.

theorem TauCeti.NatChainComplex.homologyCross_comp_homologyMap_koszulBraidingHom_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K L : ChainComplex C ℕ) [HomologicalComplex.HasTensor K L] [HomologicalComplex.HasTensor L K] [CategoryTheory.BraidedCategory C] (p q n : ℕ) (h : p + q = n) [HomologicalComplex.HasHomology K p] [HomologicalComplex.HasHomology L q] [(HomologicalComplex.tensorObj K L).HasHomology n] [(HomologicalComplex.tensorObj L K).HasHomology n] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology K p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles L q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (L.X ((ComplexShape.down ℕ).prev q)))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology L q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles K p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (K.X ((ComplexShape.down ℕ).prev p)))] {Z : C} (h✝ : (HomologicalComplex.tensorObj L K).homology n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyCross K L p q n h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (koszulBraidingHom K L) n) h✝) = CategoryTheory.CategoryStruct.comp ((-1) ^ (p * q) • CategoryTheory.CategoryStruct.comp (β_ (HomologicalComplex.homology K p) (HomologicalComplex.homology L q)).hom (HomologicalComplex.homologyCross L K q p n ⋯)) h✝

Koszul interchange on homology: the cross product x × y is sent to (-1)^(p*q) • y × x.

theorem TauCeti.NatChainComplex.isIso_homologyKunneth_comm {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (K L : ChainComplex C ℕ) [HomologicalComplex.HasTensor K L] [HomologicalComplex.HasTensor L K] [CategoryTheory.BraidedCategory C] (n : ℕ) [∀ (p : ℕ), HomologicalComplex.HasHomology K p] [∀ (q : ℕ), HomologicalComplex.HasHomology L q] [(HomologicalComplex.tensorObj K L).HasHomology n] [(HomologicalComplex.tensorObj L K).HasHomology n] [∀ (p : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology K p))] [∀ (q : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles L q))] [∀ (q : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (L.X ((ComplexShape.down ℕ).prev q)))] [∀ (q : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology L q))] [∀ (p : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles K p))] [∀ (p : ℕ), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (K.X ((ComplexShape.down ℕ).prev p)))] [CategoryTheory.GradedObject.HasTensor (fun (p : ℕ) => HomologicalComplex.homology K p) fun (q : ℕ) => HomologicalComplex.homology L q] [CategoryTheory.GradedObject.HasTensor (fun (q : ℕ) => HomologicalComplex.homology L q) fun (p : ℕ) => HomologicalComplex.homology K p] : CategoryTheory.IsIso (HomologicalComplex.homologyKunneth K L n) ↔ CategoryTheory.IsIso (HomologicalComplex.homologyKunneth L K n)

The Künneth map is symmetric: in a braided category, the Künneth map of K and L is an isomorphism exactly when that of L and K is, since Koszul interchange identifies them.

theorem HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat_right {R : Type u} [CommRing R] (K L : ChainComplex (ModuleCat R) ℕ) [∀ (q : ℕ), Module.Flat R ↑(L.X q)] (hL : ∀ (i j : ℕ), L.d i j = 0) (n : ℕ) : CategoryTheory.IsIso (homologyKunneth K L n)

The Künneth theorem when the second factor has zero differentials and flat terms: if L is a complex of flat modules with zero differentials, so that H_q(L) = L_q, then for every complex K the Künneth map ⨁_{p + q = n} Hₚ(K) ⊗ H_q(L) ⟶ Hₙ(K ⊗ L) is an isomorphism. This is HomologicalComplex.isIso_homologyKunneth_of_d_eq_zero_of_flat with the factors interchanged.