Alexander–Whitney diagonal — combinatorial and simplex-level layer

This file develops the combinatorial and simplex-level groundwork for the Alexander–Whitney (AW) chain diagonal

Δ : C_•(X) → C_•(X) ⊗ C_•(X),

the chain-level ingredient underlying the singular cochain cup product. It uses the simplex category, standard face maps, the singular simplicial set TopCat.toSSet, the singular chain complex functor, and the monoidal structure supplied by CupProductScaffolding.lean. The tensor-valued linearization and chain-map identity are developed in the related Alexander–Whitney modules.

Mathematical content

For a singular n-simplex σ (with n = p + q), the AW diagonal is

Δ(σ) = Σ_{p+q=n} (front_p σ) ⊗ (back_q σ),

where:

• the front p-face front_p σ is the restriction of σ to the first p+1 vertices {0,…,p};
• the back q-face back_q σ is the restriction of σ to the last q+1 vertices {p,…,p+q}.

These restrictions are induced by the order-preserving maps

frontFace p q : ⦋p⦌ ⟶ ⦋p+q⦌ , i ↦ i (inclusion of an initial segment)
backFace p q : ⦋q⦌ ⟶ ⦋p+q⦌ , i ↦ i + p (inclusion of a final segment)

in SimplexCategory. The two faces overlap in the single vertex p (front's last vertex = back's first vertex), which is the geometric content of the diagonal.

What this file supplies

1. Front/back combinatorial face maps frontFace, backFace in SimplexCategory, with their value lemmas, the overlap/matching identity frontFace_last_eq_backFace_zero, injectivity, and the two structural recursion identities frontFace_succ (adding a top vertex via δ (last)) and backFace_succ_square (the front-of-δ₀ commuting square) that drive the eventual chain-map identity.
2. Singular-simplex front/back restrictions frontSimplex, backSimplex of a singular (p+q)-simplex, with their naturality in the space (frontSimplex_naturality, backSimplex_naturality).
3. Degree bookkeeping for p + q = n via Finset.antidiagonal (awIndex, mem_awIndex, awIndex_add).
4. Tensor-complex target objects singularChainTensorSquare (the chain-level C_•(X) ⊗ C_•(X), the codomain of the AW diagonal) with its functorial pullback and map_id/map_comp laws — the chain-level analogue of the cochain tensor square already in CupProductScaffolding.lean.
5. Object-level diagonal shape awPair — the (p,q)-component σ ↦ (front_p σ, back_q σ) of the (un-linearized) AW diagonal, natural in the space (awPair_naturality).

1. Front and back combinatorial face maps

def SphereOddDegree.AlexanderWhitney.frontFace (p q : ℕ) : { len := p } ⟶ { len := p + q }

The front p-face inclusion ⦋p⦌ ⟶ ⦋p+q⦌ in SimplexCategory, sending vertex i to i — the inclusion of the initial segment {0,…,p} of {0,…,p+q}.

Equations

