noncomputable def AlgebraicTopologyI.crossProductMap (p q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] : SingularChains p X →+ SingularChains q Y →+ SingularChains (p + q) (X × Y)

The singular chain cross product × : S_p(X) × S_q(Y) → S_{p+q}(X × Y) as a bilinear map, defined on generators by applying the universal model cross product to each pair of simplices and extending freely. This is the underlying construction for Theorem 6.2.

theorem AlgebraicTopologyI.crossProductMap_naturality (p q : ℕ) (X X' Y Y' : Type) [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (f : C(X, X')) (g : C(Y, Y')) (a : SingularChains p X) (b : SingularChains q Y) : ((crossProductMap p q X' Y') ((SingularChains.map f) a)) ((SingularChains.map g) b) = (SingularChains.map (f.prodMap g)) (((crossProductMap p q X Y) a) b)

Naturality of the cross product: for continuous maps f : X → X' and g : Y → Y', the cross product commutes with the induced maps on singular chains, i.e. f_*(a) × g_*(b) = (f × g)_*(a × b). This is the naturality part of Theorem 6.2.

theorem AlgebraicTopologyI.crossProductMap_leibniz (p q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (a : SingularChains (p + 1) X) (b : SingularChains (q + 1) Y) : have ab := ((crossProductMap (p + 1) (q + 1) X Y) a) b; have ab' := (SingularChains.castIdx ⋯) ab; have dab := (boundaryMap (p + q + 1) (X × Y)) ab'; have da_b := (SingularChains.castIdx ⋯) (((crossProductMap p (q + 1) X Y) ((boundaryMap p X) a)) b); have a_db := (SingularChains.castIdx ⋯) (((crossProductMap (p + 1) q X Y) a) ((boundaryMap q Y) b)); dab = da_b + (-1) ^ (p + 1) • a_db

The Leibniz rule for the cross product: the boundary of a cross product chain satisfies d(a × b) = (da) × b + (-1)^p · a × (db). This is the graded-derivation part of Theorem 6.2.

theorem AlgebraicTopologyI.crossProductMap_normalization_left (q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (x : X) (b : SingularChains q Y) : (SingularChains.castIdx ⋯) (((crossProductMap 0 q X Y) (constChain x)) b) = (SingularChains.map (inclusionRight x)) b

Left normalization for the cross product: for any point x ∈ X and any chain b ∈ S_q(Y), the cross product c_x^0 × b agrees with the chain obtained by pushing b forward along the inclusion y ↦ (x, y). This is the left-normalization clause of Theorem 6.2.

theorem AlgebraicTopologyI.crossProductMap_normalization_right (p : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (y : Y) (a : SingularChains p X) : ((crossProductMap p 0 X Y) a) (constChain y) = (SingularChains.map (inclusionLeft y)) a

Right normalization for the cross product: for any point y ∈ Y and any chain a ∈ S_p(X), the cross product a × c_y^0 agrees with the chain obtained by pushing a forward along the inclusion x ↦ (x, y). This is the right-normalization clause of Theorem 6.2.

theorem AlgebraicTopologyI.crossProduct_exists : Nonempty CrossProduct

Theorem 6.2: there exists a singular chain cross product × : S_p(X) × S_q(Y) → S_{p+q}(X × Y) satisfying naturality, bilinearity, the Leibniz rule, and the normalization conditions. The witness is built from crossProductMap together with the four preceding lemmas.

structure AlgebraicTopologyI.SingularChainHomotopy {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f0 f1 : C(X, Y)) : Type

A chain homotopy between the singular-chain maps induced by two continuous maps f0, f1 : X → Y: a sequence of homomorphisms hom n : S_n(X) → S_{n+1}(Y) satisfying the chain-homotopy identity d ∘ hom + hom ∘ d = f1_* - f0_*. This is the chain-level homotopy witnessing Theorem 6.1 / Proposition 5.11.

• hom (n : ℕ) : SingularChains n X →+ SingularChains (n + 1) Y
• chain_htpy (n : ℕ) (s : SingularChains (n + 1) X) : (boundaryMap (n + 1) Y) ((self.hom (n + 1)) s) + (self.hom n) ((boundaryMap n X) s) = (SingularChains.map f1) s - (SingularChains.map f0) s

noncomputable def AlgebraicTopologyI.inclusion0 (X : Type) [TopologicalSpace X] : C(X, X × ↑unitInterval)

The bottom inclusion X → X × I given by x ↦ (x, 0).

noncomputable def AlgebraicTopologyI.inclusion1 (X : Type) [TopologicalSpace X] : C(X, X × ↑unitInterval)

The top inclusion X → X × I given by x ↦ (x, 1).

structure AlgebraicTopologyI.NaturalChainHomotopyInclusions : Type 1

A natural chain homotopy between the singular-chain maps induced by the two inclusions inclusion0, inclusion1 : X → X × I. The data consists of homomorphisms S_n(X) → S_{n+1}(X × I) satisfying the chain-homotopy identity and a naturality square in X. This is the universal ingredient used to build chain homotopies from continuous homotopies in Theorem 6.1.

• hom (X : Type) [TopologicalSpace X] (n : ℕ) : SingularChains n X →+ SingularChains (n + 1) (X × ↑unitInterval)
• chain_htpy (X : Type) [TopologicalSpace X] (n : ℕ) (s : SingularChains (n + 1) X) : (boundaryMap (n + 1) (X × ↑unitInterval)) ((self.hom X (n + 1)) s) + (self.hom X n) ((boundaryMap n X) s) = (SingularChains.map (inclusion1 X)) s - (SingularChains.map (inclusion0 X)) s
• naturality (X X' : Type) [TopologicalSpace X] [TopologicalSpace X'] (g : C(X', X)) (n : ℕ) (s : SingularChains n X') : (SingularChains.map (g.prodMap (ContinuousMap.id ↑unitInterval))) ((self.hom X' n) s) = (self.hom X n) ((SingularChains.map g) s)

theorem AlgebraicTopologyI.SingularChains.map_comp {n : ℕ} {X Y Z : Type} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(Y, Z)) (g : C(X, Y)) (s : SingularChains n X) : (map (f.comp g)) s = (map f) ((map g) s)

Functoriality of the singular-chain map: the chain map induced by a composition of continuous maps is the composition of the induced chain maps.

theorem AlgebraicTopologyI.boundaryMap_map_comm {n : ℕ} {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (s : SingularChains (n + 1) X) : (boundaryMap n Y) ((SingularChains.map f) s) = (SingularChains.map f) ((boundaryMap n X) s)

The singular boundary map commutes with the chain map induced by a continuous map; equivalently, SingularChains.map f is a chain map.

noncomputable def AlgebraicTopologyI.iotaSimplex : SingularSimplex 1 ↑unitInterval

The fundamental singular 1-simplex ι₁ : Δ¹ → I given on barycentric coordinates (t₀, t₁) by (t₀, t₁) ↦ t₁.

theorem AlgebraicTopologyI.iotaSimplex_face0 : SingularSimplex.face 0 iotaSimplex = constSimplex ⟨1, unitInterval.one_mem⟩

The 0-th face of iotaSimplex is the constant simplex at 1.

theorem AlgebraicTopologyI.iotaSimplex_face1 : SingularSimplex.face 1 iotaSimplex = constSimplex ⟨0, unitInterval.zero_mem⟩

The 1-st face of iotaSimplex is the constant simplex at 0.

theorem AlgebraicTopologyI.boundary_iota : (boundaryMap 0 ↑unitInterval) (FreeAbelianGroup.of iotaSimplex) = constChain ⟨1, unitInterval.one_mem⟩ - constChain ⟨0, unitInterval.zero_mem⟩

The boundary of the fundamental 1-simplex ι₁ on I is c₁⁰ - c₀⁰, the difference of the constant 0-simplices at the endpoints.

theorem AlgebraicTopologyI.inclusionLeft_one_eq_inclusion1 (X : Type) [TopologicalSpace X] : inclusionLeft ⟨1, unitInterval.one_mem⟩ = inclusion1 X

The right-product-inclusion at the endpoint 1 ∈ I agrees with inclusion1.

theorem AlgebraicTopologyI.inclusionLeft_zero_eq_inclusion0 (X : Type) [TopologicalSpace X] : inclusionLeft ⟨0, unitInterval.zero_mem⟩ = inclusion0 X

The right-product-inclusion at the endpoint 0 ∈ I agrees with inclusion0.

theorem AlgebraicTopologyI.naturalChainHomotopyInclusions_exists : Nonempty NaturalChainHomotopyInclusions

Existence of a natural chain homotopy between the two inclusions X → X × I. The witness is built by crossing with the fundamental 1-simplex ι₁ on I and using the Leibniz rule and normalization of the singular chain cross product. This is the chain-level engine behind Theorem 6.1.

noncomputable def AlgebraicTopologyI.ContinuousMap.Homotopy.naturalSingularChainHomotopy {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] {f0 f1 : C(X, Y)} (h : f0.Homotopy f1) : SingularChainHomotopy f0 f1

Theorem 6.1: a continuous homotopy h : f0 ≃ f1 : X → Y determines a natural chain homotopy f0_* ≃ f1_* : S_*(X) → S_*(Y). The chain homotopy is constructed by composing the universal chain homotopy for the inclusions X → X × I (cf. NaturalChainHomotopyInclusions) with the homotopy h.