The stalks of the sheaf of C^n functions are local rings

The stalk at x of the sheaf of C^n functions valued in a nontrivially normed field 𝕜 (contMDiffSheafCommRing IM 𝓘(𝕜) n M 𝕜) is a local ring: a germ is a unit iff its value at x is nonzero (contMDiffSheafCommRing.isUnit_stalk_iff), the non-units form the kernel of the evaluation at x, which is therefore the maximal ideal (maximalIdeal_stalk), and the residue field is 𝕜 through the evaluation (residueFieldEquiv). Mathlib proves this for n = ∞ (smoothSheafCommRing.instLocalRing_stalk); the argument is the same for every n: a germ with nonzero value is nonzero on a neighbourhood of x, on which its pointwise inverse is again C^n (contDiffAt_inv).

Instantiated at n = ω, these are the local rings 𝒪_{M,a} of the structure sheaf of an analytic manifold (structureSheaf); the stalk contains its residue field as the constants, as Bierstone–Milman require of the local rings of their category of spaces [BM97, (0.1)(2)].

theorem Manifold.contMDiffSheafCommRing.isUnit_stalk_iff {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] {x : M} (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x)) : IsUnit f ↔ (eval IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜 x) f ≠ 0

A germ of the sheaf of C^n functions valued in 𝕜 is a unit iff its value at the point is nonzero.

theorem Manifold.contMDiffSheafCommRing.nonunits_stalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (x : M) : nonunits ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x) = ↑(RingHom.ker (eval IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜 x))

The non-units of the stalk are the germs vanishing at the point.

instance Manifold.contMDiffSheafCommRing.instLocalRing_stalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (x : M) : IsLocalRing ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x)

The stalks of the sheaf of C^n functions valued in 𝕜 are local rings.

theorem Manifold.contMDiffSheafCommRing.maximalIdeal_stalk {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (x : M) : IsLocalRing.maximalIdeal ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x) = RingHom.ker (eval IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜 x)

The maximal ideal of the stalk is the kernel of the evaluation.

noncomputable def Manifold.contMDiffSheafCommRing.residueFieldEquiv {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (x : M) : IsLocalRing.ResidueField ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x) ≃+* 𝕜

The residue field of the stalk is 𝕜, through the evaluation.

Equations

• Manifold.contMDiffSheafCommRing.residueFieldEquiv IM n M x = (Ideal.quotEquivOfEq ⋯).trans (RingHom.quotientKerEquivOfSurjective ⋯)

theorem Manifold.contMDiffSheafCommRing.residueFieldEquiv_residue {𝕜 : Type} [NontriviallyNormedField 𝕜] {EM : Type u_1} [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_2} [TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM) (n : WithTop ℕ∞) (M : Type u) [TopologicalSpace M] [ChartedSpace HM M] (x : M) (f : ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x)) : (residueFieldEquiv IM n M x) ((IsLocalRing.residue ↑((contMDiffSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜).presheaf.stalk x)) f) = (eval IM (modelWithCornersSelf 𝕜 𝕜) n M 𝕜 x) f