def ProductsInCohomology.frontFace (p q : ℕ) : SimplexCategory.mk p ⟶ SimplexCategory.mk (p + q)

The simplex-category morphism $[p] \hookrightarrow [p+q]$ that picks out the front $p$-face $\langle v_0, \ldots, v_p\rangle$ of the $(p+q)$-simplex.

def ProductsInCohomology.backFace (p q : ℕ) : SimplexCategory.mk q ⟶ SimplexCategory.mk (p + q)

The simplex-category morphism $[q] \hookrightarrow [p+q]$ that picks out the back $q$-face $\langle v_p, \ldots, v_{p+q}\rangle$ of the $(p+q)$-simplex.

noncomputable def ProductsInCohomology.frontFaceMap (p q : ℕ) : C(↑(stdSimplex ℝ (Fin (p + 1))), ↑(stdSimplex ℝ (Fin (p + q + 1))))

Continuous-map realisation of frontFace: the inclusion $\Delta^p \hookrightarrow \Delta^{p+q}$ of the front face on topological standard simplices.

noncomputable def ProductsInCohomology.backFaceMap (p q : ℕ) : C(↑(stdSimplex ℝ (Fin (q + 1))), ↑(stdSimplex ℝ (Fin (p + q + 1))))

Continuous-map realisation of backFace: the inclusion $\Delta^q \hookrightarrow \Delta^{p+q}$ of the back face on topological standard simplices.

