English
For every base point x, the evaluation map from the stalk to R is surjective; every value in R is attained by some germ.
Русский
Для каждой точки x отображение оценки из stalk в R it's сюрьективно; каждый элемент R достигается некоторым жёрмом.
LaTeX
$$$$ \\mathrm{ev}_x : \\mathcal{O}_x \\twoheadrightarrow R $$ is surjective.$$
Lean4
@[simp, reassoc, elementwise]
theorem forgetStalk_inv_comp_eval (x : TopCat.of M) :
(smoothSheafCommRing.forgetStalk IM I M R x).inv ≫ (DFunLike.coe (smoothSheafCommRing.evalHom IM I M R x).hom) =
smoothSheaf.evalHom _ _ _ _ :=
by
apply Limits.colimit.hom_ext
intro U
change (colimit.ι _ U) ≫ _ = colimit.ι ((OpenNhds.inclusion x).op ⋙ _) U ≫ _
rw [smoothSheafCommRing.ι_forgetStalk_inv_assoc, smoothSheaf.ι_evalHom]
ext x
exact CategoryTheory.congr_fun (smoothSheafCommRing.ι_evalHom ..) x
