English
Let M be a manifold and R a smooth commutative ring. The assignment U ↦ C∞(U, R) (the ring of smooth functions from U to R) forms a sheaf of commutative rings on M, with restriction maps given by restriction of functions.
Русский
Пусть M — многообразие и R — гладкое коммутативное кольцо. Отображение U ↦ C∞(U, R) образуетSheaf из коммутативных колец на M, где ограничение задаётся ограничением функций.
LaTeX
$$$$\\mathcal{O}(U) = C^{\\infty}(U, R), \\quad \\rho_{V,U}: \\mathcal{O}(U) \\to \\mathcal{O}(V) \\text{ is restriction}, \\ \\text{and } \\mathcal{O}\\text{ is a sheaf of rings on } M.$$$$
Lean4
/-- The sheaf of smooth functions from `M` to `R`, for `R` a smooth commutative ring, as a sheaf of
commutative rings. -/
def smoothSheafCommRing : TopCat.Sheaf CommRingCat.{u} (TopCat.of M) :=
{ val := smoothPresheafCommRing IM I M R
cond := by
rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget CommRingCat)]
exact CategoryTheory.Sheaf.cond (smoothSheaf IM I M R) }
-- sanity check: applying the `CommRingCat`-to-`TypeCat` forgetful functor to the sheaf-of-rings of
-- smooth functions gives the sheaf-of-types of smooth functions.
