Barycentric Subdivision Iter

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

The N-fold barycentric subdivision chain map sd^N, defined by sd^0 = 𝟙 and sd^(N+1) = sd ≫ sd^N.

Equations

• One or more equations did not get rendered due to their size.
• SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterChainMap R X 0 = CategoryTheory.CategoryStruct.id (SphereOddDegree.AffineBarycentricSubdivision.singularChainComplex R X)

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterChainMap_zero (R : Type) [CommRing R] (X : TopCat) : barycentricSubdivisionIterChainMap R X 0 = CategoryTheory.CategoryStruct.id (singularChainComplex R X)

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterChainMap_succ (R : Type) [CommRing R] (X : TopCat) (N : ℕ) : barycentricSubdivisionIterChainMap R X (N + 1) = CategoryTheory.CategoryStruct.comp (barycentricSubdivisionChainMap R X) (barycentricSubdivisionIterChainMap R X N)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) : ↑(singularChainGroup R X n) →ₗ[R] ↑(singularChainGroup R X n)

The degree-n component of sd^N as an R-linear map.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterLinearMap_zero (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (c : ↑(singularChainGroup R X n)) : (barycentricSubdivisionIterLinearMap R X 0 n) c = c

In iterate 0, the degree-wise map is the identity.

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

The degree-wise successor formula (sd^(N+1))_n c = (sd^N)_n (sd_n c).

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

sd^N commutes with the boundary (degree-wise, pointwise form). This is the chain-map condition of barycentricSubdivisionIterChainMap.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyLinearMap (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) : ↑(singularChainGroup R X n) →ₗ[R] ↑(singularChainGroup R X (n + 1))

The explicit accumulated homotopy operator H^(N) = Σ_{r=0}^{N-1} (sd^r) ∘ H, defined by H^(0) = 0 and H^(N+1)_n = H^(N)_n + (sd^N)_{n+1} ∘ H_n.

Equations

• One or more equations did not get rendered due to their size.
• SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyLinearMap R X 0 n = 0

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyLinearMap_zero (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (c : ↑(singularChainGroup R X n)) : (barycentricSubdivisionIterHomotopyLinearMap R X 0 n) c = 0

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyLinearMap_succ (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) (c : ↑(singularChainGroup R X n)) : (barycentricSubdivisionIterHomotopyLinearMap R X (N + 1) n) c = (barycentricSubdivisionIterHomotopyLinearMap R X N n) c + (barycentricSubdivisionIterLinearMap R X N (n + 1)) ((ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) c)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyBoundaryTerm (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) (c : ↑(singularChainGroup R X n)) : ↑(singularChainGroup R X n)

The degree-wise "H ∘ ∂" term of the iterated homotopy formula. In degree 0 it is 0; in degree m+1 it is H^(N)_m (∂_m c). This matches the library's index convention ∂ : C_{n+1} → C_n = singularBoundary R X n, exactly as homotopyBoundaryTerm did for the one-step formula.

Equations

• One or more equations did not get rendered due to their size.
• SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyBoundaryTerm R X N 0 c_2 = 0

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyBoundaryTerm_zero (R : Type) [CommRing R] (X : TopCat) (N : ℕ) (c : ↑(singularChainGroup R X 0)) : barycentricSubdivisionIterHomotopyBoundaryTerm R X N 0 c = 0

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyBoundaryTerm_succ (R : Type) [CommRing R] (X : TopCat) (N m : ℕ) (c : ↑(singularChainGroup R X (m + 1))) : barycentricSubdivisionIterHomotopyBoundaryTerm R X N (m + 1) c = (barycentricSubdivisionIterHomotopyLinearMap R X N m) ((ModuleCat.Hom.hom (singularBoundary R X m)) c)

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterHomotopyBoundaryTerm_succ_iter (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) (c : ↑(singularChainGroup R X n)) : barycentricSubdivisionIterHomotopyBoundaryTerm R X (N + 1) n c = barycentricSubdivisionIterHomotopyBoundaryTerm R X N n c + (barycentricSubdivisionIterLinearMap R X N n) (homotopyBoundaryTerm R X n c)

Recursion for the boundary term. Increasing the iterate by one adds the contribution (sd^N)_n (H(∂ c)) from the one-step boundary term.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIterChainHomotopicId (R : Type) [CommRing R] (X : TopCat) (N : ℕ) : Homotopy (barycentricSubdivisionIterChainMap R X N) (CategoryTheory.CategoryStruct.id (singularChainComplex R X))

Every iterate of barycentric subdivision is chain-homotopic to the identity.

Equations

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

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

sd^N induces the identity on homology.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionIter_boundary_formula (R : Type) [CommRing R] (X : TopCat) (N n : ℕ) (c : ↑(singularChainGroup R X n)) : c - (barycentricSubdivisionIterLinearMap R X N n) c = (ModuleCat.Hom.hom (singularBoundary R X n)) ((barycentricSubdivisionIterHomotopyLinearMap R X N n) c) + barycentricSubdivisionIterHomotopyBoundaryTerm R X N n c

The iterated barycentric subdivision boundary formula.

For every singular chain c ∈ C_n(X; R) and every N,

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

where sd^N = barycentricSubdivisionIterLinearMap, H^(N) = barycentricSubdivisionIterHomotopyLinearMap is the explicit accumulated homotopy, ∂ = singularBoundary, and the term H^(N)(∂ c) is packaged degree-wise as barycentricSubdivisionIterHomotopyBoundaryTerm (which is H^(N)_{n-1}(∂_{n-1} c) in positive degree and 0 in degree 0, matching the library's index convention ∂ : C_{n+1} → C_n = singularBoundary R X n).