Embeddings of sites into opposites of real algebras

This file constructs the functor CartSp ⥤ (CommAlgCat ℝ)ᵒᵖ sending each ℝⁿ to the algebra of smooth real valued functions on it, and shows that this functor is fully faithful.

Eventually we'll want to do the same for EuclOp and FinDimMfld; for EuclOp this should already be feasible, but for FinDimMfld we still lack a variant of Whitney's embedding theorem for non-compact manifolds.

See https://ncatlab.org/nlab/show/embedding+of+smooth+manifolds+into+formal+duals+of+R-algebras.

Main definitions / results:

• CartSp.toCommAlgCatOp: the fully faithful embedding of CartSp into (CommAlgCat ℝ)ᵒᵖ

TODO

• Show that EuclOp embeds into (CommAlgCat ℝ)ᵒᵖ fully faithfully too
• Show that FinDimMfld embeds into (CommAlgCat ℝ)ᵒᵖ fully faithfully too

noncomputable def CartSp.toCommAlgCatOp : CategoryTheory.Functor CartSp (CommAlgCat ℝ)ᵒᵖ

The embedding of CartSp into the opposite category of ℝ-algebras, sending each space X to the algebra of smooth maps X → ℝ.

Equations

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

@[simp]

theorem CartSp.toCommAlgCatOp_map {n m : CartSp} (f : n ⟶ m) : toCommAlgCatOp.map f = (CommAlgCat.ofHom (DSmoothMap.compRightAlgHom f)).op

@[simp]

theorem CartSp.toCommAlgCatOp_obj (X : CartSp) : toCommAlgCatOp.obj X = Opposite.op (CommAlgCat.of ℝ (DSmoothMap (EuclideanSpace ℝ (Fin X)) ℝ))

noncomputable def CartSp.toCommAlgCatOpFullyFaithful : toCommAlgCatOp.FullyFaithful

The embedding of CartSp into (CommAlgCat ℝ)ᵒᵖ is fully faithful. Given a homomorphism f : DSmoothMap (Eucl m) ℝ →ₐ[ℝ] DSmoothMap (Eucl n) ℝ of ℝ-algebras, a corresponding smooth function Eucl n → Eucl m can be constructed by transporting the coordinate functions Eucl m → ℝ along f.

Equations

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

instance instFullCartSpOppositeCommAlgCatRealToCommAlgCatOp : CartSp.toCommAlgCatOp.Full

instance instFaithfulCartSpOppositeCommAlgCatRealToCommAlgCatOp : CartSp.toCommAlgCatOp.Faithful