Barycentric Subdivision Homotopy Operator

1. Pushforward of singular chains along a continuous map

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.singularChainMap (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : singularChainGroup R X n ⟶ singularChainGroup R Y n

The degreewise singular-chain map induced by a continuous map.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.singularChainMap R f n = (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).map f).f n

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.pushSimplex {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) (σ : singularSimplices X n) : singularSimplices Y n

Postcompose a singular simplex with a continuous map.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.pushSimplex f n σ = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := n }))) σ

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

theorem SphereOddDegree.AffineBarycentricSubdivision.singularChainMap_boundary (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (singularChainMap R f (n + 1)) (singularBoundary R Y n) = CategoryTheory.CategoryStruct.comp (singularBoundary R X n) (singularChainMap R f n)

2. The barycenter and the identity singular simplex of Δⁿ

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.deltaBarycenter (n : ℕ) : ↑(Delta n)

The barycenter of the standard real simplex.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.deltaBarycenter n = SphereOddDegree.FiniteSimplex.barycenter

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.stdSimplexIdSingularSimplex (n : ℕ) : singularSimplices (↧↑(Delta n)) n

The identity map of the standard simplex viewed as a singular simplex.

Equations

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

3. The homotopy operator built from a universal chain

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.pushUniversalHom (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (T : ↑(singularChainGroup R (↧↑(Delta n)) (n + 1))) (σ : singularSimplices X n) : ↧R ⟶ singularChainGroup R X (n + 1)

Push a universal homotopy chain along a singular simplex and scale by a coefficient.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.homotopyFromUniversal (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (T : ↑(singularChainGroup R (↧↑(Delta n)) (n + 1))) : singularChainGroup R X n ⟶ singularChainGroup R X (n + 1)

Extend a universal homotopy chain to arbitrary singular chains by linearity.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.homotopyFromUniversal R X n T = CategoryTheory.Limits.Sigma.desc (SphereOddDegree.AffineBarycentricSubdivision.pushUniversalHom R X n T)

theorem SphereOddDegree.AffineBarycentricSubdivision.homotopyFromUniversal_generator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (T : ↑(singularChainGroup R (↧↑(Delta n)) (n + 1))) (σ : singularSimplices X n) : (ModuleCat.Hom.hom (homotopyFromUniversal R X n T)) (chainGenerator R X n σ) = (ModuleCat.Hom.hom (singularChainMap R (TopCat.ofHom (singularSimplexAsContinuousMap X n σ)) (n + 1))) T

4. The universal homotopy chain T_n(ι_n)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricHomotopyUniversal (R : Type) [CommRing R] (n : ℕ) : ↑(singularChainGroup R (↧↑(Delta n)) (n + 1))

The recursively coned universal chain witnessing homotopy to barycentric subdivision.

Equations

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

5. The degree-wise homotopy operator

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionHomotopyLinearMap (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : singularChainGroup R X n ⟶ singularChainGroup R X (n + 1)

The degree-raising chain homotopy map induced by the universal subdivision chain.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionHomotopyLinearMap_apply_generator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) (chainGenerator R X n σ) = (ModuleCat.Hom.hom (singularChainMap R (TopCat.ofHom (singularSimplexAsContinuousMap X n σ)) (n + 1))) (barycentricHomotopyUniversal R n)

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionHomotopyLinearMap_map_zero (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) 0 = 0

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionHomotopyLinearMap_map_add (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (c d : ↑(singularChainGroup R X n)) : (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) (c + d) = (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) c + (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) d

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionHomotopyLinearMap_smul (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (a : R) (c : ↑(singularChainGroup R X n)) : (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) (a • c) = a • (ModuleCat.Hom.hom (barycentricSubdivisionHomotopyLinearMap R X n)) c