Barycentric Subdivision Chain Homotopy

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainHomotopyHom (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) : (singularChainComplex R X).X p ⟶ (singularChainComplex R X).X q

The components of the chain homotopy between barycentric subdivision and the identity: in the slot (p, q) it is -H_p when q = p + 1 and 0 otherwise.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainHomotopyHom_succ (R : Type) [CommRing R] (X : TopCat) (p : ℕ) : barycentricSubdivisionChainHomotopyHom R X p (p + 1) = -barycentricSubdivisionHomotopyLinearMap R X p

In the relevant slot, the homotopy component is -H_p.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainHomotopyHom_zero (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) (h : p + 1 ≠ q) : barycentricSubdivisionChainHomotopyHom R X p q = 0

Outside the relevant slot, the homotopy component vanishes.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainHomotopy_comm (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : (barycentricSubdivisionChainMap R X).f n = (dNext n) (barycentricSubdivisionChainHomotopyHom R X) + (prevD n) (barycentricSubdivisionChainHomotopyHom R X) + (CategoryTheory.CategoryStruct.id (singularChainComplex R X)).f n

The chain-homotopy identity in Mathlib's sign convention. For every degree n, the degree-n component of the subdivision chain map equals dNext + prevD of the homotopy operator plus the identity component. This is the comm field of the Homotopy structure, isolated as a theorem.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionChainHomotopicId (R : Type) [CommRing R] (X : TopCat) : Homotopy (barycentricSubdivisionChainMap R X) (CategoryTheory.CategoryStruct.id (singularChainComplex R X))

Barycentric subdivision is chain-homotopic to the identity.

A Homotopy between the barycentric subdivision chain map and the identity chain map of the singular chain complex, built from the homotopy operator -H.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivision_induces_identity_on_homology (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : HomologicalComplex.homologyMap (barycentricSubdivisionChainMap R X) n = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology (singularChainComplex R X) n)

Induced map on homology is the identity (named form).

Since barycentric subdivision is chain-homotopic to the identity, it induces the identity on every singular homology group.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivision_homologyMap_eq_id (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : HomologicalComplex.homologyMap (barycentricSubdivisionChainMap R X) n = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology (singularChainComplex R X) n)

Induced map on homology is the identity (alias). Same statement as barycentricSubdivision_induces_identity_on_homology, kept under the design's preferred name.

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

Chain-level boundary witness.

The difference sd(c) - c is the (negative of the) chain-homotopy boundary ∂ H(c) + H(∂ c). Concretely, with the library's index convention,

sd(c) - c = -(∂ H(c) + H(∂ c)),

where H(∂ c) is homotopyBoundaryTerm R X n c. This is the explicit formula needed later to show that a cycle and its subdivision represent the same homology class.