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

Equations

• instMonoidalTopCatSSetToSSet = CategoryTheory.Functor.Monoidal.ofChosenFiniteProducts TopCat.toSSet

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.

Equations

• n.toTopHomeo = (TopCat.homeoOfIso (SSet.toTopSimplex.app n)).trans Homeomorph.ulift

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 ({ len := 0 }.len + 1)))

Equations

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

@[implicit_reducible]

noncomputable instance instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat : Unique ↑(SSet.toTop.obj (SSet.stdSimplex.obj { len := 0 }))

Equations

• instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat = { len := 0 }.toTopHomeo.unique

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

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

Equations

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

theorem TopCat.toSSetObj₀Equiv_apply {X : TopCat} (a✝ : (toSSet.obj X).obj (Opposite.op { len := 0 })) : toSSetObj₀Equiv a✝ = ((X.toSSetObjEquiv (Opposite.op { len := 0 })) a✝) default

theorem TopCat.toSSetObj₀Equiv_symm_apply {X : TopCat} (a✝ : ↑X) : toSSetObj₀Equiv.symm a✝ = (X.toSSetObjEquiv (Opposite.op { len := 0 })).symm { toFun := fun (x : ↑(stdSimplex ℝ (Fin (0 + 1)))) => a✝, continuous_toFun := ⋯ }

@[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 { len := 0 }) ⟶ X) : (sSetTopAdj.homEquiv (SSet.stdSimplex.obj { len := 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.

Equations

• TopCat.stdSimplexHomeomorphI = stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm

noncomputable def SSet.stdSimplex.toTopObjIsoI : toTop.obj (stdSimplex.obj { len := 1 }) ≅ TopCat.I

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

Equations

• SSet.stdSimplex.toTopObjIsoI = TopCat.isoOfHomeo ({ len := 1 }.toTopHomeo.trans TopCat.stdSimplexHomeomorphI)

noncomputable def SSet.stdSimplex.toSSetObjI : stdSimplex.obj { len := 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.

Equations

• SSet.stdSimplex.toSSetObjI = (sSetTopAdj.homEquiv (SSet.stdSimplex.obj { len := 1 }) TopCat.I) SSet.stdSimplex.toTopObjIsoI.hom

@[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 : (CategoryTheory.ConcreteCategory.hom (toSSetObjI.app (Opposite.op { len := 0 }))) (const 1 0 (Opposite.op { len := 0 })) = TopCat.toSSetObj₀Equiv.symm 0

@[simp]

theorem SSet.stdSimplex.toSSetObj_app_const_one : (CategoryTheory.ConcreteCategory.hom (toSSetObjI.app (Opposite.op { len := 0 }))) (const 1 1 (Opposite.op { len := 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