Documentation

Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

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.

@[instance_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)) ≃ₜ Convexity.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

theorem SimplexCategory.toTopHomeo_naturality {n m : SimplexCategory} (f : n ⟶ m) :

⇑m.toTopHomeo ∘ ⇑(CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) = Convexity.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) = Convexity.StdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) (n.toTopHomeo x)

theorem SimplexCategory.toTopHomeo_symm_naturality {n m : SimplexCategory} (f : n ⟶ m) :

⇑m.toTopHomeo.symm ∘ Convexity.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 : Convexity.StdSimplex ℝ (Fin (n.len + 1))) :

m.toTopHomeo.symm (Convexity.StdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) x) = (CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) (n.toTopHomeo.symm x)

@[instance_reducible]

noncomputable instance instUniqueStdSimplexRealFinHAddNatLenMkOfNat :

Unique (Convexity.StdSimplex ℝ (Fin ({ len := 0 }.len + 1)))

Equations

instUniqueStdSimplexRealFinHAddNatLenMkOfNat = { toInhabited := Convexity.StdSimplex.instInhabited, uniq := instUniqueStdSimplexRealFinHAddNatLenMkOfNat._proof_2 }

@[instance_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.

Instances For

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 : Convexity.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 TopCat.toSSetObjEquiv_symm_naturality {X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (g : C(Convexity.StdSimplex ℝ (Fin (m.len + 1)), ↑X)) :

(CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map f.op)) ((X.toSSetObjEquiv (Opposite.op m)).symm g) = (X.toSSetObjEquiv (Opposite.op n)).symm (g.comp { toFun := Convexity.StdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })

@[simp]

theorem TopCat.toSSetObjEquiv_naturality_apply {X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (x : (toSSet.obj X).obj (Opposite.op m)) (z : Convexity.StdSimplex ℝ (Fin (n.len + 1))) :

((X.toSSetObjEquiv (Opposite.op n)) ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map f.op)) x)) z = ((X.toSSetObjEquiv (Opposite.op m)) x) (Convexity.StdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) z)

@[simp]

theorem TopCat.toSSetObjEquiv_δ_apply {X : TopCat} {n : ℕ} (x : (toSSet.obj X).obj (Opposite.op { len := n + 1 })) (i : Fin (n + 2)) (z : Convexity.StdSimplex ℝ (Fin (n + 1))) :

((X.toSSetObjEquiv (Opposite.op { len := n })) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (toSSet.obj X) i)) x)) z = ((X.toSSetObjEquiv (Opposite.op { len := n + 1 })) x) (Convexity.StdSimplex.map i.succAbove z)

@[simp]

theorem TopCat.toSSetObjEquiv_σ_apply {X : TopCat} {n : ℕ} (x : (toSSet.obj X).obj (Opposite.op { len := n })) (i : Fin (n + 1)) (z : Convexity.StdSimplex ℝ (Fin (n + 2))) :

((X.toSSetObjEquiv (Opposite.op { len := n + 1 })) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (toSSet.obj X) i)) x)) z = ((X.toSSetObjEquiv (Opposite.op { len := n })) x) (Convexity.StdSimplex.map i.predAbove z)

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

noncomputable def TopCat.stdSimplexHomeomorphI :

Convexity.StdSimplex ℝ (Fin 2) ≃ₜ ↑I

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

Equations

TopCat.stdSimplexHomeomorphI = Convexity.StdSimplex.homeomorphI.trans Homeomorph.ulift.symm

Instances For

@[simp]

theorem TopCat.stdSimplexHomeomorphI_vertex_zero :

stdSimplexHomeomorphI (Convexity.StdSimplex.single 0) = 0

@[simp]

theorem TopCat.stdSimplexHomeomorphI_vertex_one :

stdSimplexHomeomorphI (Convexity.StdSimplex.single 1) = 1

@[simp]

theorem TopCat.stdSimplexHomeomorphI_symm_zero :

stdSimplexHomeomorphI.symm 0 = Convexity.StdSimplex.single 0

@[simp]

theorem TopCat.stdSimplexHomeomorphI_symm_one :

stdSimplexHomeomorphI.symm 1 = Convexity.StdSimplex.single 1

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)

Instances For

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

Instances For

@[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_μ (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.ι₁