instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf

Mathlib.Geometry.Manifold.Sheaf.Smooth

URI: https://scilib.ai/kg/mathlib#instRingObjOppositeOpensCarrierOfPresheafSmoothSheaf

← MathLib Explorer

English

The presheaf of smooth functions from M to R, where R is a smooth ring, is a presheaf of rings.

Русский

Оболочка гладких отображений из M в R образует прешеф кольцо.

LaTeX

$$smoothPresheafRing IM I M R$$

Lean4

instance (U : (Opens (TopCat.of M))ᵒᵖ) : Ring ((smoothSheaf IM I M R).presheaf.obj U) :=
  (ContMDiffMap.ring : Ring C^∞⟮IM, (unop U : Opens M); I, R⟯)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru