Cross products in singular cohomology

The external product sends classes on X and Y to a class on X × Y. It uses the Alexander–Whitney map with a coefficient pairing M ⊗ N ⟶ P, and is natural in both spaces. Pulling it back along the diagonal gives the cup product. Equivalently, the external product is the cup product of the pullbacks along the two projections.

The Eilenberg–Zilber isomorphism identifies cohomology of the product with cohomology of Hom(C(X; R) ⊗ C(Y; S), P). Under this isomorphism the external product is represented by the tensor product of cocycles. This comparison uses the shuffle–Alexander–Whitney chain homotopy; it does not assert a Künneth decomposition of cohomology.

References

• A. Hatcher, Algebraic Topology, Section 3.2, for cross products and the diagonal formula.
• S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953).

The construction uses TauCeti.ChainComplex.cup, and the comparison uses TopCat.eilenbergZilberHomotopyEquiv and TauCeti.HomotopyEquiv.linearYonedaFunctorMap.

noncomputable def TauCeti.singularCross {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y : TopCat) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) : ↑(TopCat.singularCohomology R k M X p) →ₗ[k] ↑(TopCat.singularCohomology S k N Y q) →ₗ[k] ↑(TopCat.singularCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) k P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n)

The bilinear external product in singular cohomology, induced by the Alexander–Whitney map and the coefficient pairing μ.

Equations

• TauCeti.singularCross k X Y μ p q n h = TauCeti.ChainComplex.cup k (X.alexanderWhitney Y R S) μ p q n h

theorem TauCeti.singularCross_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y : TopCat) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) : singularCross k X Y μ p q n h = ChainComplex.cup k (X.alexanderWhitney Y R S) μ p q n h

The external product is the cohomology cup product along Alexander–Whitney.

@[simp]

theorem TauCeti.singularCross_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y : TopCat) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(HomologicalComplex.cycles (TopCat.singularCochainComplex R k M X) p)) (b : ↑(HomologicalComplex.cycles (TopCat.singularCochainComplex S k N Y) q)) : ((singularCross k X Y μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M X) p)) a)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex S k N Y) q)) b) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) k P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) n)) (((ChainComplex.cupCycles k (X.alexanderWhitney Y R S) μ p q n h) a) b)

The external product of classes of cocycles is represented by their tensor cochain precomposed with the Alexander–Whitney map.

theorem TauCeti.singularCross_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(TopCat.singularCohomology R k M X' p)) (b : ↑(TopCat.singularCohomology S k N Y' q)) : ((singularCross k X Y μ p q n h) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f p)) a)) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap g q)) b) = (CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) n)) (((singularCross k X' Y' μ p q n h) a) b)

External products commute with pullback along a product of continuous maps.

theorem TauCeti.singularCross_diagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X : TopCat) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(TopCat.singularCohomology R k M X p)) (b : ↑(TopCat.singularCohomology S k N X q)) : (CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X)) n)) (((singularCross k X X μ p q n h) a) b) = ((X.singularCup k (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) μ p q n h) a) b

Pulling the external product back along the diagonal gives the cup product.

theorem TauCeti.singularCross_eq_singularCup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (X Y : TopCat) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(TopCat.singularCohomology R k M X p)) (b : ↑(TopCat.singularCohomology S k N Y q)) : ((singularCross k X Y μ p q n h) a) b = (((CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).singularCup k (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) μ p q n h) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) p)) a)) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) q)) b)

The external product is the cup product of pullbacks along the two projections.

noncomputable def TauCeti.singularEilenbergZilberCohomologyIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S P : C) (n : ℕ) : TopCat.singularCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) k P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n ≅ HomologicalComplex.homology (ChainComplex.linearYonedaObj (HomologicalComplex.tensorObj ((TopCat.toSSet.obj X).chainComplex R) ((TopCat.toSSet.obj Y).chainComplex S)) k P) n

The Eilenberg–Zilber isomorphism on cohomology with arbitrary target coefficients P. Its forward map is pullback along the shuffle map, and its inverse is pullback along Alexander–Whitney.

Equations

• TauCeti.singularEilenbergZilberCohomologyIso k X Y R S P n = (TauCeti.HomotopyEquiv.linearYonedaFunctorMap k P (X.eilenbergZilberHomotopyEquiv Y R S).symm).toHomologyIso n