noncomputable def ProductsInCohomology.frontProjection {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (p q : ℕ) (σ : C(↑(stdSimplex ℝ (Fin (p + q + 1))), X × Y)) : C(↑(stdSimplex ℝ (Fin (p + 1))), X)

Front projection of a $(p+q)$-simplex $\sigma$ of $X \times Y$: the $p$-simplex of $X$ obtained by restricting to the front face and projecting on the first factor. The "front" half of the Alexander-Whitney decomposition.

noncomputable def ProductsInCohomology.backProjection {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (p q : ℕ) (σ : C(↑(stdSimplex ℝ (Fin (p + q + 1))), X × Y)) : C(↑(stdSimplex ℝ (Fin (q + 1))), Y)

Back projection of a $(p+q)$-simplex $\sigma$ of $X \times Y$: the $q$-simplex of $Y$ obtained by restricting to the back face and projecting on the second factor. The "back" half of the Alexander-Whitney decomposition.

noncomputable def ProductsInCohomology.alexanderWhitneyMap {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (p q : ℕ) : FreeAbelianGroup C(↑(stdSimplex ℝ (Fin (p + q + 1))), X × Y) →+ TensorProduct ℤ (FreeAbelianGroup C(↑(stdSimplex ℝ (Fin (p + 1))), X)) (FreeAbelianGroup C(↑(stdSimplex ℝ (Fin (q + 1))), Y))

Construction 28.1 (Alexander-Whitney map). The natural chain map $\alpha : S_{p+q}(X \times Y) \to S_p(X) \otimes S_q(Y)$ sending a $(p+q)$-simplex $\sigma$ of $X \times Y$ to the tensor of its front $p$-projection and back $q$-projection.

noncomputable def ProductsInCohomology.cupProduct (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (SingularCohomology.singularCohomology R X (ModuleCat.of R R) p) (SingularCohomology.singularCohomology R X (ModuleCat.of R R) q) ⟶ SingularCohomology.singularCohomology R X (ModuleCat.of R R) (p + q)

Definition 28.2 (cup product). Alias for the SingularCohomology.cupProduct, the multiplicative structure $\smile : H^p(X; R) \otimes H^q(X; R) \to H^{p+q}(X; R)$ defined via pulling back the cohomology cross product along the diagonal.

noncomputable def ProductsInCohomology.cochainCrossProduct {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {R : Type u_3} [CommRing R] (p q : ℕ) (f : C(↑(stdSimplex ℝ (Fin (p + 1))), X) → R) (g : C(↑(stdSimplex ℝ (Fin (q + 1))), Y) → R) (σ : C(↑(stdSimplex ℝ (Fin (p + q + 1))), X × Y)) : R

The cochain-level cross product: given cochains $f$ on $X$ (degree $p$) and $g$ on $Y$ (degree $q$), produces the cochain on $X \times Y$ (degree $p+q$) sending a simplex $\sigma$ to $(-1)^{pq} f(\text{front}(\sigma)) \cdot g(\text{back}(\sigma))$.

def ProductsInCohomology.reassocSimplex {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] (n : ℕ) (σ : C(↑(stdSimplex ℝ (Fin (n + 1))), X × Y × Z)) : C(↑(stdSimplex ℝ (Fin (n + 1))), (X × Y) × Z)

Re-associate a simplex of $X \times Y \times Z$ to a simplex of $(X \times Y) \times Z$, by composing with the homeomorphism Homeomorph.prodAssoc. Used for comparing the two ways of bracketing a triple cup product.

noncomputable def ProductsInCohomology.castSimplex {W : Type u_4} [TopologicalSpace W] (n m : ℕ) (h : n = m) (σ : C(↑(stdSimplex ℝ (Fin (n + 1))), W)) : C(↑(stdSimplex ℝ (Fin (m + 1))), W)

Cast a simplex of dimension $n$ to dimension $m$ when $n = m$, by composing with the canonical simplex isomorphism induced by Fin.cast.

theorem ProductsInCohomology.frontProjection_frontProjection_reassoc {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] (p q r : ℕ) (σ : C(↑(stdSimplex ℝ (Fin (p + q + r + 1))), X × Y × Z)) : frontProjection p q (frontProjection (p + q) r (reassocSimplex (p + q + r) σ)) = frontProjection p (q + r) (castSimplex (p + q + r) (p + (q + r)) ⋯ σ)

Compatibility lemma: iterating front projections, first on a $(p+q)$-face then on a $p$-face, of the reassociated triple simplex equals one front projection at $(p, q+r)$ after a cast. A combinatorial identity used in cochainCrossProduct_assoc.

theorem ProductsInCohomology.backProjection_frontProjection_reassoc {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] (p q r : ℕ) (σ : C(↑(stdSimplex ℝ (Fin (p + q + r + 1))), X × Y × Z)) : backProjection p q (frontProjection (p + q) r (reassocSimplex (p + q + r) σ)) = frontProjection q r (backProjection p (q + r) (castSimplex (p + q + r) (p + (q + r)) ⋯ σ))

Compatibility lemma: composing back-then-front projections of the reassociated triple simplex equals front-of-back projections, after a cast. A combinatorial identity used in cochainCrossProduct_assoc.

theorem ProductsInCohomology.backProjection_reassoc {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] (p q r : ℕ) (σ : C(↑(stdSimplex ℝ (Fin (p + q + r + 1))), X × Y × Z)) : backProjection (p + q) r (reassocSimplex (p + q + r) σ) = backProjection q r (backProjection p (q + r) (castSimplex (p + q + r) (p + (q + r)) ⋯ σ))

Compatibility lemma: the back projection of the reassociated triple simplex factors through two back projections, after a cast. The third combinatorial identity used in cochainCrossProduct_assoc.

theorem ProductsInCohomology.cochainCrossProduct_assoc {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {Z : Type u_3} [TopologicalSpace Z] {R : Type u_4} [CommRing R] (p q r : ℕ) (f : C(↑(stdSimplex ℝ (Fin (p + 1))), X) → R) (g : C(↑(stdSimplex ℝ (Fin (q + 1))), Y) → R) (h : C(↑(stdSimplex ℝ (Fin (r + 1))), Z) → R) (σ : C(↑(stdSimplex ℝ (Fin (p + q + r + 1))), X × Y × Z)) : cochainCrossProduct (p + q) r (cochainCrossProduct p q f g) h (reassocSimplex (p + q + r) σ) = cochainCrossProduct p (q + r) f (cochainCrossProduct q r g h) (castSimplex (p + q + r) (p + (q + r)) ⋯ σ)

Proposition 28.3 (Associativity of the cochain cross product). The cochain-level cross product is associative up to the reassociation homeomorphism $X \times (Y \times Z) \cong (X \times Y) \times Z$: $(f \times g) \times h = f \times (g \times h)$ after suitable reassociation, and the sign $(-1)^{pq}$ cancels correctly. This is the combinatorial backbone of cup-product associativity.