Barycentric subdivision as a chain map

This file packages the degree-wise barycentric subdivision maps barycentricSubdivisionLinearMap R X n into a single morphism of chain complexes from the singular chain complex of X to itself.

The chain-map condition is exactly the boundary-commutation identity barycentricSubdivisionLinearMap_commutes_boundary proved earlier.

Main results

• barycentricSubdivisionChainMap: the chain map singularChainComplex R X ⟶ singularChainComplex R X;
• barycentricSubdivisionChainMap_f_n: its degree-n component is the previously defined degree-wise map barycentricSubdivisionLinearMap R X n;
• barycentricSubdivisionChainMap_map_generator: on a basis generator [σ] the chain map gives the signed subdivision sum barycentricSubdivisionGenerator R X n σ.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.AffineBarycentricSubdivision.singularChainComplex (R : Type) [CommRing R] (X : TopCat) : ChainComplex (ModuleCat R) ℕ

The singular chain complex C_•(X; R) of X with coefficients in R, specialized to coefficients R as a module over itself. This is the actual project object underlying singularChainGroup, singularBoundary and barycentricSubdivisionLinearMap.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.singularChainComplex R X = ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).obj X

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainMap (R : Type) [CommRing R] (X : TopCat) : singularChainComplex R X ⟶ singularChainComplex R X

Barycentric subdivision as a chain map. The degree-wise subdivision maps barycentricSubdivisionLinearMap R X n assemble into a morphism of chain complexes singularChainComplex R X ⟶ singularChainComplex R X. The chain-map condition is the boundary commutation barycentricSubdivisionLinearMap_commutes_boundary.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainMap_f_n (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : (barycentricSubdivisionChainMap R X).f n = barycentricSubdivisionLinearMap R X n

Degree-wise component of the subdivision chain map. In degree n the chain map is exactly the previously defined degree-wise operator.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainMap_map_generator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : (ModuleCat.Hom.hom ((barycentricSubdivisionChainMap R X).f n)) (chainGenerator R X n σ) = barycentricSubdivisionGenerator R X n σ

Generator formula for the subdivision chain map. On a basis generator [σ] the chain map returns the signed subdivision sum barycentricSubdivisionGenerator R X n σ.