evalHom — Mathlib

English

There is a canonical evaluation-to-function correspondence: sections over U correspond to functions on points of U.

Русский

Существует каноническое соответствие между значениями секций над U и функциями на точках U.

LaTeX

$$Существуют естественные отображения $U\mapsto$ функции, такие что на каждом x∈U значение секции равно $f(x)$.$$

Lean4

/-- Canonical map from the stalk of `smoothSheaf IM I M N` at `x` to `N`, given by evaluating
sections at `x`, considered as a morphism in the category of types. -/
def evalHom (x : TopCat.of M) : (smoothSheaf IM I M N).presheaf.stalk x ⟶ N :=
  TopCat.stalkToFiber (StructureGroupoid.LocalInvariantProp.localPredicate M N _) x

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