• SphereOddDegree.AlexanderWhitney.frontFace p q = SimplexCategory.mkHom { toFun := fun (i : Fin (p + 1)) => Fin.castLE ⋯ i, monotone' := ⋯ }

def SphereOddDegree.AlexanderWhitney.backFace (p q : ℕ) : { len := q } ⟶ { len := p + q }

The back q-face inclusion ⦋q⦌ ⟶ ⦋p+q⦌ in SimplexCategory, sending vertex i to i + p — the inclusion of the final segment {p,…,p+q} of {0,…,p+q}.

Equations

• SphereOddDegree.AlexanderWhitney.backFace p q = SimplexCategory.mkHom { toFun := fun (i : Fin (q + 1)) => ⟨↑i + p, ⋯⟩, monotone' := ⋯ }

@[simp]

theorem SphereOddDegree.AlexanderWhitney.frontFace_apply (p q : ℕ) (i : Fin (p + 1)) : ↑((SimplexCategory.Hom.toOrderHom (frontFace p q)) i) = ↑i

@[simp]

theorem SphereOddDegree.AlexanderWhitney.backFace_apply (p q : ℕ) (i : Fin (q + 1)) : ↑((SimplexCategory.Hom.toOrderHom (backFace p q)) i) = ↑i + p

theorem SphereOddDegree.AlexanderWhitney.frontFace_last (p q : ℕ) : ↑((SimplexCategory.Hom.toOrderHom (frontFace p q)) (Fin.last p)) = p

The last vertex of the front p-face is p.

theorem SphereOddDegree.AlexanderWhitney.frontFace_zero (p q : ℕ) : ↑((SimplexCategory.Hom.toOrderHom (frontFace p q)) 0) = 0

The first vertex of the front p-face is 0.

theorem SphereOddDegree.AlexanderWhitney.backFace_zero (p q : ℕ) : ↑((SimplexCategory.Hom.toOrderHom (backFace p q)) 0) = p

The first vertex of the back q-face is p.

theorem SphereOddDegree.AlexanderWhitney.backFace_last (p q : ℕ) : ↑((SimplexCategory.Hom.toOrderHom (backFace p q)) (Fin.last q)) = p + q

The last vertex of the back q-face is p + q.

theorem SphereOddDegree.AlexanderWhitney.frontFace_last_eq_backFace_zero (p q : ℕ) : (SimplexCategory.Hom.toOrderHom (frontFace p q)) (Fin.last p) = (SimplexCategory.Hom.toOrderHom (backFace p q)) 0

Overlap / matching identity. The last vertex of the front p-face and the first vertex of the back q-face are the same vertex p of ⦋p+q⦌. This single shared vertex is the geometric content of the Alexander–Whitney diagonal.

theorem SphereOddDegree.AlexanderWhitney.frontFace_injective (p q : ℕ) : Function.Injective ⇑(SimplexCategory.Hom.toOrderHom (frontFace p q))

The front face map is injective on vertices.

theorem SphereOddDegree.AlexanderWhitney.backFace_injective (p q : ℕ) : Function.Injective ⇑(SimplexCategory.Hom.toOrderHom (backFace p q))

The back face map is injective on vertices.

theorem SphereOddDegree.AlexanderWhitney.frontFace_succ (p q : ℕ) : frontFace p (q + 1) = CategoryTheory.CategoryStruct.comp (frontFace p q) (SimplexCategory.δ (Fin.last (p + q + 1)))

Front recursion. Extending the back length by one is the same as post-composing the front face with the top face map δ (last), i.e. adding the new top vertex p+q+1 that the front face never reaches.

theorem SphereOddDegree.AlexanderWhitney.backFace_succ_square (p q : ℕ) : CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 0) (backFace p (q + 1)) = CategoryTheory.CategoryStruct.comp (backFace p q) (SimplexCategory.δ 0)

Back commuting square. The bottom face map δ 0 intertwines the back faces backFace p q and backFace p (q+1): both routes ⦋q⦌ ⟶ ⦋p+q+1⦌ send i ↦ i + p + 1. This is the first-face simplicial identity for the back faces that enters the chain-map identity of the AW diagonal.

2. Singular-simplex front/back restrictions

A singular (p+q)-simplex of a space X is an element of (TopCat.toSSet.obj X).obj (op ⦋p+q⦌). Restricting it along the front/back face maps yields its front p-face and back q-face, the two tensor factors of the (p,q)-component of the Alexander–Whitney diagonal.

noncomputable def SphereOddDegree.AlexanderWhitney.frontSimplex (X : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q })) : (TopCat.toSSet.obj X).obj (Opposite.op { len := p })

The front p-face of a singular (p+q)-simplex σ, obtained by restricting σ along frontFace p q.

Equations

• SphereOddDegree.AlexanderWhitney.frontSimplex X p q σ = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map (SphereOddDegree.AlexanderWhitney.frontFace p q).op)) σ

noncomputable def SphereOddDegree.AlexanderWhitney.backSimplex (X : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q })) : (TopCat.toSSet.obj X).obj (Opposite.op { len := q })

The back q-face of a singular (p+q)-simplex σ, obtained by restricting σ along backFace p q.

Equations

• SphereOddDegree.AlexanderWhitney.backSimplex X p q σ = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map (SphereOddDegree.AlexanderWhitney.backFace p q).op)) σ

theorem SphereOddDegree.AlexanderWhitney.frontSimplex_naturality {X Y : TopCat} (f : X ⟶ Y) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q })) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := p }))) (frontSimplex X p q σ) = frontSimplex Y p q ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := p + q }))) σ)

Naturality of the front face in the space. A continuous map f : X ⟶ Y commutes with taking front faces of singular simplices. This is naturality of the singular simplicial set functor TopCat.toSSet.

theorem SphereOddDegree.AlexanderWhitney.backSimplex_naturality {X Y : TopCat} (f : X ⟶ Y) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q })) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := q }))) (backSimplex X p q σ) = backSimplex Y p q ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := p + q }))) σ)

Naturality of the back face in the space. A continuous map f : X ⟶ Y commutes with taking back faces of singular simplices.

3. Degree bookkeeping for p + q = n

The Alexander–Whitney diagonal of an n-simplex is a sum over all splittings p + q = n, i.e. over Finset.antidiagonal n.

def SphereOddDegree.AlexanderWhitney.awIndex (n : ℕ) : Finset (ℕ × ℕ)

