ι_evalHom — Mathlib

English

The composite of the forgetStalk inverse with the evaluation map equals the evaluation map on the original smooth presheaf, establishing a compatibility of the two viewpoints.

Русский

Состав противоположного forgetStalk с оценкой равен исходной карте оценки гладкого прешифра; связь согласуется между двумя подходами.

LaTeX

$$$$ (forgetStalk)^{-1} \\circ \\mathrm{ev} = \\mathrm{ev}_{\\text{smooth}}.$$$$

Lean4

@[simp, reassoc, elementwise]
theorem ι_evalHom (x : TopCat.of M) (U) :
    colimit.ι ((OpenNhds.inclusion x).op ⋙ _) U ≫ smoothSheafCommRing.evalHom IM I M R x =
      smoothSheafCommRing.evalAt _ _ _ _ _ _ :=
  colimit.ι_desc _ _

Похожие утверждения