English
There exists a canonical isomorphism between the colimit category perspective and the stalk after forgetting the ring structure, realized by forgetStalk.
Русский
Существует канонический изоморфизм между перспективой колимита и stalk после забывания кольцевой структуры, реализованный через forgetStalk.
LaTeX
$$$$ \\mathrm{colim}\\to \\text{stalk} \\cong \\text{stalk} \\text{ after forget}$$$$
Lean4
/-- Canonical ring homomorphism from the stalk of `smoothSheafCommRing IM I M R` at `x` to `R`,
given by evaluating sections at `x`, considered as a morphism in the category of commutative rings.
-/
def evalHom (x : TopCat.of M) : (smoothSheafCommRing IM I M R).presheaf.stalk x ⟶ CommRingCat.of R :=
by
refine CategoryTheory.Limits.colimit.desc _ ⟨_, ⟨fun U ↦ ?_, ?_⟩⟩
· apply smoothSheafCommRing.evalAt
· cat_disch
