Topological simplices

We define the natural functor from SimplexCategory to TopCat sending [n] to the topological n-simplex. This is used to define TopCat.toSSet in AlgebraicTopology.SingularSet.

instance SimplexCategory.instFintypeObjForget (x : SimplexCategory) : Fintype (CategoryTheory.ConcreteCategory.forget.obj x)

Equations

• x.instFintypeObjForget = inferInstanceAs (Fintype (Fin (x.len + 1)))

def SimplexCategory.toTopObj (x : SimplexCategory) : Set ((CategoryTheory.forget SimplexCategory).obj x → NNReal)

The topological simplex associated to x : SimplexCategory. This is the object part of the functor SimplexCategory.toTop.

Equations

• x.toTopObj = {f : (CategoryTheory.forget SimplexCategory).obj x → NNReal | ∑ i : (CategoryTheory.forget SimplexCategory).obj x, f i = 1}

instance SimplexCategory.instCoeFunElemForallObjForgetNNRealToTopObj (x : SimplexCategory) : CoeFun ↑x.toTopObj fun (x_1 : ↑x.toTopObj) => (CategoryTheory.forget SimplexCategory).obj x → NNReal

Equations

• x.instCoeFunElemForallObjForgetNNRealToTopObj = { coe := fun (f : ↑x.toTopObj) => ↑f }

theorem SimplexCategory.toTopObj.ext_iff {x : SimplexCategory} {f : ↑x.toTopObj} {g : ↑x.toTopObj} : f = g ↔ ↑f = ↑g

theorem SimplexCategory.toTopObj.ext {x : SimplexCategory} (f : ↑x.toTopObj) (g : ↑x.toTopObj) : ↑f = ↑g → f = g

def SimplexCategory.toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) (g : ↑x.toTopObj) : ↑y.toTopObj

A morphism in SimplexCategory induces a map on the associated topological spaces.

Equations

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

@[simp]

theorem SimplexCategory.coe_toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) (g : ↑x.toTopObj) (i : (CategoryTheory.forget SimplexCategory).obj y) : ↑(SimplexCategory.toTopMap f g) i = ∑ j ∈ Finset.filter (fun (x_1 : (CategoryTheory.forget SimplexCategory).obj x) => f x_1 = i) Finset.univ, ↑g j

theorem SimplexCategory.continuous_toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) : Continuous (SimplexCategory.toTopMap f)

@[simp]

theorem SimplexCategory.toTop_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), SimplexCategory.toTop.map f = { toFun := SimplexCategory.toTopMap f, continuous_toFun := ⋯ }

@[simp]

theorem SimplexCategory.toTop_obj (x : SimplexCategory) : SimplexCategory.toTop.obj x = TopCat.of ↑x.toTopObj

def SimplexCategory.toTop : CategoryTheory.Functor SimplexCategory TopCat

The functor associating the topological n-simplex to [n] : SimplexCategory.

Equations

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