Singular H0

noncomputable def SphereOddDegree.pointSimplex (X : TopCat) (x : ↑X) : singularSimplices X 0

The 0-simplex of X sitting at the point x.

Equations

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

noncomputable def SphereOddDegree.pathSimplex {X : TopCat} {a b : ↑X} (p : Path a b) : singularSimplices X 1

The singular 1-simplex of X obtained from a path, by reparametrising the standard 1-simplex Δ¹ as the unit interval.

Equations

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

theorem SphereOddDegree.test_coface0 (x : ↑(AffineBarycentricSubdivision.Delta 0)) : (AffineBarycentricSubdivision.cofaceTop 0 0) x = ⟨Pi.single 1 1, ⋯⟩

theorem SphereOddDegree.test_coface1 (x : ↑(AffineBarycentricSubdivision.Delta 0)) : (AffineBarycentricSubdivision.cofaceTop 0 1) x = ⟨Pi.single 0 1, ⋯⟩

theorem SphereOddDegree.faceSimplex_pathSimplex_0 {X : TopCat} {a b : ↑X} (p : Path a b) : AlexanderWhitney.faceSimplex X 0 0 (pathSimplex p) = pointSimplex X b

theorem SphereOddDegree.faceSimplex_pathSimplex_1 {X : TopCat} {a b : ↑X} (p : Path a b) : AlexanderWhitney.faceSimplex X 0 1 (pathSimplex p) = pointSimplex X a

theorem SphereOddDegree.boundary_pathSimplex {X : TopCat} {a b : ↑X} (p : Path a b) : (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary ℤ X 0)) (AffineBarycentricSubdivision.chainGenerator ℤ X 1 (pathSimplex p)) = AffineBarycentricSubdivision.chainGenerator ℤ X 0 (pointSimplex X b) - AffineBarycentricSubdivision.chainGenerator ℤ X 0 (pointSimplex X a)

theorem SphereOddDegree.chainGenerator_sub_mem_range_of_path {X : TopCat} {a b : ↑X} (p : Path a b) : AffineBarycentricSubdivision.chainGenerator ℤ X 0 (pointSimplex X b) - AffineBarycentricSubdivision.chainGenerator ℤ X 0 (pointSimplex X a) ∈ (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary ℤ X 0)).range

theorem SphereOddDegree.pointSimplex_singularSimplex {X : TopCat} (σ : singularSimplices X 0) : pointSimplex X ((AffineBarycentricSubdivision.singularSimplexAsContinuousMap X 0 σ) (FiniteSimplex.vertex 0)) = σ

theorem SphereOddDegree.chainGenerator_sub_mem_range {X : TopCat} [PathConnectedSpace ↑X] (σ τ : singularSimplices X 0) : AffineBarycentricSubdivision.chainGenerator ℤ X 0 σ - AffineBarycentricSubdivision.chainGenerator ℤ X 0 τ ∈ (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary ℤ X 0)).range

noncomputable def SphereOddDegree.aug (X : TopCat) : AffineBarycentricSubdivision.singularChainGroup ℤ X 0 ⟶ ↧ℤ

The augmentation sending every singular zero-simplex to one.

Equations

• SphereOddDegree.aug X = CategoryTheory.Limits.Sigma.desc fun (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) => CategoryTheory.CategoryStruct.id ↧ℤ

@[simp]

theorem SphereOddDegree.aug_generator {X : TopCat} (σ : singularSimplices X 0) : (ModuleCat.Hom.hom (aug X)) (AffineBarycentricSubdivision.chainGenerator ℤ X 0 σ) = 1

theorem SphereOddDegree.aug_boundary {X : TopCat} (c : ↑(AffineBarycentricSubdivision.singularChainGroup ℤ X 1)) : (ModuleCat.Hom.hom (aug X)) ((ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary ℤ X 0)) c) = 0

theorem SphereOddDegree.sub_aug_smul_basept_mem_range {X : TopCat} [PathConnectedSpace ↑X] (b : ↑X) (c : ↑(AffineBarycentricSubdivision.singularChainGroup ℤ X 0)) : c - (ModuleCat.Hom.hom (aug X)) c • AffineBarycentricSubdivision.chainGenerator ℤ X 0 (pointSimplex X b) ∈ (ModuleCat.Hom.hom (AffineBarycentricSubdivision.singularBoundary ℤ X 0)).range