English
The forgetful stalk functor from smooth ring sections to ordinary sections is compatible with evaluation, providing a canonical comparison between the two stalks at a given point.
Русский
Забывающий stalk-функтор для секций гладких колец совместим с оценкой и обеспечивает каноническое сравнение двух stalk в данной точке.
LaTeX
$$$$ \\text{forgetStalk} \\;\\colon\\; (\\text{presheaf of rings})_x \\to (\\text{presheaf of types})_x $$ preserves the stalk structure and commutes with evaluation maps.$$
Lean4
/-- Identify the stalk at a point of the sheaf-of-commutative-rings of functions from `M` to `R`
(for `R` a smooth ring) with the stalk at that point of the corresponding sheaf of types. -/
def forgetStalk (x : TopCat.of M) :
((smoothSheafCommRing IM I M R).presheaf.stalk x).carrier ≅ (smoothSheaf IM I M R).presheaf.stalk x :=
preservesColimitIso (forget _) _
