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.

source

@[implicit_reducible]

noncomputable instance instMonoidalTopCatSSetToSSet :

TopCat.toSSet.Monoidal

Equations

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

source

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

Instances For

source

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

source

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)

source

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

source

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)

source

@[implicit_reducible]

instance instUniqueElemForallFinHAddNatLenMkOfNatRealStdSimplex :

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

Equations

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

source

@[implicit_reducible]

noncomputable instance instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat :

Unique ↑(SSet.toTop.obj (SSet.stdSimplex.obj (SimplexCategory.mk 0)))

Equations

instUniqueCarrierObjSSetTopCatToTopSimplexCategoryStdSimplexMkOfNatNat = (SimplexCategory.mk 0).toTopHomeo.unique

source

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.

Equations

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

Instances For

source

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✝)

source

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✝)

source

@[simp]