The Alexander–Whitney map on singular chains

For topological spaces X and Y, TopCat.alexanderWhitney X Y R S is the Alexander–Whitney chain map from the singular chains of X × Y with coefficients in R ⊗ S to the tensor product of the singular chains of X and of Y. A singular simplex σ of X × Y is sent to ∑_{p + q = n} (pr₁ ∘ σ)|[0, …, p] ⊗ (pr₂ ∘ σ)|[p, …, n]: it is the simplicial Alexander–Whitney map SSet.alexanderWhitney precomposed with the map Sing(X × Y) ⟶ Sing X × Sing Y induced by the two projections (CartesianMonoidalCategory.prodComparison). It is natural in both spaces.

For a single space X and a coefficient morphism u : T ⟶ R ⊗ S, the Alexander–Whitney diagonal X.alexanderWhitneyDiagonal u : C(X; T) ⟶ C(X; R) ⊗ C(X; S) is u, followed by the chain map induced by the diagonal X ⟶ X × X and by TopCat.alexanderWhitney X X R S. It sends a singular simplex σ to ∑_{p + q = n} σ|[0, …, p] ⊗ σ|[p, …, n], and is natural in X. Cup products of singular cochains and cap products of singular chains with singular cochains are taken along it.

Main definitions and results

• TopCat.alexanderWhitney: the Alexander–Whitney map on singular chains.
• TopCat.alexanderWhitney_def: its factorization through the product of singular simplicial sets.
• TopCat.ιChainComplex_alexanderWhitney_f: its value on a singular simplex.
• TopCat.alexanderWhitney_naturality: it is natural in both spaces.
• TopCat.alexanderWhitney_coefficient_naturality: it is natural in both coefficient objects.
• TopCat.alexanderWhitneyDiagonal: the Alexander–Whitney diagonal of a space, with TopCat.ιChainComplex_alexanderWhitneyDiagonal_f its value on a singular simplex and TopCat.alexanderWhitneyDiagonal_naturality its naturality.
• TopCat.ιChainComplex_alexanderWhitneyDiagonal_f_tensorCochain: the tensor product of two cochains, precomposed with the Alexander–Whitney diagonal, on a singular simplex.

References

• A. Hatcher, Algebraic Topology, Section 3.2, for the front and back faces of a singular simplex.

noncomputable def TopCat.alexanderWhitney {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] (X Y : TopCat) (R S : C) : (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S)

The Alexander–Whitney map C(X × Y; R ⊗ S) ⟶ C(X; R) ⊗ C(Y; S) on singular chains: the simplicial Alexander–Whitney map of Sing X and Sing Y, precomposed with the comparison map Sing(X × Y) ⟶ Sing X × Sing Y induced by the two projections of X × Y.

Equations

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

theorem TopCat.alexanderWhitney_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] (X Y : TopCat) (R S : C) : X.alexanderWhitney Y R S = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (CategoryTheory.CartesianMonoidalCategory.prodComparison toSSet X Y) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) ((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S)

The singular Alexander--Whitney map is the map induced by the two projections, followed by the simplicial Alexander--Whitney map on the resulting product of singular simplicial sets.

@[simp]

theorem TopCat.ιChainComplex_alexanderWhitney_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {X Y : TopCat} (R S : C) {n : ℕ} (σ : (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).ιChainComplex σ) ((X.alexanderWhitney Y R S).f n) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj (toSSet.obj X) (toSSet.obj Y)).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).app (Opposite.op { len := n }))) σ, (CategoryTheory.ConcreteCategory.hom ((toSSet.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).app (Opposite.op { len := n }))) σ)) (((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S).f n)

The Alexander–Whitney map on the summand of a singular simplex σ of X × Y is the simplicial Alexander–Whitney map on the pair of its projections to X and Y.

@[simp]

theorem TopCat.ιChainComplex_alexanderWhitney_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {X Y : TopCat} (R S : C) {n : ℕ} (σ : (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).obj (Opposite.op { len := n })) {Z : C} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((X.alexanderWhitney Y R S).f n) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj (toSSet.obj X) (toSSet.obj Y)).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)).app (Opposite.op { len := n }))) σ, (CategoryTheory.ConcreteCategory.hom ((toSSet.map (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).app (Opposite.op { len := n }))) σ)) (CategoryTheory.CategoryStruct.comp (((toSSet.obj X).alexanderWhitney (toSSet.obj Y) R S).f n) h)

The Alexander–Whitney map on the summand of a singular simplex σ of X × Y is the simplicial Alexander–Whitney map on the pair of its projections to X and Y.

theorem TopCat.alexanderWhitney_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S : C) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (toSSet.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (X'.alexanderWhitney Y' R S) = CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (toSSet.map f) R) (SSet.chainComplexMap (toSSet.map g) S))

The Alexander–Whitney map on singular chains is natural in both spaces.

theorem TopCat.alexanderWhitney_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {X Y X' Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (R S : C) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X').chainComplex R) ((toSSet.obj Y').chainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (toSSet.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (CategoryTheory.CategoryStruct.comp (X'.alexanderWhitney Y' R S) h) = CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (toSSet.map f) R) (SSet.chainComplexMap (toSSet.map g) S)) h)

The Alexander–Whitney map on singular chains is natural in both spaces.

theorem TopCat.alexanderWhitney_coefficient_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] (X Y : TopCat) {R S R' S' : C} (f : R ⟶ R') (g : S ⟶ S') : CategoryTheory.CategoryStruct.comp (((SSet.chainComplexFunctor C).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))) (X.alexanderWhitney Y R' S') = CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (CategoryTheory.MonoidalCategoryStruct.tensorHom (((SSet.chainComplexFunctor C).map f).app (toSSet.obj X)) (((SSet.chainComplexFunctor C).map g).app (toSSet.obj Y)))

