Alexander–Whitney diagonals for relative cup products

The Alexander–Whitney diagonal C(X; T) ⟶ C(X; R) ⊗ C(X; S) of a space X sends a singular simplex σ to ∑_{p + q = n} σ|[0, …, p] ⊗ σ|[p, …, n]. If σ lies in a subspace, so do its front and back faces. This file records the two descents of the diagonal to relative chains along which relative cup products are taken.

• For a pair (X, A), the diagonal followed by the quotient map to relative chains on the second factor vanishes on the chains of A, and descends to TopPair.rightAlexanderWhitneyDiagonal : C(X, A; T) ⟶ C(X; R) ⊗ C(X, A; S). It gives the action Hᵖ(X) × H^q(X, A) ⟶ Hⁿ(X, A) of absolute cohomology on relative cohomology.
• For subsets U and V of X, the diagonal followed by the quotient maps on both factors vanishes on the chains of U and on those of V, hence on the chains C(U) + C(V) of the singular simplices of X lying in U or in V (the subcomplex X.smallSingularSubcomplex ![U, V]). It descends to TopCat.relativeAlexanderWhitneyDiagonal : C(X; U + V; T) ⟶ C(X, U; R) ⊗ C(X, V; S), where C(X; U + V) is the quotient of C(X) by C(U) + C(V). When U and V are open in U ∪ V, the small-chain theorem identifies C(X; U + V) with C(X, U ∪ V) up to quasi-isomorphism, which gives the relative cup product Hᵖ(X, U) × H^q(X, V) ⟶ Hⁿ(X, U ∪ V).

Main definitions and results

• TopPair.rightAlexanderWhitneyDiagonal, characterized by TopPair.singularChainComplexπ_rightAlexanderWhitneyDiagonal and natural in maps of pairs (TopPair.rightAlexanderWhitneyDiagonal_naturality).
• TopCat.relativeAlexanderWhitneyDiagonal, characterized by TopCat.chainComplexπ_relativeAlexanderWhitneyDiagonal and natural in maps of spaces carrying U into U' and V into V' (TopCat.relativeAlexanderWhitneyDiagonal_naturality, along the maps of pairs TopCat.smallSingularSubcomplexPairMap).

References

• A. Hatcher, Algebraic Topology, Section 3.2, the relative cup product Hᵏ(X, A) × Hˡ(X, B) ⟶ Hᵏ⁺ˡ(X, A ∪ B).

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

The right relative Alexander–Whitney diagonal C(X, A; T) ⟶ C(X; R) ⊗ C(X, A; S) of a pair (X, A): the Alexander–Whitney diagonal C(X; T) ⟶ C(X; R) ⊗ C(X; S) of X followed by the quotient map to relative chains on the second factor, which vanishes on the chains of A and so descends to relative chains.

@[simp]

theorem TopPair.singularChainComplexπ_rightAlexanderWhitneyDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} (P : TopPair) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : CategoryTheory.CategoryStruct.comp (P.singularChainComplexπ T) (P.rightAlexanderWhitneyDiagonal u) = CategoryTheory.CategoryStruct.comp (fst.alexanderWhitneyDiagonal u) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((TopCat.toSSet.obj fst).chainComplex R) (P.singularChainComplexπ S))

The right relative Alexander–Whitney diagonal of a pair (X, A) is the descent of the Alexander–Whitney diagonal of X, followed by the quotient map on the second factor.

@[simp]

theorem TopPair.singularChainComplexπ_rightAlexanderWhitneyDiagonal_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} (P : TopPair) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((TopCat.toSSet.obj fst).chainComplex R) (P.singularChainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.singularChainComplexπ T) (CategoryTheory.CategoryStruct.comp (P.rightAlexanderWhitneyDiagonal u) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (fst.alexanderWhitneyDiagonal u) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((TopCat.toSSet.obj fst).chainComplex R) (P.singularChainComplexπ S))) h

The right relative Alexander–Whitney diagonal of a pair (X, A) is the descent of the Alexander–Whitney diagonal of X, followed by the quotient map on the second factor.

theorem TopPair.rightAlexanderWhitneyDiagonal_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {P P' : TopPair} (f : P ⟶ P') (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : CategoryTheory.CategoryStruct.comp (singularChainComplexMap f T) (P'.rightAlexanderWhitneyDiagonal u) = CategoryTheory.CategoryStruct.comp (P.rightAlexanderWhitneyDiagonal u) (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (TopCat.toSSet.map (Hom.fst f)) R) (singularChainComplexMap f S))

The right relative Alexander–Whitney diagonal is natural in maps of pairs.

theorem TopPair.rightAlexanderWhitneyDiagonal_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {P P' : TopPair} (f : P ⟶ P') (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((TopCat.toSSet.obj fst).chainComplex R) (P'.singularChainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularChainComplexMap f T) (CategoryTheory.CategoryStruct.comp (P'.rightAlexanderWhitneyDiagonal u) h) = CategoryTheory.CategoryStruct.comp (P.rightAlexanderWhitneyDiagonal u) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (SSet.chainComplexMap (TopCat.toSSet.map (Hom.fst f)) R) (singularChainComplexMap f S)) h)