@[simp]

theorem TauCeti.singularEilenbergZilberCohomologyIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S P : C) (n : ℕ) : (singularEilenbergZilberCohomologyIso k X Y R S P n).hom = HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k P).map (X.shuffle Y R S).op) n

The forward Eilenberg–Zilber comparison is induced by precomposition with the shuffle map.

@[simp]

theorem TauCeti.singularEilenbergZilberCohomologyIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S P : C) (n : ℕ) : (singularEilenbergZilberCohomologyIso k X Y R S P n).inv = HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k P).map (X.alexanderWhitney Y R S).op) n

The inverse Eilenberg–Zilber comparison is induced by precomposition with Alexander–Whitney.

theorem TauCeti.singularEilenbergZilberCohomologyIso_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S P : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) n) (singularEilenbergZilberCohomologyIso k X Y R S P n).hom = CategoryTheory.CategoryStruct.comp (singularEilenbergZilberCohomologyIso k X' Y' R S P n).hom (HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k P).map (HomologicalComplex.tensorHom (SSet.chainComplexMap (TopCat.toSSet.map f) R) (SSet.chainComplexMap (TopCat.toSSet.map g) S)).op) n)

The Eilenberg–Zilber comparison commutes with pullback along maps in both spaces.

theorem TauCeti.singularEilenbergZilberCohomologyIso_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S P : C) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology (ChainComplex.linearYonedaObj (HomologicalComplex.tensorObj ((TopCat.toSSet.obj X).chainComplex R) ((TopCat.toSSet.obj Y).chainComplex S)) k P) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) n) (CategoryTheory.CategoryStruct.comp (singularEilenbergZilberCohomologyIso k X Y R S P n).hom h) = CategoryTheory.CategoryStruct.comp (singularEilenbergZilberCohomologyIso k X' Y' R S P n).hom (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k P).map (HomologicalComplex.tensorHom (SSet.chainComplexMap (TopCat.toSSet.map f) R) (SSet.chainComplexMap (TopCat.toSSet.map g) S)).op) n) h)

The Eilenberg–Zilber comparison commutes with pullback along maps in both spaces.

theorem TauCeti.singularEilenbergZilberCohomologyIso_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S P : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularEilenbergZilberCohomologyIso k X' Y' R S P n).inv (TopCat.singularCohomologyMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k P).map (HomologicalComplex.tensorHom (SSet.chainComplexMap (TopCat.toSSet.map f) R) (SSet.chainComplexMap (TopCat.toSSet.map g) S)).op) n) (singularEilenbergZilberCohomologyIso k X Y R S P n).inv

The inverse Eilenberg–Zilber comparison commutes with pullback in both spaces.

theorem TauCeti.singularEilenbergZilberCohomologyIso_inv_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S P : C) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) k P (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularEilenbergZilberCohomologyIso k X' Y' R S P n).inv (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((ChainComplex.linearYonedaFunctor k P).map (HomologicalComplex.tensorHom (SSet.chainComplexMap (TopCat.toSSet.map f) R) (SSet.chainComplexMap (TopCat.toSSet.map g) S)).op) n) (CategoryTheory.CategoryStruct.comp (singularEilenbergZilberCohomologyIso k X Y R S P n).inv h)

The inverse Eilenberg–Zilber comparison commutes with pullback in both spaces.

theorem TauCeti.singularEilenbergZilberCohomologyIso_hom_singularCross {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) {R S M N P : C} [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(TopCat.singularCohomology R k M X p)) (b : ↑(TopCat.singularCohomology S k N Y q)) : (CategoryTheory.ConcreteCategory.hom (singularEilenbergZilberCohomologyIso k X Y R S P n).hom) (((singularCross k X Y μ p q n h) a) b) = ((ChainComplex.cup k (CategoryTheory.CategoryStruct.id (HomologicalComplex.tensorObj ((TopCat.toSSet.obj X).chainComplex R) ((TopCat.toSSet.obj Y).chainComplex S))) μ p q n h) a) b

Under Eilenberg–Zilber, the external product is the class of the tensor product of cocycles. Here the cup product along the identity is the product on the tensor chain complex itself.