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.

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

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

Equations

• x.toTopObj = {f : CategoryTheory.ToType x → NNReal | ∑ i : CategoryTheory.ToType x, f i = 1}

instance SimplexCategory.instCoeFunElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj (x : SimplexCategory) : CoeFun ↑x.toTopObj fun (x_1 : ↑x.toTopObj) => CategoryTheory.ToType x → NNReal

Equations

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

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

@[simp]

theorem SimplexCategory.toTopObj_zero_apply_zero (f : ↑(mk 0).toTopObj) : ↑f 0 = 1

theorem SimplexCategory.toTopObj_one_add_eq_one (f : ↑(mk 1).toTopObj) : ↑f 0 + ↑f 1 = 1

theorem SimplexCategory.toTopObj_one_coe_add_coe_eq_one (f : ↑(mk 1).toTopObj) : ↑(↑f 0) + ↑(↑f 1) = 1

instance SimplexCategory.instNonemptyElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj (x : SimplexCategory) : Nonempty ↑x.toTopObj

instance SimplexCategory.instUniqueElemForallToTypeOrderHomFinHAddNatLenOfNatMkNNRealToTopObj : Unique ↑(mk 0).toTopObj

Equations

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

def SimplexCategory.toTopObjOneHomeo : ↑(mk 1).toTopObj ≃ₜ ↑unitInterval

The one-dimensional topological simplex is homeomorphic to the unit interval.

Equations

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

instance SimplexCategory.instPathConnectedSpaceElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj (x : SimplexCategory) : PathConnectedSpace ↑x.toTopObj

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.ToType y) : ↑(toTopMap f g) i = ∑ j ∈ Finset.filter (fun (x_1 : (fun (X : SimplexCategory) => Fin (X.len + 1)) x) => (CategoryTheory.ConcreteCategory.hom 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_obj (x : SimplexCategory) : toTop.obj x = TopCat.of ↑x.toTopObj

@[simp]

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