@[reducible, inline]

noncomputable abbrev BarycentricSubdivision.singularChainFunctorZ : CategoryTheory.Functor TopCat (ChainComplex AddCommGrpCat ℕ)

The singular chain complex functor with integer coefficients, X ↦ S_*(X; ℤ), as a functor from topological spaces to non-negatively graded chain complexes of abelian groups. This is the ambient functor on which the subdivision operator acts.

noncomputable def BarycentricSubdivision.barycenter (n : ℕ) : ↑(stdSimplex ℝ (Fin (n + 1)))

The barycenter of the standard n-simplex Δ^n: the point all of whose barycentric coordinates equal 1/(n+1). This is the cone point used in the subdivision construction of Section 12.

@[simp]

theorem BarycentricSubdivision.barycenter_coord (n : ℕ) (i : Fin (n + 1)) : ↑(barycenter n) i = 1 / (↑n + 1)

Each barycentric coordinate of the barycenter of Δ^n is 1/(n+1).

noncomputable def BarycentricSubdivision.stdSimplexTop (n : ℕ) : TopCat

The standard topological n-simplex Δ^n, viewed as an object of TopCat.

def BarycentricSubdivision.SingType (X : TopCat) (n : ℕ) : Type

The type of singular n-simplices of X, i.e. Sin_n(X), accessed via the underlying simplicial set of X.

theorem BarycentricSubdivision.chainGroup_eq_coprod (X : TopCat) (n : ℕ) : (singularChainFunctorZ.obj X).X n = ∐ fun (x : SingType X n) => AddCommGrpCat.of ℤ

The chain group S_n(X; ℤ) is definitionally the coproduct of copies of ℤ indexed by singular n-simplices, exhibiting it as the free abelian group on Sin_n(X) (Definition 1.3).

noncomputable def BarycentricSubdivision.identitySimplex (n : ℕ) : SingType (stdSimplexTop n) n

The identity map Δ^n → Δ^n viewed as a singular n-simplex of Δ^n. This is the universal n-simplex ι_n on which the subdivision construction is built.

noncomputable def BarycentricSubdivision.coneSingularSimplexFun {n k : ℕ} (b : ↑(stdSimplex ℝ (Fin (n + 1)))) (τ : stdSimplexTop k ⟶ stdSimplexTop n) (x : ↑(stdSimplexTop (k + 1))) : ↑(stdSimplexTop n)

The set-level cone construction b * τ taking a (k+1)-simplex of Δ^n. Given a cone point b ∈ Δ^n and a k-simplex τ : Δ^k → Δ^n, this sends a point x = (t₀, t₁, …, t_{k+1}) of Δ^{k+1} to the linear interpolation t₀ · b + (1 - t₀) · τ(x₁, …, x_{k+1}) after renormalizing the tail.

theorem BarycentricSubdivision.coneSingularSimplex_continuous {n k : ℕ} (b : ↑(stdSimplex ℝ (Fin (n + 1)))) (τ : stdSimplexTop k ⟶ stdSimplexTop n) : Continuous (coneSingularSimplexFun b τ)

The cone map coneSingularSimplexFun b τ : Δ^{k+1} → Δ^n is continuous.

noncomputable def BarycentricSubdivision.coneSingularSimplex {n k : ℕ} (b : ↑(stdSimplex ℝ (Fin (n + 1)))) (τ : stdSimplexTop k ⟶ stdSimplexTop n) : stdSimplexTop (k + 1) ⟶ stdSimplexTop n

The cone b * τ : Δ^{k+1} → Δ^n of a singular k-simplex τ of Δ^n over the cone point b, as a morphism in TopCat.

noncomputable def BarycentricSubdivision.coneOperator {n : ℕ} (b : ↑(stdSimplex ℝ (Fin (n + 1)))) (k : ℕ) : (singularChainFunctorZ.obj (stdSimplexTop n)).X k ⟶ (singularChainFunctorZ.obj (stdSimplexTop n)).X (k + 1)

The cone operator b * (-) : S_k(Δ^n) → S_{k+1}(Δ^n) sending each generator τ to its cone b * τ over the chosen cone point b ∈ Δ^n, extended linearly.

noncomputable def BarycentricSubdivision.chainGenerator {X : TopCat} {n : ℕ} (σ : SingType X n) : ↑((singularChainFunctorZ.obj X).X n)

The chain 1 · σ ∈ S_n(X) associated to a singular simplex σ, viewed as a free generator in the coproduct representation of the singular chain group.

noncomputable def BarycentricSubdivision.chainPushforward {X : TopCat} {k : ℕ} (elem : ↑((singularChainFunctorZ.obj (stdSimplexTop k)).X k)) (σ : SingType X k) : ↑((singularChainFunctorZ.obj X).X k)

Push forward a chain elem ∈ S_k(Δ^k) along a singular k-simplex σ : Δ^k → X to obtain a chain in S_k(X).