The Alexander–Whitney map on singular chains is natural in both coefficient objects.

theorem TopCat.alexanderWhitney_coefficient_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] (X Y : TopCat) {R S R' S' : C} (f : R ⟶ R') (g : S ⟶ S') {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R') ((toSSet.obj Y).chainComplex S') ⟶ Z) : CategoryTheory.CategoryStruct.comp (((SSet.chainComplexFunctor C).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).app (toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))) (CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R' S') h) = CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((SSet.chainComplexFunctor C).map f).app (toSSet.obj X)) (((SSet.chainComplexFunctor C).map g).app (toSSet.obj Y))) h)

The Alexander–Whitney map on singular chains is natural in both coefficient objects.

noncomputable def TopCat.alexanderWhitneyDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {R S T : C} (X : TopCat) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : (toSSet.obj X).chainComplex T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj X).chainComplex S)

The Alexander–Whitney diagonal C(X; T) ⟶ C(X; R) ⊗ C(X; S) of a space X: the coefficient morphism u : T ⟶ R ⊗ S, followed by the chain map induced by the diagonal X ⟶ X × X and by the Alexander–Whitney map TopCat.alexanderWhitney X X R S.

Equations

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

@[simp]

theorem TopCat.ιChainComplex_alexanderWhitneyDiagonal_f {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {R S T : C} (X : TopCat) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {n : ℕ} (σ : (toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex σ) ((X.alexanderWhitneyDiagonal u).f n) = CategoryTheory.CategoryStruct.comp u (∑ p : Fin (n + 1), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval 0 ↑p ⋯).op)) σ)) ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval (↑p) (n - ↑p) ⋯).op)) σ))) (HomologicalComplex.ιTensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj X).chainComplex S) (↑p) (n - ↑p) n ⋯))

The Alexander–Whitney diagonal sends a singular n-simplex σ to ∑_{p + q = n} σ|[0, …, p] ⊗ σ|[p, …, n], after the coefficient morphism u.

@[simp]

theorem TopCat.ιChainComplex_alexanderWhitneyDiagonal_f_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {R S T : C} (X : TopCat) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {n : ℕ} (σ : (toSSet.obj X).obj (Opposite.op { len := n })) {Z : C} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj X).chainComplex S)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((X.alexanderWhitneyDiagonal u).f n) h) = CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (∑ x : Fin (n + 1), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval 0 ↑x ⋯).op)) σ)) ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval (↑x) (n - ↑x) ⋯).op)) σ))) (HomologicalComplex.ιTensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj X).chainComplex S) (↑x) (n - ↑x) n ⋯)) h)

The Alexander–Whitney diagonal sends a singular n-simplex σ to ∑_{p + q = n} σ|[0, …, p] ⊗ σ|[p, …, n], after the coefficient morphism u.

theorem TopCat.ιChainComplex_alexanderWhitneyDiagonal_f_tensorCochain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {R S T : C} (X : TopCat) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {M N P : C} (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : ((toSSet.obj X).chainComplex R).X p ⟶ M) (ψ : ((toSSet.obj X).chainComplex S).X q ⟶ N) (σ : (toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((X.alexanderWhitneyDiagonal u).f n) (TauCeti.ChainComplex.tensorCochain μ φ ψ n)) = CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval 0 p ⋯).op)) σ)) φ) (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval p q ⋯).op)) σ)) ψ)) μ)

The tensor product of cochains φ of degree p and ψ of degree q (TauCeti.ChainComplex.tensorCochain), precomposed with the Alexander–Whitney diagonal, sends a singular (p + q)-simplex σ to φ of the front p-face of σ tensored with ψ of its back q-face, followed by μ, after the coefficient morphism u. This evaluates both the cup and the cap product of singular cochains on a simplex.

theorem TopCat.alexanderWhitneyDiagonal_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {R S T : C} {X Y : TopCat} (f : X ⟶ Y) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (toSSet.map f) T) (Y.alexanderWhitneyDiagonal u) = CategoryTheory.CategoryStruct.comp (X.alexanderWhitneyDiagonal u) (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (toSSet.map f) R) (SSet.chainComplexMap (toSSet.map f) S))

The Alexander–Whitney diagonal is natural in the space.

theorem TopCat.alexanderWhitneyDiagonal_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {R S T : C} {X Y : TopCat} (f : X ⟶ Y) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj Y).chainComplex R) ((toSSet.obj Y).chainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (toSSet.map f) T) (CategoryTheory.CategoryStruct.comp (Y.alexanderWhitneyDiagonal u) h) = CategoryTheory.CategoryStruct.comp (X.alexanderWhitneyDiagonal u) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (toSSet.map f) R) (SSet.chainComplexMap (toSSet.map f) S)) h)

The Alexander–Whitney diagonal is natural in the space.

theorem TauCeti.alexanderWhitneyDiagonal_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] {X : TopCat} {R S T : C} (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : X.alexanderWhitneyDiagonal u = CategoryTheory.CategoryStruct.comp (((SSet.chainComplexFunctor C).map u).app (TopCat.toSSet.obj X)) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))) (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (X.alexanderWhitney X R S))

The Alexander–Whitney diagonal factors through coefficient change and the diagonal of the space.