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.

source
instance SimplexCategory.instFintypeObjSimplexCategoryToQuiverToCategoryStructSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForget (x : SimplexCategory) :
Fintype (CategoryTheory.ConcreteCategory.forget.obj x)
Equations
  • One or more equations did not get rendered due to their size.
source
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
Instances For
    source
    instance SimplexCategory.instCoeFunElemForAllObjSimplexCategoryToQuiverToCategoryStructSmallCategoryTypeToQuiverToCategoryStructTypesToPrefunctorForgetInstConcreteCategorySimplexCategorySmallCategoryNNRealToTopObj (x : SimplexCategory) :
    CoeFun ↑(SimplexCategory.toTopObj x) fun (x_1 : ↑(SimplexCategory.toTopObj x)) => (CategoryTheory.forget SimplexCategory).obj x → NNReal
    Equations
    • One or more equations did not get rendered due to their size.
    source
    theorem SimplexCategory.toTopObj.ext {x : SimplexCategory} (f : ↑(SimplexCategory.toTopObj x)) (g : ↑(SimplexCategory.toTopObj x)) :
    ↑f = ↑g → f = g
    source
    def SimplexCategory.toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) (g : ↑(SimplexCategory.toTopObj x)) :
    ↑(SimplexCategory.toTopObj y)

    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
      source
      @[simp]
      theorem SimplexCategory.coe_toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) (g : ↑(SimplexCategory.toTopObj x)) (i : (CategoryTheory.forget SimplexCategory).obj y) :
      ↑(SimplexCategory.toTopMap f g) i = Finset.sum (Finset.filter (fun (x_1 : (CategoryTheory.forget SimplexCategory).obj x) => f x_1 = i) Finset.univ) fun (j : (CategoryTheory.forget SimplexCategory).obj x) => ↑g j
      source
      theorem SimplexCategory.continuous_toTopMap {x : SimplexCategory} {y : SimplexCategory} (f : x ⟶ y) :
      Continuous (SimplexCategory.toTopMap f)
      source
      @[simp]
      theorem SimplexCategory.toTop_obj (x : SimplexCategory) :
      SimplexCategory.toTop.obj x = TopCat.of ↑(SimplexCategory.toTopObj x)
      source
      @[simp]
      theorem SimplexCategory.toTop_map_apply :
      ∀ {X Y : SimplexCategory} (f : X ⟶ Y) (g : ↑(SimplexCategory.toTopObj X)), (SimplexCategory.toTop.map f) g = SimplexCategory.toTopMap f g
      source
      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.
      Instances For