noncomputable def BarycentricSubdivision.sdDegreeWithElem {k : ℕ} (elem : ↑((singularChainFunctorZ.obj (stdSimplexTop k)).X k)) (X : TopCat) : (singularChainFunctorZ.obj X).X k ⟶ (singularChainFunctorZ.obj X).X k

Endomorphism of S_k(X) built from a chosen element elem ∈ S_k(Δ^k): on each generator σ it returns the pushforward σ_*(elem). This is the abstract pattern used to define the subdivision operator from its values on the universal simplex.

def BarycentricSubdivision.sdIota_elem (n : ℕ) : ↑((singularChainFunctorZ.obj (stdSimplexTop n)).X n)

The subdivision $ι_n ∈ S_n(Δ^n) of the universal n-simplex, defined recursively: in degree 0 it is the identity simplex, and in degree n + 1 it is the cone from the barycenter over the subdivision of the boundary d ι_{n+1}. This is the inductive definition driving the construction of the subdivision operator of Proposition 12.1.

noncomputable def BarycentricSubdivision.sdIotaHom (n : ℕ) : AddCommGrpCat.of ℤ ⟶ (singularChainFunctorZ.obj (stdSimplexTop n)).X n

The subdivision element $ι_n, packaged as the group homomorphism ℤ → S_n(Δ^n) sending 1 to $ι_n.

noncomputable def BarycentricSubdivision.sdSigmaComponent (X : TopCat) (n : ℕ) (σ : SingType X n) : AddCommGrpCat.of ℤ ⟶ (singularChainFunctorZ.obj X).X n

The component of the subdivision operator on the free generator indexed by σ: it sends the generator to σ_*($ι_n) ∈ S_n(X).

noncomputable def BarycentricSubdivision.sdDegreeMap (X : TopCat) (n : ℕ) : (singularChainFunctorZ.obj X).X n ⟶ (singularChainFunctorZ.obj X).X n

The subdivision operator $ : S_n(X) → S_n(X) in degree n, assembled from its components on free generators via the coproduct universal property.

theorem BarycentricSubdivision.sdDegreeMap_comm_on_stdSimplex (n i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) : CategoryTheory.CategoryStruct.comp (sdDegreeMap (stdSimplexTop n) i) ((singularChainFunctorZ.obj (stdSimplexTop n)).d i j) = CategoryTheory.CategoryStruct.comp ((singularChainFunctorZ.obj (stdSimplexTop n)).d i j) (sdDegreeMap (stdSimplexTop n) j)

The subdivision operator commutes with the boundary on S_*(Δ^n); that is, on the standard simplex it is a chain map. This standard-simplex case is the seed from which the general chain-map property is bootstrapped by naturality.

theorem BarycentricSubdivision.sdDegreeMap_comm (X : TopCat) (i j : ℕ) (hij : (ComplexShape.down ℕ).Rel i j) : CategoryTheory.CategoryStruct.comp (sdDegreeMap X i) ((singularChainFunctorZ.obj X).d i j) = CategoryTheory.CategoryStruct.comp ((singularChainFunctorZ.obj X).d i j) (sdDegreeMap X j)

The subdivision operator $ commutes with the boundary on S_*(X) for any topological space X, so it is a chain map. This is the chain-map half of Proposition 12.1, deduced from the standard-simplex case by naturality.

noncomputable def BarycentricSubdivision.sdChainMap (X : TopCat) : singularChainFunctorZ.obj X ⟶ singularChainFunctorZ.obj X

The subdivision chain map $ : S_*(X) → S_*(X), assembled from the degreewise maps sdDegreeMap X n together with the boundary-commutation theorem. This is the chain map of Proposition 12.1 for a fixed space X.

theorem BarycentricSubdivision.sdChainMap_naturality (X Y : TopCat) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (singularChainFunctorZ.map f) (sdChainMap Y) = CategoryTheory.CategoryStruct.comp (sdChainMap X) (singularChainFunctorZ.map f)

Naturality of the subdivision chain map in X: for f : X → Y, the squares f_* ∘ $_X = $_Y ∘ f_* commute. This is the naturality assertion of Proposition 12.1.

noncomputable def BarycentricSubdivision.subdivisionOperator : singularChainFunctorZ ⟶ singularChainFunctorZ

The subdivision operator as a natural transformation $ : S_* ⟹ S_* of singular chain complex functors. This is the natural chain map of Proposition 12.1.

noncomputable def BarycentricSubdivision.homotopyPushforward {X : TopCat} {k : ℕ} (elem : ↑((singularChainFunctorZ.obj (stdSimplexTop k)).X (k + 1))) (σ : SingType X k) : ↑((singularChainFunctorZ.obj X).X (k + 1))

Push forward a chain elem ∈ S_{k+1}(Δ^k) along a singular k-simplex σ : Δ^k → X to obtain a chain in S_{k+1}(X). Used in the construction of the chain homotopy.

noncomputable def BarycentricSubdivision.homotopyDegreeWithElem {k : ℕ} (elem : ↑((singularChainFunctorZ.obj (stdSimplexTop k)).X (k + 1))) (X : TopCat) : (singularChainFunctorZ.obj X).X k ⟶ (singularChainFunctorZ.obj X).X (k + 1)

