nonunits_stalk — Mathlib

English

The non-units of the stalk equal the kernel of evaluation at x.

Русский

Не-единицы stalk равны ядру оценки в x.

LaTeX

$$nonunits (smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf.stalk x = ker (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x)$$

Lean4

/-- The non-units of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜`, considered
as a sheaf of commutative rings, are the functions whose values at `x` are zero. -/
theorem nonunits_stalk (x : M) :
    nonunits ((smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf.stalk x) =
      RingHom.ker (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x) :=
  by
  ext1 f
  rw [mem_nonunits_iff, not_iff_comm, Iff.comm]
  apply smoothSheafCommRing.isUnit_stalk_iff

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