smoothSheaf — Mathlib

English

For the sheaf of smooth maps from M to N, on an open set U, the value is exactly the type of $(IM, (unop U))$-smooth maps from U to N.

Русский

Для непрерывной (гладкой) оболочки от M в N на открытом множестве U значение есть ровно множество гладких отображений из U в N, учитывая структуру IM и I.

LaTeX

$$$ (\text{smoothSheaf IM I M N}).presheaf.obj U = C^∞\langle IM, (unop\,U) : Opens M; I, N \rangle $$$

Lean4

/-- The sheaf of smooth functions from `M` to `N`, as a sheaf of types. -/
def smoothSheaf : TopCat.Sheaf (Type u) (TopCat.of M) :=
  (contDiffWithinAt_localInvariantProp (I := IM) (I' := I) ∞).sheaf M N

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