Degree-raising map S_k(X) → S_{k+1}(X) built from a chosen element elem ∈ S_{k+1}(Δ^k): on each generator σ it returns σ_*(elem). This is the abstract pattern used to build the chain homotopy.

def BarycentricSubdivision.sdHomotopyIota_elem (n : ℕ) : ↑((singularChainFunctorZ.obj (stdSimplexTop n)).X (n + 1))

The element T_n ∈ S_{n+1}(Δ^n) defining the chain homotopy on the universal n-simplex, constructed recursively: zero in degree 0, and in degree n + 1 the cone from the barycenter over $ι_{n+1} - ι_{n+1} - T(dι_{n+1}). This is the standard inductive recipe yielding dh + hd = $ - 1.

noncomputable def BarycentricSubdivision.sdHomotopyIotaHom (n : ℕ) : AddCommGrpCat.of ℤ ⟶ (singularChainFunctorZ.obj (stdSimplexTop n)).X (n + 1)

The chain-homotopy element T_n, packaged as the group homomorphism ℤ → S_{n+1}(Δ^n) sending 1 to T_n.

noncomputable def BarycentricSubdivision.sdHomotopySigmaComponent (X : TopCat) (n : ℕ) (σ : SingType X n) : AddCommGrpCat.of ℤ ⟶ (singularChainFunctorZ.obj X).X (n + 1)

The component of the chain homotopy on the free generator indexed by σ: it sends the generator to σ_*(T_n) ∈ S_{n+1}(X).

noncomputable def BarycentricSubdivision.sdHomotopyDegreeMap (X : TopCat) (n : ℕ) : (singularChainFunctorZ.obj X).X n ⟶ (singularChainFunctorZ.obj X).X (n + 1)

The chain homotopy h : S_n(X) → S_{n+1}(X) in degree n, assembled from its components on the free generators of S_n(X).

noncomputable def BarycentricSubdivision.sdChainHomotopyHom (X : TopCat) (i j : ℕ) : (singularChainFunctorZ.obj X).X i ⟶ (singularChainFunctorZ.obj X).X j

The chain homotopy assembled into the family of maps required by Mathlib's Homotopy structure: it equals sdHomotopyDegreeMap (up to a degree cast) when j = i + 1 and is zero otherwise.

theorem BarycentricSubdivision.sdChainHomotopyHom_zero (X : TopCat) (i j : ℕ) (h : ¬(ComplexShape.down ℕ).Rel j i) : sdChainHomotopyHom X i j = 0

Outside the relevant degree shift the chain homotopy vanishes.

theorem BarycentricSubdivision.sdChainHomotopyHom_comm_on_stdSimplex (i : ℕ) : (sdChainMap (stdSimplexTop i)).f i = (dNext i) (sdChainHomotopyHom (stdSimplexTop i)) + (prevD i) (sdChainHomotopyHom (stdSimplexTop i)) + (CategoryTheory.CategoryStruct.id (singularChainFunctorZ.obj (stdSimplexTop i))).f i

On the standard simplex Δ^i, the chain homotopy identity $ = dh + hd + id holds in degree i. This is the seed case from which the general identity is bootstrapped by naturality.

theorem BarycentricSubdivision.sdChainHomotopyHom_comm (X : TopCat) (i : ℕ) : (sdChainMap X).f i = (dNext i) (sdChainHomotopyHom X) + (prevD i) (sdChainHomotopyHom X) + (CategoryTheory.CategoryStruct.id (singularChainFunctorZ.obj X)).f i

The chain homotopy identity $ = dh + hd + id in every degree on S_*(X) for any topological space X. This is the chain-homotopy half of Proposition 12.1: $ is chain-homotopic to the identity.

noncomputable def BarycentricSubdivision.subdivisionChainHomotopy (X : TopCat) : Homotopy (subdivisionOperator.app X) (CategoryTheory.CategoryStruct.id (singularChainFunctorZ.obj X))

The chain homotopy h : $ ≃ id on S_*(X), packaged as a Homotopy between the subdivision operator and the identity chain map. This is the explicit witness behind Proposition 12.1.

theorem BarycentricSubdivision.subdivision_homotopic_id (X : TopCat) : Nonempty (Homotopy (subdivisionOperator.app X) (CategoryTheory.CategoryStruct.id (singularChainFunctorZ.obj X)))

Proposition 12.1: the subdivision operator $ on S_*(X) is chain-homotopic to the identity.

theorem BarycentricSubdivision.sdHomotopyDegreeMap_naturality (X Y : TopCat) (f : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((singularChainFunctorZ.map f).f n) (sdHomotopyDegreeMap Y n) = CategoryTheory.CategoryStruct.comp (sdHomotopyDegreeMap X n) ((singularChainFunctorZ.map f).f (n + 1))

Naturality of the chain-homotopy degree map in X: f_* ∘ h_X = h_Y ∘ f_* for every continuous map f : X → Y. This makes the chain homotopy from Proposition 12.1 natural in the space.