Chain-level barycentric boundary commutation ∂ ∘ sd = sd ∘ ∂

This file lifts the generator-level cancellation expandedBarycentricBoundaryCancellation (from BarycentricBoundaryCancellation.lean) to all singular chains.

The main results are:

• barycentricSubdivisionLinearMap_commutes_boundary: the morphism-level identity

sd ≫ ∂ = ∂ ≫ sd

in the category of R-modules, i.e. degree-wise barycentric subdivision is a chain map for the singular boundary;

• boundary_barycentricSubdivision_apply: the pointwise version, ∂ (sd c) = sd (∂ c) for every chain c.

Degree convention

The singular boundary singularBoundary R X n : C_{n+1} → C_n is the degree (n+1) → n differential of the alternating face map complex, with the library's (-1)^i sign convention on faces. The subdivision operator barycentricSubdivisionLinearMap R X n : C_n → C_n is the signed sum over permutations. The commutation identity below relates barycentricSubdivisionLinearMap R X (n+1) ≫ singularBoundary R X n with singularBoundary R X n ≫ barycentricSubdivisionLinearMap R X n.

theorem SphereOddDegree.AffineBarycentricSubdivision.boundary_barycentricSubdivision_generator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X (n + 1)) : (ModuleCat.Hom.hom (singularBoundary R X n)) ((ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X (n + 1))) (chainGenerator R X (n + 1) σ)) = (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) ((ModuleCat.Hom.hom (singularBoundary R X n)) (chainGenerator R X (n + 1) σ))

Boundary commutation on a generator (chain-map form). On a basis generator [σ], the singular boundary of its subdivision equals the subdivision of its boundary.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap_commutes_boundary (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : CategoryTheory.CategoryStruct.comp (barycentricSubdivisionLinearMap R X (n + 1)) (singularBoundary R X n) = CategoryTheory.CategoryStruct.comp (singularBoundary R X n) (barycentricSubdivisionLinearMap R X n)

Chain-level boundary commutation. Degree-wise barycentric subdivision is a chain map for the singular boundary:

sd ≫ ∂ = ∂ ≫ sd.

This lifts the generator-level cancellation to all chains by coproduct extensionality.

theorem SphereOddDegree.AffineBarycentricSubdivision.boundary_barycentricSubdivision_apply (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (c : ↑(singularChainGroup R X (n + 1))) : (ModuleCat.Hom.hom (singularBoundary R X n)) ((ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X (n + 1))) c) = (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) ((ModuleCat.Hom.hom (singularBoundary R X n)) c)

Pointwise boundary commutation. For every singular chain c,

∂ (sd c) = sd (∂ c).

This is the element-level form of barycentricSubdivisionLinearMap_commutes_boundary.