Singular simplicial sets #

Like topological spaces, we can associate to each diffeological space a singular simplicial set, consisting of all smooth singular simplicies (i.e. smooth maps from the standard simplices) in it. This defines a functor from DiffSp ⥤ SSet, which is right-adjoint to a geometric realisation functor SSet ⥤ DiffSp.

TODO #

generalise universe levels
compare with corresponding functors for topological spaces

source

theorem FunOnFinite.dsmooth_map (M : Type u_1) [AddCommMonoid M] [DiffeologicalSpace M] [DSmoothAdd M] {X : Type u_2} {Y : Type u_3} [Finite X] [Finite Y] (f : X → Y) :

DSmooth (map f)

source

theorem FunOnFinite.dsmooth_linearMap (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [DiffeologicalSpace M] [DSmoothAdd M] {X : Type u_3} {Y : Type u_4} [Finite X] [Finite Y] (f : X → Y) :

DSmooth ⇑(linearMap R M f)

source

theorem stdSimplex.dsmooth_map {R : Type u_1} {X : Type u_2} {Y : Type u_3} [Ring R] [PartialOrder R] [IsOrderedRing R] [DiffeologicalSpace R] [DiffeologicalRing R] [Fintype X] [Fintype Y] (f : X → Y) :

DSmooth (map f)

source

noncomputable def SimplexCategory.toDiffSp₀ :

CategoryTheory.Functor SimplexCategory DiffSp

The standard cosimplicial object in DiffSp.{0}, sending each n : SimplexCategory to the standard n-simplex with the subspace diffeology.

Equations

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

Instances For

source

@[simp]

theorem SimplexCategory.toDiffSp₀_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :

toDiffSp₀.map f = DiffSp.ofHom { toFun := stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), dsmooth := ⋯ }

source

@[simp]

theorem SimplexCategory.toDiffSp₀_obj (n : SimplexCategory) :

toDiffSp₀.obj n = DiffSp.of ↑(stdSimplex ℝ (Fin (n.len + 1)))

source

noncomputable def SimplexCategory.toDiffSp :

CategoryTheory.Functor SimplexCategory DiffSp

The standard cosimplicial object in DiffSp.{u}, sending each n : SimplexCategory to the standard n-simplex with the subspace diffeology lifted to the universe u.

Equations

SimplexCategory.toDiffSp = SimplexCategory.toDiffSp₀.comp DiffSp.uliftFunctor

Instances For

source

@[simp]

theorem SimplexCategory.toDiffSp_map {X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) :

toDiffSp.map f = DiffSp.ofHom { toFun := ULift.map (stdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f)), dsmooth := ⋯ }

source

@[simp]

theorem SimplexCategory.toDiffSp_obj (X : SimplexCategory) :

toDiffSp.obj X = DiffSp.of (ULift.{u, 0} ↑(stdSimplex ℝ (Fin (X.len + 1))))

source

noncomputable def DiffSp.toSSet :

CategoryTheory.Functor DiffSp SSet

The singular simplicial set functor for diffeological spaces, sending each diffeological space to the simplicial set of all smooth singular simplices in it.

Equations

DiffSp.toSSet = CategoryTheory.Presheaf.restrictedULiftYoneda SimplexCategory.toDiffSp

Instances For

source

noncomputable def SSet.toDiffSp :

CategoryTheory.Functor SSet DiffSp

The geometric realisation functor from simplicial sets to diffeological spaces. TODO: generalise universe levels in DiffSp.hasColimitsOfSize and this.

Equations