instLocalRing_stalk — Mathlib

English

For every point x on a smooth manifold M, the stalk of the structure sheaf of smooth functions at x is a local ring.

Русский

Для каждой точки x гладкого многообразия M локализация структуры каскада гладких функций в точке x образует локальное кольцо.

LaTeX

$$$\forall x \in M,\; \mathcal{O}_{M,x} \text{ является локальным кольцом}$$$

Lean4

/-- The stalks of the structure sheaf of a smooth manifold are local rings. -/
instance instLocalRing_stalk (x : M) : IsLocalRing ((smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf.stalk x) :=
  by
  apply IsLocalRing.of_nonunits_add
  rw [smoothSheafCommRing.nonunits_stalk]
  intro f g
  exact Ideal.add_mem _

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