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
noncomputable def SimplexCategory.toTop₀ :
CategoryTheory.CosimplicialObject TopCat

The functor SimplexCategory ⥤ TopCat.{0} associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SimplexCategory.toTop₀_obj (n : SimplexCategory) :
    toTop₀.obj n = TopCat.of ↑(stdSimplex ℝ (Fin (n.len + 1)))
    source
    @[simp]
    theorem SimplexCategory.toTop₀_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
    toTop₀.map f = TopCat.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ }
    source
    noncomputable def SimplexCategory.toTop :
    CategoryTheory.Functor SimplexCategory TopCat

    The functor SimplexCategory ⥤ TopCat.{u} associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

    Equations
    Instances For
      source
      @[simp]
      theorem SimplexCategory.toTop_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :
      toTop.{u}.map f = TopCat.uliftFunctor.map (TopCat.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })
      source
      @[simp]
      theorem SimplexCategory.toTop_obj (X : SimplexCategory) :
      toTop.{u}.obj X = TopCat.uliftFunctor.obj (TopCat.of ↑(stdSimplex ℝ (Fin (X.len + 1))))
      source
      instance SimplexCategory.instNonemptyCarrierObjTopCatToTop₀ (n : SimplexCategory) :
      Nonempty ↑(toTop₀.obj n)
      source
      instance SimplexCategory.instNonemptyCarrierObjTopCatToTop (n : SimplexCategory) :
      Nonempty ↑(toTop.{u}.obj n)
      source
      instance SimplexCategory.instUniqueCarrierObjTopCatToTop₀MkOfNatNat :
      Unique ↑(toTop₀.obj (mk 0))
      Equations
      source
      instance SimplexCategory.instUniqueCarrierObjTopCatToTopMkOfNatNat :
      Unique ↑(toTop.{u}.obj (mk 0))
      Equations
      source
      instance SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop₀ (n : SimplexCategory) :
      PathConnectedSpace ↑(toTop₀.obj n)
      source
      instance SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop (n : SimplexCategory) :
      PathConnectedSpace ↑(toTop.{u}.obj n)
      source
      @[deprecated SimplexCategory.toTop₀ (since := "2025-08-25")]
      def SimplexCategory.toTopObj :
      CategoryTheory.CosimplicialObject TopCat

      Alias of SimplexCategory.toTop₀.

      The functor SimplexCategory ⥤ TopCat.{0} associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

      Equations
      Instances For
        source
        @[deprecated stdSimplex.ext (since := "2025-08-25")]
        theorem SimplexCategory.toTopObj.ext {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] {s t : ↑(stdSimplex S X)} (h : ⇑s = ⇑t) :
        s = t

        Alias of stdSimplex.ext.

        source
        @[deprecated stdSimplex.eq_one_of_unique (since := "2025-08-25")]
        theorem SimplexCategory.toTopObj_zero_apply_zero {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} [Fintype X] [IsOrderedRing S] [Unique X] (s : ↑(stdSimplex S X)) (x : X) :
        s x = 1

        Alias of stdSimplex.eq_one_of_unique.

        source
        @[deprecated stdSimplex.add_eq_one (since := "2025-08-25")]
        theorem SimplexCategory.toTopObj_one_add_eq_one {S : Type u_1} [Semiring S] [PartialOrder S] (s : ↑(stdSimplex S (Fin 2))) :
        s 0 + s 1 = 1

        Alias of stdSimplex.add_eq_one.

        source
        @[deprecated stdSimplex.add_eq_one (since := "2025-08-25")]
        theorem SimplexCategory.toTopObj_one_coe_add_coe_eq_one {S : Type u_1} [Semiring S] [PartialOrder S] (s : ↑(stdSimplex S (Fin 2))) :
        s 0 + s 1 = 1

        Alias of stdSimplex.add_eq_one.

        source
        @[deprecated stdSimplexHomeomorphUnitInterval (since := "2025-08-25")]
        def SimplexCategory.toTopObjOneHomeo :
        ↑(stdSimplex ℝ (Fin 2)) ≃ₜ ↑unitInterval

        Alias of stdSimplexHomeomorphUnitInterval.

        The standard one-dimensional simplex in ℝ² = Fin 2 → ℝ is homeomorphic to the unit interval.

        Equations
        Instances For
          source
          @[deprecated SimplexCategory.toTop₀ (since := "2025-08-25")]
          def SimplexCategory.toTopMap :
          CategoryTheory.CosimplicialObject TopCat

          Alias of SimplexCategory.toTop₀.

          The functor SimplexCategory ⥤ TopCat.{0} associating the topological n-simplex to ⦋n⦌ : SimplexCategory.

          Equations
          Instances For
            source
            @[deprecated FunOnFinite.linearMap_apply_apply (since := "2025-08-25")]
            theorem SimplexCategory.coe_toTopMap (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Fintype X] [Finite Y] [DecidableEq Y] (f : X → Y) (s : X → M) (y : Y) :
            (FunOnFinite.linearMap R M f) s y = {x : X | f x = y}.sum s

            Alias of FunOnFinite.linearMap_apply_apply.

            source
            @[deprecated stdSimplex.continuous_map (since := "2025-08-25")]
            theorem SimplexCategory.continuous_toTopMap {S : Type u_1} [Semiring S] [PartialOrder S] {X : Type u_2} {Y : Type u_3} [Fintype X] [Fintype Y] [IsOrderedRing S] [TopologicalSpace S] [IsTopologicalSemiring S] (f : X → Y) :
            Continuous (stdSimplex.map f)

            Alias of stdSimplex.continuous_map.