Naturality of singular simplices

The identification of singular simplices with continuous maps from standard simplices commutes with continuous maps, which act by postcomposition; in particular, so does the identification of points with singular zero-simplices. Faces of singular simplices obtained by precomposition with affine simplices are also expressed in terms of their vertex maps. This transfers naturality of simplicial vertex classes to singular homology, giving naturality of the basepoint section of the augmentation in TauCeti.singularHomology₀Section_naturality. Along an inducing map, a singular simplex of the target is induced from the source exactly when its image lies in the range (Topology.IsInducing.mem_range_toSSet_map_app_iff).

@[simp]

theorem TauCeti.TopCat.toSSet_map_app_toSSetObj₀Equiv_symm {X Y : TopCat} (f : X ⟶ Y) (x : ↑X) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := 0 }))) (TopCat.toSSetObj₀Equiv.symm x) = TopCat.toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) x)

Mapping the singular vertex of a point gives the singular vertex of its image.

@[simp]

theorem TauCeti.TopCat.toSSetObjEquiv_toSSet_map_app {X Y : TopCat} (f : X ⟶ Y) {n : SimplexCategoryᵒᵖ} (σ : (TopCat.toSSet.obj X).obj n) : (Y.toSSetObjEquiv n) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) σ) = (CategoryTheory.ConcreteCategory.hom f).comp ((X.toSSetObjEquiv n) σ)

The map of singular simplicial sets induced by a continuous map acts on singular simplices by postcomposition.

@[simp]

theorem TauCeti.TopCat.toSSet_map_app_toSSetObjEquiv_symm {X Y : TopCat} (f : X ⟶ Y) {n : SimplexCategoryᵒᵖ} (g : C(Convexity.StdSimplex ℝ (Fin ((Opposite.unop n).len + 1)), ↑X)) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) ((X.toSSetObjEquiv n).symm g) = (Y.toSSetObjEquiv n).symm ((CategoryTheory.ConcreteCategory.hom f).comp g)

The map of singular simplicial sets induced by a continuous map sends the singular simplex of a continuous map g from a standard simplex to that of its composite with the map.

@[simp]

theorem TauCeti.TopCat.δ_toSSetObjEquiv_symm_comp_affineMapMk {X : TopCat} {m n : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) (v : Fin (n + 2) → Convexity.StdSimplex ℝ (Fin (m + 1))) (k : Fin (n + 2)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) k)) ((X.toSSetObjEquiv (Opposite.op { len := n + 1 })).symm (σ.comp (Convexity.StdSimplex.continuousAffineMapMk v))) = (X.toSSetObjEquiv (Opposite.op { len := n })).symm (σ.comp (Convexity.StdSimplex.continuousAffineMapMk (v ∘ k.succAbove)))

Precomposing a singular simplex with the affine simplex with vertices v, and then with the inclusion of a facet, is precomposing it with the affine simplex with the restricted vertices.

@[simp]

theorem TauCeti.TopCat.toSSetObjEquiv_symm_comp_affineMapMk_δ {X : TopCat} {m n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := m + 1 })) (v : Fin (n + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) (j : Fin (m + 2)) : (X.toSSetObjEquiv (Opposite.op { len := n })).symm (((X.toSSetObjEquiv (Opposite.op { len := m })) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) j)) σ)).comp (Convexity.StdSimplex.continuousAffineMapMk v)) = (X.toSSetObjEquiv (Opposite.op { len := n })).symm (((X.toSSetObjEquiv (Opposite.op { len := m + 1 })) σ).comp (Convexity.StdSimplex.continuousAffineMapMk (Convexity.StdSimplex.map j.succAbove ∘ v)))

Precomposing a facet of a singular simplex with the affine simplex with vertices v is precomposing the singular simplex with the affine simplex with the pushed-forward vertices.

theorem Topology.IsInducing.mem_range_toSSet_map_app_iff {X Y : TopCat} {f : Y ⟶ X} (hf : IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (n : SimplexCategoryᵒᵖ) (σ : (TopCat.toSSet.obj X).obj n) : σ ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app n)) ↔ Set.range ⇑((X.toSSetObjEquiv n) σ) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f)

A singular simplex of X is induced from Y along an inducing map f : Y ⟶ X exactly when its image lies in the range of f.