Barycentric Subdivision Homotopy Formula

0. Functoriality of the pushforward on singular chains

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_id (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : singularChainMap R (CategoryTheory.CategoryStruct.id X) n = CategoryTheory.CategoryStruct.id (singularChainGroup R X n)

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_comp (R : Type) [CommRing R] {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (n : ℕ) : singularChainMap R (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (singularChainMap R f n) (singularChainMap R g n)

theorem SphereOddDegree.AffineBarycentricSubdivision.pushSimplex_continuousMap {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (σ : singularSimplices X n) : singularSimplexAsContinuousMap Y n (pushSimplex f n σ) = (CategoryTheory.ConcreteCategory.hom f).comp (singularSimplexAsContinuousMap X n σ)

1. ∂∂ = 0

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

2. Subdivision in degree 0 is the identity

theorem SphereOddDegree.AffineBarycentricSubdivision.delta0_subsingleton (a b : ↑(Delta 0)) : a = b

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionGenerator_zero (R : Type) [CommRing R] (X : TopCat) (σ : singularSimplices X 0) : barycentricSubdivisionGenerator R X 0 σ = chainGenerator R X 0 σ

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricHomotopyUniversal_zero (R : Type) [CommRing R] : barycentricHomotopyUniversal R 0 = 0

3. Naturality of subdivision and homotopy under pushforward

theorem SphereOddDegree.AffineBarycentricSubdivision.pushSimplex_stdSimplexId (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : pushSimplex (TopCat.ofHom (singularSimplexAsContinuousMap X n σ)) n (stdSimplexIdSingularSimplex n) = σ

theorem SphereOddDegree.AffineBarycentricSubdivision.pushSimplex_barycentricSubdivSimplex {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (σ : singularSimplices X n) : pushSimplex f n (barycentricSubdivSimplex X n π σ) = barycentricSubdivSimplex Y n π (pushSimplex f n σ)

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_barycentricSubdivision_generator (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (σ : singularSimplices X n) : (ModuleCat.Hom.hom (singularChainMap R f n)) (barycentricSubdivisionGenerator R X n σ) = barycentricSubdivisionGenerator R Y n (pushSimplex f n σ)

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_barycentricSubdivision (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (c : ↑(singularChainGroup R X n)) : (ModuleCat.Hom.hom (singularChainMap R f n)) ((ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) c) = (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R Y n)) ((ModuleCat.Hom.hom (singularChainMap R f n)) c)

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_barycentricHomotopy_generator (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (σ : singularSimplices X n) : (ModuleCat.Hom.hom (singularChainMap R f (n + 1))) ((ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) (chainGenerator R X n σ)) = (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R Y n)) (chainGenerator R Y n (pushSimplex f n σ))

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_barycentricHomotopy (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (c : ↑(singularChainGroup R X n)) : (ModuleCat.Hom.hom (singularChainMap R f (n + 1))) ((ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) c) = (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R Y n)) ((ModuleCat.Hom.hom (singularChainMap R f n)) c)

4. The recursion equation for the universal chain

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricHomotopyUniversal_succ_eq (R : Type) [CommRing R] (m : ℕ) : barycentricHomotopyUniversal R (m + 1) = (ModuleCat.Hom.hom (coneLinearMap R (m + 1) (m + 1) (deltaBarycenter (m + 1)))) (chainGenerator R (↧↑(Delta (m + 1))) (m + 1) (stdSimplexIdSingularSimplex (m + 1)) - (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R (↧↑(Delta (m + 1))) (m + 1))) (chainGenerator R (↧↑(Delta (m + 1))) (m + 1) (stdSimplexIdSingularSimplex (m + 1))) - (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R (↧↑(Delta (m + 1))) m)) ((ModuleCat.Hom.hom (singularBoundary R (↧↑(Delta (m + 1))) m)) (chainGenerator R (↧↑(Delta (m + 1))) (m + 1) (stdSimplexIdSingularSimplex (m + 1)))))

5. The boundary term and the chain-homotopy formula

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

Apply the subdivision homotopy to the boundary of a chain, using zero in degree zero.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.homotopyBoundaryTerm_succ (R : Type) [CommRing R] (X : TopCat) (m : ℕ) (c : ↑(singularChainGroup R X (m + 1))) : homotopyBoundaryTerm R X (m + 1) c = (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X m)) ((ModuleCat.Hom.hom (singularBoundary R X m)) c)

theorem SphereOddDegree.AffineBarycentricSubdivision.homotopyBoundaryTerm_zero (R : Type) [CommRing R] (X : TopCat) (c : ↑(singularChainGroup R X 0)) : homotopyBoundaryTerm R X 0 c = 0

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_boundary_apply (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (c : ↑(singularChainGroup R X (n + 1))) : (ModuleCat.Hom.hom (singularBoundary R Y n)) ((ModuleCat.Hom.hom (singularChainMap R f (n + 1))) c) = (ModuleCat.Hom.hom (singularChainMap R f n)) ((ModuleCat.Hom.hom (singularBoundary R X n)) c)

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

6. The chain-homotopy formula ∂H + H∂ = id - sd

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

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