@[reducible, inline]

abbrev AlgebraicTopologyI.StdSimplexProd (p q : ℕ) : Type

The model space for the Eilenberg–Zilber construction in bidegree $(p,q)$: the product $\Delta^p \times \Delta^q$ of two standard simplices, which serves as the universal example used in acyclic models.

def AlgebraicTopologyI.stdSimplexBasepoint (n : ℕ) : ↑(stdSimplex ℝ (Fin (n + 1)))

A distinguished basepoint of the standard $n$-simplex (the vertex $e_0$), used as a base for inclusions of one factor into a product.

def AlgebraicTopologyI.universalSimplex (n : ℕ) : SingularSimplex n ↑(stdSimplex ℝ (Fin (n + 1)))

The universal (tautological) singular $n$-simplex: the identity map $\Delta^n \to \Delta^n$. Every singular $n$-simplex $\sigma : \Delta^n \to X$ is the pushforward of this universal one along $\sigma$.

def AlgebraicTopologyI.universalChain (n : ℕ) : SingularChains n ↑(stdSimplex ℝ (Fin (n + 1)))

The universal singular $n$-chain on $\Delta^n$: the generator of the free abelian group corresponding to the universal simplex.

noncomputable def AlgebraicTopologyI.crossFromModelChain {p q : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (c : SingularChains (p + q) (StdSimplexProd p q)) (σ : SingularSimplex p X) (τ : SingularSimplex q Y) : SingularChains (p + q) (X × Y)

Given a chain $c$ in the product of model simplices $\Delta^p \times \Delta^q$ and a pair of singular simplices $\sigma : \Delta^p \to X$, $\tau : \Delta^q \to Y$, push the model chain forward along $\sigma \times \tau$ to produce a chain in $X \times Y$. This is the basic naturality of the cross product built from a model chain.

noncomputable def AlgebraicTopologyI.leibnizTarget {p q : ℕ} (c_left : SingularChains (p + (q + 1)) (StdSimplexProd p (q + 1))) (c_right : SingularChains (p + 1 + q) (StdSimplexProd (p + 1) q)) : SingularChains (p + q + 1) (StdSimplexProd (p + 1) (q + 1))

The Leibniz target used in the inductive construction of the universal cross product: given chains realising the cross product in bidegrees $(p, q+1)$ and $(p+1, q)$, this assembles the right-hand side of the Leibniz rule $d(x \times y) = dx \times y + (-1)^p\, x \times dy$ in the next bidegree $(p+1, q+1)$.

@[irreducible]

noncomputable def AlgebraicTopologyI.universalCross (p q : ℕ) : SingularChains (p + q) (StdSimplexProd p q)

The universal cross product chain in bidegree $(p, q)$: a singular $(p+q)$-chain on $\Delta^p \times \Delta^q$ recursively built so that it satisfies the Leibniz rule with respect to the boundary. It serves as the model chain from which the Eilenberg–Zilber map is obtained by naturality, via the acyclicity of products of standard simplices.

structure AlgebraicTopologyI.ModelChainSystem : Type

A bidegree-graded family of model chains: a choice, for each pair $(p,q)$, of a singular $(p+q)$-chain on the product $\Delta^p \times \Delta^q$. This packages the data of a candidate Eilenberg–Zilber cross product at the level of model spaces.

• chains (p q : ℕ) : SingularChains (p + q) (StdSimplexProd p q)