theorem AlgebraicTopologyI.faceMap_mem_stdSimplex (n : ℕ) (i : Fin (n + 2)) (t : Fin (n + 1) → ℝ) (ht : t ∈ stdSimplex ℝ (Fin (n + 1))) : i.insertNth 0 t ∈ stdSimplex ℝ (Fin (n + 2))

Inserting a zero in the i-th coordinate of a point of the standard (n+1)-simplex yields a point of the standard (n+2)-simplex: this is the i-th face inclusion at the level of barycentric coordinates.

noncomputable def AlgebraicTopologyI.faceInclusion (n : ℕ) (i : Fin (n + 2)) : C(↑(stdSimplex ℝ (Fin (n + 1))), ↑(stdSimplex ℝ (Fin (n + 2))))

The continuous i-th face inclusion Δⁿ ↪ Δⁿ⁺¹ that sends the barycentric coordinates t to the tuple with 0 inserted in position i.

noncomputable def AlgebraicTopologyI.SingularSimplex.face {n : ℕ} {X : Type u_1} [TopologicalSpace X] (i : Fin (n + 2)) (σ : SingularSimplex (n + 1) X) : SingularSimplex n X

The i-th face of a singular (n+1)-simplex σ, obtained by precomposing with the i-th face inclusion of the standard simplex.

noncomputable def AlgebraicTopologyI.boundaryMap (n : ℕ) (X : Type u_1) [TopologicalSpace X] : SingularChains (n + 1) X →+ SingularChains n X

The singular boundary map d : S_{n+1}(X) → S_n(X) defined on generators by the alternating sum ∑_i (-1)^i σ ∘ d^i of face restrictions.

noncomputable def AlgebraicTopologyI.SingularSimplex.map {n : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) (σ : SingularSimplex n X) : SingularSimplex n Y

Pushforward of a singular n-simplex along a continuous map f : X → Y, namely f ∘ σ.

noncomputable def AlgebraicTopologyI.SingularChains.map {n : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : C(X, Y)) : SingularChains n X →+ SingularChains n Y

The induced map on singular chains f_* : S_n(X) → S_n(Y), extending the pushforward of simplices linearly.

noncomputable def AlgebraicTopologyI.inclusionRight {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (x : X) : C(Y, X × Y)

The slice inclusion j_x : Y → X × Y, y ↦ (x, y).

noncomputable def AlgebraicTopologyI.inclusionLeft {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) : C(X, X × Y)

The slice inclusion i_y : X → X × Y, x ↦ (x, y).

noncomputable def AlgebraicTopologyI.constSimplex {X : Type u_1} [TopologicalSpace X] (x : X) : SingularSimplex 0 X

The constant 0-simplex c_x^0 : Δ^0 → X at the point x.

noncomputable def AlgebraicTopologyI.constChain {X : Type u_1} [TopologicalSpace X] (x : X) : SingularChains 0 X

The constant 0-chain at x, namely the generator of S_0(X) corresponding to the constant simplex c_x^0.

noncomputable def AlgebraicTopologyI.SingularChains.castIdx {n m : ℕ} (h : n = m) {X : Type u_1} [TopologicalSpace X] : SingularChains n X →+ SingularChains m X

Trivial reindexing isomorphism S_n(X) → S_m(X) along an equality n = m. Used to identify chains living in defeq-but-not-syntactically-equal degrees.

structure AlgebraicTopologyI.CrossProduct : Type 1

(Theorem 6.2) Bundle of data and axioms for the singular cross product × : S_p(X) × S_q(Y) → S_{p+q}(X × Y): it is natural in both arguments, bilinear, satisfies the Leibniz rule d(a × b) = (da) × b + (-1)^p a × db, and is normalized so that c_x^0 × b = (j_x)_* b and a × c_y^0 = (i_y)_* a.

• crossMap (p q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] : SingularChains p X →+ SingularChains q Y →+ SingularChains (p + q) (X × Y)
• 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) : ((self.crossMap p q X' Y') ((SingularChains.map f) a)) ((SingularChains.map g) b) = (SingularChains.map (f.prodMap g)) (((self.crossMap p q X Y) a) b)
• leibniz (p q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (a : SingularChains (p + 1) X) (b : SingularChains (q + 1) Y) : let ab := ((self.crossMap (p + 1) (q + 1) X Y) a) b; let ab' := (SingularChains.castIdx ⋯) ab; let dab := (boundaryMap (p + q + 1) (X × Y)) ab'; let da_b := (SingularChains.castIdx ⋯) (((self.crossMap p (q + 1) X Y) ((boundaryMap p X) a)) b); let a_db := (SingularChains.castIdx ⋯) (((self.crossMap (p + 1) q X Y) a) ((boundaryMap q Y) b)); dab = da_b + (-1) ^ (p + 1) • a_db
• normalization_left (q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (x : X) (b : SingularChains q Y) : (SingularChains.castIdx ⋯) (((self.crossMap 0 q X Y) (constChain x)) b) = (SingularChains.map (inclusionRight x)) b
• normalization_right (p : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (y : Y) (a : SingularChains p X) : ((self.crossMap p 0 X Y) a) (constChain y) = (SingularChains.map (inclusionLeft y)) a