evalHom_germ — Mathlib

English

There is a canonical ring homomorphism from the stalk of the smooth ring sheaf at a point to R, obtained by evaluating sections at that point.

Русский

Существует канонический кольцевой гомоморфизм от stalk гладкого пучка колец в R, получаемый за счёт оценки секций в данной точке.

LaTeX

$$$$ \\mathrm{eval}(x) : (\\text{stalk at } x) \\to R $$ is the evaluation map at x.$$

Lean4

@[simp]
theorem evalHom_germ (U : Opens (TopCat.of M)) (x : M) (hx : x ∈ U)
    (f : (smoothSheafCommRing IM I M R).presheaf.obj (op U)) :
    smoothSheafCommRing.evalHom IM I M R (x : TopCat.of M) ((smoothSheafCommRing IM I M R).presheaf.germ U x hx f) =
      f ⟨x, hx⟩ :=
  congr_arg (fun a ↦ a f) <| smoothSheafCommRing.ι_evalHom IM I M R x ⟨U, hx⟩

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