The index set of the degree-n Alexander–Whitney diagonal: all pairs (p, q) with p + q = n, the bidegrees of the tensor summands.

Equations

• SphereOddDegree.AlexanderWhitney.awIndex n = Finset.antidiagonal n

@[simp]

theorem SphereOddDegree.AlexanderWhitney.mem_awIndex {n : ℕ} {pq : ℕ × ℕ} : pq ∈ awIndex n ↔ pq.1 + pq.2 = n

theorem SphereOddDegree.AlexanderWhitney.awIndex_add {n : ℕ} {pq : ℕ × ℕ} (h : pq ∈ awIndex n) : pq.1 + pq.2 = n

Each summand bidegree (p, q) of the degree-n AW diagonal satisfies p + q = n.

4. Tensor-complex target objects C_•(X) ⊗ C_•(X)

With the monoidal wiring of CupProductScaffolding.lean in place, the tensor product of the singular chain complex with itself is a genuine ChainComplex (ModuleCat R) ℕ. This is the codomain of the Alexander–Whitney diagonal Δ : C_•(X) → C_•(X) ⊗ C_•(X).

noncomputable def SphereOddDegree.AlexanderWhitney.singularChainTensorSquare (R : Type) [CommRing R] (M : ModuleCat R) (X : TopCat) : ChainComplex (ModuleCat R) ℕ

The tensor square of the singular chain complex with coefficients in M : ModuleCat R, i.e. C_•(X; M) ⊗ C_•(X; M) as a ChainComplex (ModuleCat R) ℕ. This is the chain-level codomain of the Alexander–Whitney diagonal.

Equations

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

noncomputable def SphereOddDegree.AlexanderWhitney.singularChainTensorSquareMap (R : Type) [CommRing R] (M : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) : singularChainTensorSquare R M X ⟶ singularChainTensorSquare R M Y

The functorial pushforward on the chain tensor square: a continuous map f : X ⟶ Y induces f_# ⊗ f_# on the tensor squares.

Equations

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

@[simp]

theorem SphereOddDegree.AlexanderWhitney.singularChainTensorSquareMap_id (R : Type) [CommRing R] (M : ModuleCat R) (X : TopCat) : singularChainTensorSquareMap R M (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (singularChainTensorSquare R M X)

Functoriality: the chain tensor-square pushforward preserves identities.

theorem SphereOddDegree.AlexanderWhitney.singularChainTensorSquareMap_comp (R : Type) [CommRing R] (M : ModuleCat R) {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) : singularChainTensorSquareMap R M (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (singularChainTensorSquareMap R M f) (singularChainTensorSquareMap R M g)

Functoriality: the chain tensor-square pushforward preserves composition.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.AlexanderWhitney.singularChainTensorSquareZMod2 (X : TopCat) : ChainComplex (ModuleCat (ZMod 2)) ℕ

The tensor square of the singular F₂-chain complex, C_•(X; F₂) ⊗ C_•(X; F₂).

Equations

• SphereOddDegree.AlexanderWhitney.singularChainTensorSquareZMod2 X = SphereOddDegree.AlexanderWhitney.singularChainTensorSquare (ZMod 2) (↧(ZMod 2)) X

5. Object-level Alexander–Whitney diagonal shape

The (p, q)-component of the (un-linearized) Alexander–Whitney diagonal sends a singular (p+q)-simplex σ to the pair (front_p σ, back_q σ). Summing the linearizations of these pairs over awIndex n is the AW diagonal; the linearization itself is the required input (see the module footer).

noncomputable def SphereOddDegree.AlexanderWhitney.awPair (X : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q })) : (TopCat.toSSet.obj X).obj (Opposite.op { len := p }) × (TopCat.toSSet.obj X).obj (Opposite.op { len := q })

The (p, q)-component of the Alexander–Whitney diagonal, at the level of sets of simplices: a singular (p+q)-simplex σ maps to the pair of its front p-face and back q-face. The genuine chain diagonal is the R-linearization of the sum of these pairs over awIndex (p+q).

Equations

• SphereOddDegree.AlexanderWhitney.awPair X p q σ = (SphereOddDegree.AlexanderWhitney.frontSimplex X p q σ, SphereOddDegree.AlexanderWhitney.backSimplex X p q σ)

theorem SphereOddDegree.AlexanderWhitney.awPair_naturality {X Y : TopCat} (f : X ⟶ Y) (p q : ℕ) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := p + q })) : awPair Y p q ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := p + q }))) σ) = ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := p }))) (awPair X p q σ).1, (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := q }))) (awPair X p q σ).2)

Naturality of the object-level AW diagonal component in the space.