Embeddings of categories of manifolds into the category of diffeological spaces

In this file we define the natural inclusion functors from categories of manifolds into the category DiffSp of diffeological spaces, and show that some of them are fully faithful.

Main definitions / results:

• Functors Mfld ℝ ∞ ⥤ DiffSp and P.FullSubcategory ⥤ DiffSp for any P : ObjectProperty (Mfld ℝ ∞), both available as forget₂. Only the former is registered as a HasForget₂ instance here, as a HasForget₂ for restrictions to full subcategories is already available.
• forget₂ : FinDimMfld ℝ ∞ ⥤ DiffSp is fully faithful.

TODO

• Show that FinDimMfldWCorners ℝ ∞ ⥤ DiffSp is fully faithful too, if it is. This is known to be true for manifolds with corners, but I haven't yet checked the details for manifolds with corners.
• Show that BanachMfld ℝ ∞ ⥤ DiffSp is fully faithful too. In the literature this is proven more generally for Frechet manifolds, but mathlib only has Banach manifolds for now. For the manifolds modelled on general normed spaces that mathlib has instead, this is presumably false because out of the many inequivalent notions of smoothness in normed spaces, mathlib has picked a different one than the one diffeological smoothness is equivalent to.

noncomputable instance instHasForget₂MfldRealSomeENatTopDiffSp : CategoryTheory.HasForget₂ (Mfld ℝ ↑⊤) DiffSp

The category of (possibly non-Hausdorff, non-paracompact) smooth real manifolds with corners carries a functor to the category of diffeological spaces that assigns to each manifold M the diffeology IsManifold.toDiffeology given by all smooth maps from ℝⁿ to M.

Equations

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

def FinDimMfld.fullyFaithfulForgetToDiffSp : (CategoryTheory.forget₂ (FinDimMfld ℝ ↑⊤) DiffSp).FullyFaithful

For finite-dimensional manifolds, the inclusion into DiffSp is fully faithful.

Equations

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

instance FinDimMfld.instFullRealSomeENatTopDiffSpForget₂ : (CategoryTheory.forget₂ (FinDimMfld ℝ ↑⊤) DiffSp).Full