Barycentric subdivision is chain homotopic to the identity

This file constructs the prism operator P of barycentric subdivision S and proves the chain homotopy formula ∂ P + P ∂ = 1 - S, first on affine chains and then on singular chains with coefficients in an object R of a preadditive category with coproducts. On the standard simplex Δᵏ, the operator is given by Hatcher's recursion P Δᵏ = b · (Δᵏ - S Δᵏ - P ∂Δᵏ), where b is the cone from the barycenter of Δᵏ; it is extended to all affine chains, and to singular chains, by naturality. Consequently barycentric subdivision induces the identity on singular homology. This is the step of the small-chains theorem that replaces a singular chain by its iterated subdivision without changing its homology class.

Main definitions and results

• TauCeti.AffineChain.prism: the prism operator on affine chains in a convex space, with TauCeti.AffineChain.boundary_prism_add_prism_boundary: ∂ (P c) + P (∂ c) = c - S c.
• TauCeti.singularPrismX: the prism operator on singular chains, natural in the space (TauCeti.singularPrismX_naturality).
• TauCeti.singularSubdivisionHomotopy: the chain homotopy from the identity of the singular chain complex to its barycentric subdivision.
• TauCeti.homologyMap_singularSubdivisionChainMap: barycentric subdivision induces the identity on singular homology.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, step (2).

def TauCeti.AffineChain.prismModel (k : ℕ) : (Fin (k + 2) → Convexity.StdSimplex ℝ (Fin (k + 1))) →₀ ℤ

The prism operator on the standard simplex, defined by Hatcher's recursion P Δᵏ = b · (Δᵏ - S Δᵏ - P ∂Δᵏ), where b is the barycenter of Δᵏ, S is the barycentric subdivision and P ∂Δᵏ is computed from P Δᵏ⁻¹ through the facet inclusions.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.AffineChain.prismModel 0 = 0

noncomputable def TauCeti.AffineChain.prism (E : Type u_1) [Convexity.ConvexSpace ℝ E] (k : ℕ) : ((Fin (k + 1) → E) →₀ ℤ) →ₗ[ℤ] (Fin (k + 2) → E) →₀ ℤ

The prism operator on affine chains: a vertex tuple v is sent to the image of the prism operator of the standard simplex under the affine map with vertices v. It is a chain homotopy between the identity and the barycentric subdivision (TauCeti.AffineChain.boundary_prism_add_prism_boundary).

Equations

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

@[simp]

theorem TauCeti.AffineChain.prism_single {E : Type u_1} [Convexity.ConvexSpace ℝ E] {k : ℕ} (v : Fin (k + 1) → E) (a : ℤ) : (prism E k) (Finsupp.single v a) = a • (map (⇑(Convexity.StdSimplex.affineMapMk v)) (k + 1)) (prismModel k)

theorem TauCeti.AffineChain.prism_simplex (k : ℕ) : (prism (Convexity.StdSimplex ℝ (Fin (k + 1))) k) (simplex k) = prismModel k

theorem TauCeti.AffineChain.prism_boundary_simplex (k : ℕ) : (prism (Convexity.StdSimplex ℝ (Fin (k + 1 + 1))) k) ((boundary (Convexity.StdSimplex ℝ (Fin (k + 1 + 1))) k) (simplex (k + 1))) = ∑ j : Fin (k + 2), (-1) ^ ↑j • (map (Convexity.StdSimplex.map j.succAbove) (k + 1)) (prismModel k)

theorem TauCeti.AffineChain.map_prism {E : Type u_1} {F : Type u_2} [Convexity.ConvexSpace ℝ E] [Convexity.ConvexSpace ℝ F] (f : Convexity.ConvexSpace.AffineMap ℝ E F) {k : ℕ} (c : (Fin (k + 1) → E) →₀ ℤ) : (map (⇑f) (k + 1)) ((prism E k) c) = (prism F k) ((map (⇑f) k) c)

The prism operator is natural under affine maps.

@[simp]

theorem TauCeti.AffineChain.prism_zero {E : Type u_1} [Convexity.ConvexSpace ℝ E] : prism E 0 = 0

@[simp]

theorem TauCeti.AffineChain.prismModel_zero : prismModel 0 = 0

theorem TauCeti.AffineChain.prismModel_succ (k : ℕ) : prismModel (k + 1) = (cone Convexity.StdSimplex.barycenter (k + 1)) (simplex (k + 1) - (subdivision (Convexity.StdSimplex ℝ (Fin (k + 1 + 1))) (k + 1)) (simplex (k + 1)) - (prism (Convexity.StdSimplex ℝ (Fin (k + 1 + 1))) k) ((boundary (Convexity.StdSimplex ℝ (Fin (k + 1 + 1))) k) (simplex (k + 1))))

