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.HasForget.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 {x : SimplexCategory} (f g : ↑x.toTopObj) : ↑f = ↑g → f = g

def SimplexCategory.toTopMap {x 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 y : SimplexCategory} (f : x ⟶ y) (g : ↑x.toTopObj) (i : (CategoryTheory.forget SimplexCategory).obj y) : ↑(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 y : SimplexCategory} (f : x ⟶ y) : Continuous (toTopMap f)

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.

@[simp]

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

@[simp]

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