Smooth Spaces

Smooth spaces are sheaves on the site CartSp; see https://ncatlab.org/nlab/show/smooth+set.

Main definitions / results:

• SmoothSp: the category of smooth spaces, as the category of sheaves on CartSp
• DiffSp.toSmoothSp: the embedding of diffeological spaces into smooth sets
• SmoothSp.Γ: the global sections functor taking a smooth space to the set of its points
• SmoothSp.concr: the concretisation functor from smooth spaces to diffeological spaces
• DiffSp.reflectorAdjunction: the adjunction between SmoothSp.concr and DiffSp.toSmoothSp turning DiffSp into a reflective subcategory of SmoothSp

TODO

• discrete and codiscrete smooth spaces, corresponding adjunctions
• connected components functor Π_0, corresponding adjunction
• smooth spaces Ω k of differential forms
• De-Rham cohomology for smooth spaces?

def SmoothSp : Type (u + 1)

The category of sheaves on CartSp, also known as smooth spaces.

Equations

• SmoothSp = CategoryTheory.Sheaf CartSp.openCoverTopology (Type ?u.2)

noncomputable instance instCategorySmoothSp : CategoryTheory.Category.{u, u + 1} SmoothSp

Morphisms of smooth spaces are simply morphisms of sheaves.

Equations

• instCategorySmoothSp = id inferInstance

noncomputable def DiffSp.toSmoothSp : CategoryTheory.Functor DiffSp SmoothSp

The embedding of diffeological spaces into smooth spaces.

Equations

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

def DiffSp.toSmoothSp.fullyFaithful : toSmoothSp.FullyFaithful

DiffSp.toSmoothSp is fully faithful.

Equations

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

instance instFullDiffSpSmoothSpToSmoothSp : DiffSp.toSmoothSp.Full

instance instFaithfulDiffSpSmoothSpToSmoothSp : DiffSp.toSmoothSp.Faithful

def SmoothSp.Γ : CategoryTheory.Functor SmoothSp (Type u)

The global sections functor taking a smooth space to its type of points. Note that this is by no means faithful; SmoothSp is not a concrete category.

Equations

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

instance SmoothSp.instDiffeologicalSpaceΓ (X : SmoothSp) : DiffeologicalSpace (Γ.obj X)

The diffeology on the points of a smooth space given by the concretisation functor.

Equations

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

def SmoothSp.concr : CategoryTheory.Functor SmoothSp DiffSp

The reflector of DiffSp inside of SmoothSp, sending a smooth space to its concretisation.

Equations

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

noncomputable def DiffSp.reflectorAdjunction : SmoothSp.concr ⊣ toSmoothSp

The adjunction between the concretisation functor SmoothSp ⥤ DiffSp and the embedding DiffSp ⥤ SmoothSp.

Equations

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

instance instIsLeftAdjointSmoothSpDiffSpConcr : SmoothSp.concr.IsLeftAdjoint

SmoothSp.concr is a left-adjoint. In particular, this means that it preserves colimits.

noncomputable instance DiffSp.toSmoothSp.reflective : CategoryTheory.Reflective toSmoothSp

Diffeological spaces form a reflective subcategory of the category of smooth spaces.

Equations

• DiffSp.toSmoothSp.reflective = { toFull := instFullDiffSpSmoothSpToSmoothSp, toFaithful := instFaithfulDiffSpSmoothSpToSmoothSp, L := SmoothSp.concr, adj := DiffSp.reflectorAdjunction }

noncomputable instance DiffSp.toSmoothSp.createsLimits : CategoryTheory.CreatesLimits toSmoothSp

Equations

• DiffSp.toSmoothSp.createsLimits = CategoryTheory.monadicCreatesLimits DiffSp.toSmoothSp

noncomputable def instDiffeologicalSpaceAlternatingMapReal (M : Type u_1) (N : Type u_2) [AddCommGroup M] [Module ℝ M] [DiffeologicalSpace M] [AddCommGroup N] [Module ℝ N] [DiffeologicalSpace N] (ι : Type u_3) : DiffeologicalSpace (M [⋀^ι]→ₗ[ℝ] N)

Equations

• instDiffeologicalSpaceAlternatingMapReal M N ι = fineDiffeology ℝ (M [⋀^ι]→ₗ[ℝ] N)

noncomputable def SmoothSp.Ω {k : ℕ} : SmoothSp

One possible future target for formalisation: the smooth spaces Ω k of smooth k-forms. Maps X → Ω k correspond to smooth k-forms on X, so they can be used to define differential forms and the De-Rham-cohomology on all smooth spaces.

Right now, one major obstactle to this is showing that pullbacks of smooth k-forms along smooth maps are smooth (i.e. the first sorry); it requires showing that AlternatingMap.compLinearMap is a smooth function of f and g and that fderiv is a smooth function of x, but we have not yet even put a diffeology on the involved spaces of continuous linear functions.

Equations

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