English
There is a canonical comparison morphism between the colimit injections into the stalk and the forgetStalk map, compatible with evaluation maps.
Русский
Существует каноническое сравнение между вложениями колимита в stalk и forgetStalk-морфизмом, совместимое с оценкой.
LaTeX
$$$$ \\text{ι}_{\\mathcal{F}}: \\mathrm{colim} \\to \\mathrm{stalk} \\quad \\text{and} \\quad \\text{forgetStalk} \\text{ commute with } \\mathrm{eval}.$$$$
Lean4
@[simp, reassoc, elementwise]
theorem ι_forgetStalk_hom (x : TopCat.of M) (U) :
CategoryStruct.comp (Z := (smoothSheaf IM I M R).presheaf.stalk x)
(DFunLike.coe (α := (((smoothSheafCommRing IM I M R).presheaf.obj (op ((OpenNhds.inclusion x).obj U.unop)))))
(colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U).hom)
(forgetStalk IM I M R x).hom =
colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U :=
ι_preservesColimitIso_hom (forget CommRingCat) _ _