The right relative Alexander–Whitney diagonal is natural in maps of pairs.

noncomputable def TopCat.relativeAlexanderWhitneyDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {X : TopCat} (U V : Set ↑X) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : (X.smallSingularSubcomplex ![U, V]).pair.chainComplex T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj ((TopPair.ofSubset U).singularChainComplex R) ((TopPair.ofSubset V).singularChainComplex S)

The relative Alexander–Whitney diagonal C(X; U + V; T) ⟶ C(X, U; R) ⊗ C(X, V; S) for subsets U and V of X, where C(X; U + V) is the quotient of the singular chains of X by the chains of the singular simplices lying in U or in V: the Alexander–Whitney diagonal of X followed by the quotient maps on both factors, which vanishes on those chains and so descends.

@[simp]

theorem TopCat.chainComplexπ_relativeAlexanderWhitneyDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {X : TopCat} (U V : Set ↑X) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex ![U, V]).pair.chainComplexπ T) (relativeAlexanderWhitneyDiagonal U V u) = CategoryTheory.CategoryStruct.comp (X.alexanderWhitneyDiagonal u) (CategoryTheory.MonoidalCategoryStruct.tensorHom ((TopPair.ofSubset U).singularChainComplexπ R) ((TopPair.ofSubset V).singularChainComplexπ S))

The relative Alexander–Whitney diagonal is the descent of the Alexander–Whitney diagonal of X, followed by the quotient maps on both factors.

@[simp]

theorem TopCat.chainComplexπ_relativeAlexanderWhitneyDiagonal_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {X : TopCat} (U V : Set ↑X) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((TopPair.ofSubset U).singularChainComplex R) ((TopPair.ofSubset V).singularChainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex ![U, V]).pair.chainComplexπ T) (CategoryTheory.CategoryStruct.comp (relativeAlexanderWhitneyDiagonal U V u) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.alexanderWhitneyDiagonal u) (CategoryTheory.MonoidalCategoryStruct.tensorHom ((TopPair.ofSubset U).singularChainComplexπ R) ((TopPair.ofSubset V).singularChainComplexπ S))) h

The relative Alexander–Whitney diagonal is the descent of the Alexander–Whitney diagonal of X, followed by the quotient maps on both factors.

theorem TopCat.relativeAlexanderWhitneyDiagonal_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {X Y : TopCat} {U V : Set ↑X} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) : CategoryTheory.CategoryStruct.comp (SSetPair.chainComplexMap (smallSingularSubcomplexPairMap f hfU hfV) T) (relativeAlexanderWhitneyDiagonal U' V' u) = CategoryTheory.CategoryStruct.comp (relativeAlexanderWhitneyDiagonal U V u) (CategoryTheory.MonoidalCategoryStruct.tensorHom (TopPair.singularChainComplexMap (TopPair.ofSubsetMap f hfU) R) (TopPair.singularChainComplexMap (TopPair.ofSubsetMap f hfV) S))

The relative Alexander–Whitney diagonal is natural in maps f : X ⟶ Y carrying U into U' and V into V'.

theorem TopCat.relativeAlexanderWhitneyDiagonal_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T : C} {X Y : TopCat} {U V : Set ↑X} {U' V' : Set ↑Y} (f : X ⟶ Y) (hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U') (hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V') (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) {Z : ChainComplex C ℕ} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj ((TopPair.ofSubset U').singularChainComplex R) ((TopPair.ofSubset V').singularChainComplex S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSetPair.chainComplexMap (smallSingularSubcomplexPairMap f hfU hfV) T) (CategoryTheory.CategoryStruct.comp (relativeAlexanderWhitneyDiagonal U' V' u) h) = CategoryTheory.CategoryStruct.comp (relativeAlexanderWhitneyDiagonal U V u) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (TopPair.singularChainComplexMap (TopPair.ofSubsetMap f hfU) R) (TopPair.singularChainComplexMap (TopPair.ofSubsetMap f hfV) S)) h)

The relative Alexander–Whitney diagonal is natural in maps f : X ⟶ Y carrying U into U' and V into V'.