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
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
    Instances For
      source
      instance SimplexCategory.instCoeFunElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj (x : SimplexCategory) :
      CoeFun ↑x.toTopObj fun (x_1 : ↑x.toTopObj) => CategoryTheory.ToType x → NNReal
      Equations
        source
        theorem SimplexCategory.toTopObj.ext {x : SimplexCategory} (f g : ↑x.toTopObj) :
        ↑f = ↑g → f = g
        source
        theorem SimplexCategory.toTopObj.ext_iff {x : SimplexCategory} {f g : ↑x.toTopObj} :
        f = g ↔ ↑f = ↑g
        source
        @[simp]
        theorem SimplexCategory.toTopObj_zero_apply_zero (f : ↑(mk 0).toTopObj) :
        ↑f 0 = 1
        source
        theorem SimplexCategory.toTopObj_one_add_eq_one (f : ↑(mk 1).toTopObj) :
        ↑f 0 + ↑f 1 = 1
        source
        theorem SimplexCategory.toTopObj_one_coe_add_coe_eq_one (f : ↑(mk 1).toTopObj) :
        ↑(↑f 0) + ↑(↑f 1) = 1
        source
        instance SimplexCategory.instNonemptyElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj (x : SimplexCategory) :
        Nonempty ↑x.toTopObj
        source
        instance SimplexCategory.instUniqueElemForallToTypeOrderHomFinHAddNatLenOfNatMkNNRealToTopObj :
        Unique ↑(mk 0).toTopObj
        Equations
          source
          def SimplexCategory.toTopObjOneHomeo :
          ↑(mk 1).toTopObj ≃ₜ ↑unitInterval

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

          Equations
            Instances For
              source
              instance SimplexCategory.instPathConnectedSpaceElemForallToTypeOrderHomFinHAddNatLenOfNatNNRealToTopObj (x : SimplexCategory) :
              PathConnectedSpace ↑x.toTopObj
              source
              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
                Instances For
                  source
                  @[simp]
                  theorem SimplexCategory.coe_toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : ↑x.toTopObj) (i : CategoryTheory.ToType y) :
                  ↑(toTopMap f g) i = ∑ j : (fun (X : SimplexCategory) => Fin (X.len + 1)) x with (CategoryTheory.ConcreteCategory.hom f) j = i, ↑g j
                  source
                  theorem SimplexCategory.continuous_toTopMap {x y : SimplexCategory} (f : x ⟶ y) :
                  Continuous (toTopMap f)
                  source
                  def SimplexCategory.toTop :
                  CategoryTheory.Functor SimplexCategory TopCat

                  The functor associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem SimplexCategory.toTop_obj (x : SimplexCategory) :
                      toTop.obj x = TopCat.of ↑x.toTopObj
                      source
                      @[simp]
                      theorem SimplexCategory.toTop_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
                      toTop.map f = TopCat.ofHom { toFun := toTopMap f, continuous_toFun := ⋯ }