smoothPresheafRing — Mathlib

English

The presheaf of smooth functions from M to R naturally forms a presheaf of rings with restriction maps given by smooth restriction homomorphisms.

Русский

Прешеф гладких отображений образует прешеф колец с ограничениями по гладким отображениям.

LaTeX

$$smoothPresheafRing IM I M R$$

Lean4

/-- The presheaf of smooth functions from `M` to `R`, for `R` a smooth ring, as a presheaf
of rings. -/
def smoothPresheafRing : TopCat.Presheaf RingCat.{u} (TopCat.of M) :=
  { obj := fun U ↦ RingCat.of ((smoothSheaf IM I M R).presheaf.obj U)
    map := fun h ↦ RingCat.ofHom <| ContMDiffMap.restrictRingHom IM I R <| CategoryTheory.leOfHom h.unop
    map_id := fun _ ↦ rfl
    map_comp := fun _ _ ↦ rfl }

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