theorem TauCeti.AffineChain.boundary_prism_add_prism_boundary {E : Type u_1} [Convexity.ConvexSpace ℝ E] (k : ℕ) (c : (Fin (k + 2) → E) →₀ ℤ) : (boundary E (k + 1)) ((prism E (k + 1)) c) + (prism E k) ((boundary E k) c) = c - (subdivision E (k + 1)) c

The prism operator is a chain homotopy from the identity to the barycentric subdivision. For an affine chain c of positive degree, ∂ (P c) + P (∂ c) = c - S c.

noncomputable def TauCeti.singularPrismX {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) (n : ℕ) : ((TopCat.toSSet.obj X).chainComplex R).X n ⟶ ((TopCat.toSSet.obj X).chainComplex R).X (n + 1)

The prism operator on singular n-chains of X with coefficients in R: the summand of a singular simplex σ is sent to the push-forward along σ of the prism operator of the standard simplex.

Equations

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

@[simp]

theorem TauCeti.ιChainComplex_singularPrismX {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (singularPrismX R X n) = (AffineChain.singularChain R ((X.toSSetObjEquiv (Opposite.op { len := n })) σ) (n + 1)) (AffineChain.prismModel n)

@[simp]

theorem TauCeti.ιChainComplex_singularPrismX_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) {Z : C} (h : ((TopCat.toSSet.obj X).chainComplex R).X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp (singularPrismX R X n) h) = CategoryTheory.CategoryStruct.comp ((AffineChain.singularChain R ((X.toSSetObjEquiv (Opposite.op { len := n })) σ) (n + 1)) (AffineChain.prismModel n)) h

@[simp]

theorem TauCeti.singularPrismX_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) : singularPrismX R X 0 = 0

The singular prism operator vanishes on 0-chains.

theorem TauCeti.singularPrismX_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) {Y : TopCat} (f : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (TopCat.toSSet.map f) R).f n) (singularPrismX R Y n) = CategoryTheory.CategoryStruct.comp (singularPrismX R X n) ((SSet.chainComplexMap (TopCat.toSSet.map f) R).f (n + 1))

The prism operator is natural in the space.

theorem TauCeti.singularPrismX_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) {Y : TopCat} (f : X ⟶ Y) (n : ℕ) {Z : C} (h : ((TopCat.toSSet.obj Y).chainComplex R).X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (TopCat.toSSet.map f) R).f n) (CategoryTheory.CategoryStruct.comp (singularPrismX R Y n) h) = CategoryTheory.CategoryStruct.comp (singularPrismX R X n) (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (TopCat.toSSet.map f) R).f (n + 1)) h)

The prism operator is natural in the space.

theorem TauCeti.singularPrismX_boundary_add_boundary_singularPrismX {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) (n : ℕ) : CategoryTheory.CategoryStruct.comp (((TopCat.toSSet.obj X).chainComplex R).d (n + 1) n) (singularPrismX R X n) + CategoryTheory.CategoryStruct.comp (singularPrismX R X (n + 1)) (((TopCat.toSSet.obj X).chainComplex R).d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.id (((TopCat.toSSet.obj X).chainComplex R).X (n + 1)) - singularSubdivisionX R X (n + 1)

The chain homotopy formula for the singular prism operator in positive degrees: ∂ P + P ∂ = 1 - S.

noncomputable def TauCeti.singularSubdivisionHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) : Homotopy (CategoryTheory.CategoryStruct.id ((TopCat.toSSet.obj X).chainComplex R)) (singularSubdivisionChainMap R X)

Barycentric subdivision is chain homotopic to the identity. The singular prism operator is a chain homotopy from the identity of the singular chain complex of X with coefficients in R to its barycentric subdivision.

Equations

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

@[simp]

theorem TauCeti.singularSubdivisionHomotopy_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) (n : ℕ) : (singularSubdivisionHomotopy R X).hom n (n + 1) = singularPrismX R X n

@[simp]

theorem TauCeti.homologyMap_singularSubdivisionChainMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (X : TopCat) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : HomologicalComplex.homologyMap (singularSubdivisionChainMap R X) n = CategoryTheory.CategoryStruct.id (HomologicalComplex.homology ((TopCat.toSSet.obj X).chainComplex R) n)

Barycentric subdivision induces the identity on singular homology.