Documentation

Mathlib.AlgebraicTopology.TopologicalSimplex

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

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

Equations
Instances For
    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 = gf = 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.
    Instances For
      @[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 = jFinset.filter (fun (x_1 : (CategoryTheory.forget SimplexCategory).obj x) => f x_1 = i) Finset.univ, g j
      @[simp]
      theorem SimplexCategory.toTop_map :
      ∀ {X Y : SimplexCategory} (f : X Y), SimplexCategory.toTop.map f = { toFun := SimplexCategory.toTopMap f, continuous_toFun := }

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

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