Properties of the geometric realization

In this file, we introduce some API in order to study the geometric realization functor (and its right adjoint the singular simplicial set functor):

• SimplexCategory.toTopHomeo: the homeomorphism between the geometric realization of Δ[n] and stdSimplex ℝ (Fin (n + 1));
• TopCat.toSSetObj₀Equiv : toSSet.obj X _⦋0⦌ ≃ X for X : TopCat;
• SSet.stdSimplex.toTopObjIsoI : |Δ[1]| ≅ TopCat.I;
• SSet.stdSimplex.toSSetObjI : Δ[1] ⟶ TopCat.toSSet.obj TopCat.I: the morphism corresponding to toTopObjIsoI.hom by adjunction.

@[implicit_reducible]

noncomputable instance instMonoidalTopCatSSetToSSet : TopCat.toSSet.Monoidal

noncomputable def SimplexCategory.toTopHomeo (n : SimplexCategory) : ↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) ≃ₜ ↑(stdSimplex ℝ (Fin (n.len + 1)))

The homeomorphism between the topological realization of a standard simplex in SSet and the corresponding topological standard simplex.

theorem SimplexCategory.toTopHomeo_naturality {n m : SimplexCategory} (f : n ⟶ m) : ⇑m.toTopHomeo ∘ ⇑(CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) = stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo

theorem SimplexCategory.toTopHomeo_naturality_apply {n m : SimplexCategory} (f : n ⟶ m) (x : ↑(SSet.toTop.obj (SSet.stdSimplex.obj n))) : m.toTopHomeo ((CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) x) = stdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) (n.toTopHomeo x)

theorem SimplexCategory.toTopHomeo_symm_naturality {n m : SimplexCategory} (f : n ⟶ m) : ⇑m.toTopHomeo.symm ∘ stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) ∘ ⇑n.toTopHomeo.symm

theorem SimplexCategory.toTopHomeo_symm_naturality_apply {n m : SimplexCategory} (f : n ⟶ m) (x : ↑(stdSimplex ℝ (Fin (n.len + 1)))) : m.toTopHomeo.symm (stdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) x) = (CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) (n.toTopHomeo.symm x)

@[implicit_reducible]

instance instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex : Unique ↑(stdSimplex ℝ (Fin ((SimplexCategory.mk 0).len + 1)))

@[implicit_reducible]

noncomputable instance instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat : Unique ↑(SSet.toTop.obj (SSet.stdSimplex.obj (SimplexCategory.mk 0)))

noncomputable def TopCat.toSSetObj₀Equiv {X : TopCat} : (toSSet.obj X).obj (Opposite.op (SimplexCategory.mk 0)) ≃ ↑X

Given X : TopCat, this is the bijection between 0-simplices of the singular simplicial set of X and X.

theorem TopCat.toSSetObj₀Equiv_apply {X : TopCat} (a✝ : (toSSet.obj X).obj (Opposite.op (SimplexCategory.mk 0))) : toSSetObj₀Equiv a✝ = { toFun := fun (f : C(↑(stdSimplex ℝ (Fin (0 + 1))), ↑X)) => f default, invFun := fun (x : ↑X) => { toFun := fun (x_1 : ↑(stdSimplex ℝ (Fin (0 + 1)))) => x, continuous_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ } ((X.toSSetObjEquiv (Opposite.op (SimplexCategory.mk 0))) a✝)

theorem TopCat.toSSetObj₀Equiv_symm_apply {X : TopCat} (a✝ : ↑X) : toSSetObj₀Equiv.symm a✝ = (X.toSSetObjEquiv (Opposite.op (SimplexCategory.mk 0))).symm ({ toFun := fun (f : C(↑(stdSimplex ℝ (Fin (0 + 1))), ↑X)) => f default, invFun := fun (x : ↑X) => { toFun := fun (x_1 : ↑(stdSimplex ℝ (Fin (0 + 1)))) => x, continuous_toFun := ⋯ }, left_inv := ⋯, right_inv := ⋯ }.symm a✝)

@[simp]

theorem TopCat.toSSet_map_const (X : TopCat) {Y : TopCat} (y : ↑Y) : toSSet.map (const y) = SSet.const (toSSetObj₀Equiv.symm y)

theorem sSetTopAdj_homEquiv_stdSimplex_zero {X : TopCat} (f : SSet.toTop.obj (SSet.stdSimplex.obj (SimplexCategory.mk 0)) ⟶ X) : (sSetTopAdj.homEquiv (SSet.stdSimplex.obj (SimplexCategory.mk 0)) X) f = SSet.const (TopCat.toSSetObj₀Equiv.symm ((CategoryTheory.ConcreteCategory.hom f) default))

def TopCat.stdSimplexHomeomorphI : ↑(stdSimplex ℝ (Fin 2)) ≃ₜ ↑I

The standard topological simplex of dimension 1 is homeomorphic to TopCat.I.

noncomputable def SSet.stdSimplex.toTopObjIsoI : toTop.obj (stdSimplex.obj (SimplexCategory.mk 1)) ≅ TopCat.I

The geometric realization of Δ[1] is isomorphic to TopCat.I.

noncomputable def SSet.stdSimplex.toSSetObjI : stdSimplex.obj (SimplexCategory.mk 1) ⟶ TopCat.toSSet.obj TopCat.I

The canonical morphism Δ[1] ⟶ TopCat.toSSet.obj TopCat.I: by adjunction, it corresponds to the isomorphism toTopObjIsoI : |Δ[1]| ≅ TopCat.I.

@[simp]

theorem SSet.stdSimplex.δ_one_toSSetObjI : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

@[simp]

theorem SSet.stdSimplex.δ_zero_toSSetObjI : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) toSSetObjI = SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

@[simp]

theorem SSet.stdSimplex.toSSetObj_app_const_zero : toSSetObjI.app (Opposite.op (SimplexCategory.mk 0)) (const 1 0 (Opposite.op (SimplexCategory.mk 0))) = TopCat.toSSetObj₀Equiv.symm 0

@[simp]

theorem SSet.stdSimplex.toSSetObj_app_const_one : toSSetObjI.app (Opposite.op (SimplexCategory.mk 0)) (const 1 1 (Opposite.op (SimplexCategory.mk 0))) = TopCat.toSSetObj₀Equiv.symm 1

@[simp]

theorem SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ (X : TopCat) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) toSSetObjI) (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I)) = TopCat.toSSet.map TopCat.ι₀

@[simp]

theorem SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ_assoc (X : TopCat) {Z : SSet} (h : TopCat.toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) toSSetObjI) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I) h)) = CategoryTheory.CategoryStruct.comp (TopCat.toSSet.map TopCat.ι₀) h

@[simp]

theorem SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ (X : TopCat) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) toSSetObjI) (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I)) = TopCat.toSSet.map TopCat.ι₁

@[simp]

theorem SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ_assoc (X : TopCat) {Z : SSet} (h : TopCat.toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X TopCat.I) ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (TopCat.toSSet.obj X) toSSetObjI) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ TopCat.toSSet X TopCat.I) h)) = CategoryTheory.CategoryStruct.comp (TopCat.toSSet.map TopCat.ι₁) h