Barycentric subdivision of singular chains #
The barycentric subdivision of the standard n-simplex Δⁿ has one n-simplex for each
permutation π of the vertices {0, …, n}: the affine simplex
StdSimplex.continuousAffineMapMk (BarycentricSubdivision.vertex π) whose k-th vertex is the
barycenter of the face of Δⁿ spanned by π k, …, π n. Its vertices are thus the barycenters
of a decreasing chain of faces, starting at the barycenter of Δⁿ itself.
The barycentric subdivision of a singular n-simplex σ : Δⁿ → X is the signed sum over π of
sign π • σ ∘ StdSimplex.continuousAffineMapMk (vertex π). This is the closed form of Hatcher's
inductive definition S σ = σ_♯ (b · S (∂ Δⁿ)), where b · is the cone from the barycenter b
of Δⁿ, placed as the first vertex. It is a morphism of singular chain complexes, natural in the
space.
Main definitions and results #
TauCeti.BarycentricSubdivision.sum_sign_boundary: the boundary formula for the subdivision of the standard simplex. The faces of the subdivision simplices that meet the interior ofΔⁿcancel in pairs (exchanging two consecutive entries ofπ), and the remaining faces, which omit the barycenter ofΔⁿ, are the subdivision simplices of the facets ofΔⁿ, with the signs of the simplicial boundary (reindexing through Mathlib'sEquiv.Perm.decomposeFin').TauCeti.singularSubdivisionX: the subdivision of singularn-chains with coefficients in an objectRof a preadditive category, computed on summands byTauCeti.ιChainComplex_singularSubdivisionX; it is the identity on0-chains (TauCeti.singularSubdivisionX_zero).TauCeti.singularSubdivisionChainMap: the subdivision is a chain map,∂ S = S ∂.TauCeti.singularSubdivision: the subdivision as a natural endomorphism of the singular chain complex functorTopCat ⥤ ChainComplex C ℕ.
References #
- A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, steps (2) and (3).
The k-th vertex of the simplex of the barycentric subdivision of the standard n-simplex
indexed by the permutation π: the barycenter of the face spanned by π k, …, π n.
Equations
Instances For
The vertices of a subdivision simplex other than the barycenter of the simplex are the vertices of the subdivision simplex of a facet, pushed forward along the facet inclusion.
The faces of the subdivision simplices of Δⁿ⁺¹ which contain the barycenter of Δⁿ⁺¹
cancel in pairs.
The faces of the subdivision simplices of Δⁿ⁺¹ which omit the barycenter of Δⁿ⁺¹ are the
subdivision simplices of the facets of Δⁿ⁺¹, with the signs of the simplicial boundary.
Boundary formula for the barycentric subdivision of the standard simplex. The signed
sum of the faces of the subdivision simplices of Δⁿ⁺¹ equals the signed sum, over the facets of
Δⁿ⁺¹, of the subdivision simplices of the facet. The simplices are recorded by their vertices,
and F is an arbitrary function of the vertices with values in an abelian group.
The barycentric subdivision of singular n-chains of X with coefficients in R: the
summand of a singular simplex σ is sent to the signed sum over the permutations π of the
summands of the singular simplices σ ∘ StdSimplex.continuousAffineMapMk (vertex π).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The barycentric subdivision is the identity on singular 0-chains.
The barycentric subdivision of singular chains of X with coefficients in R, as an
endomorphism of the singular chain complex: the boundary formula ∂ S = S ∂.
Equations
- TauCeti.singularSubdivisionChainMap R X = { f := fun (n : ℕ) => TauCeti.singularSubdivisionX R X n, comm' := ⋯ }
Instances For
Barycentric subdivision of singular chains. The barycentric subdivision operator on the
singular chain complexes with coefficients in R, as a natural transformation of functors
TopCat ⥤ ChainComplex C ℕ.
Equations
- TauCeti.singularSubdivision R = { app := fun (X : TopCat) => TauCeti.singularSubdivisionChainMap R X, naturality := ⋯ }