The analytic stalk is a Noetherian regular local ring of dimension n

Bierstone–Milman require of their category of spaces that "𝒪_X is a coherent sheaf of rings and X is locally Noetherian" [BM97, (3.8)(3)] and call X smooth "if, for all x ∈ |X|, 𝒪_{X,x} is a regular local ring" [BM97, §3]; Hironaka calls a point simple if its local ring is regular, the simple points being, by the Jacobian criterion and the implicit function theorem, those with a neighbourhood isomorphic to an open subset of K^n [Hir64, p. 121]. For the stalk 𝒪_{M,a} of the structure sheaf of an analytic manifold:

• Noetherian (Rückert's basis theorem): the Taylor homomorphism T_a of a chart is injective with range the convergent power series (Hironaka/Manifold/Germ/TaylorIdeal.lean), so 𝒪_{M,a} ≃+* Conv 𝕜 n (taylorEquivConv), and Conv 𝕜 n is Noetherian (Hironaka/Analytic/Rueckert/Noetherian.lean);
• dimension n: 𝒪̂_{M,a} ≅ 𝕜[[X_1, …, X_n]] (Hironaka/Manifold/Germ/TaylorCompletion.lean), the completion of a Noetherian local ring has the same Krull dimension (IsLocalRing.ringKrullDim_adicCompletion_eq; 𝒪̂ is Noetherian by IsLocalRing.isNoetherianRing_adicCompletion), and dim 𝕜[[X_1, …, X_n]] = n (IsLocalRing.ringKrullDim_mvPowerSeries);
• regular: 𝔪_a is generated by the n centred coordinates, so spanFinrank 𝔪_a ≤ n = ringKrullDim 𝒪_{M,a}, which is Mathlib's criterion IsRegularLocalRing.of_spanFinrank_maximalIdeal_le; the embedding dimension is then n (spanFinrank_maximalIdeal_stalk).

The chart-parametrised statements take a chart (φ, ψ) at a; the instances take [IsManifold 𝓘(𝕜, E) ω M] and [FiniteDimensional 𝕜 E] and use the chart at a with the coordinates modelCoord of the finite-dimensional model space (n = finrank 𝕜 E). The Noetherian instance is used throughout the Hironaka library wherever an ideal of a stalk has to be finitely generated, and the regularity and dimension wherever a centre or a hypersurface is compared with the ambient stalk.

noncomputable def Manifold.taylorEquivConv {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* ↥(Analytic.Conv 𝕜 n)

The Taylor homomorphism of a chart as a ring isomorphism 𝒪_{M,a} ≃+* Conv 𝕜 n onto the convergent power series: injective (IsTaylorHom.injective') with range Conv 𝕜 n (range_taylorHom).

Equations

• Manifold.taylorEquivConv E ψ φ ha hφ = RingEquiv.ofBijective ((Manifold.taylorHom E ψ φ ha hφ).codRestrict (Analytic.Conv 𝕜 n) ⋯) ⋯

theorem Manifold.taylorEquivConv_apply_coe {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) (s : ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) : ↑((taylorEquivConv E ψ φ ha hφ) s) = (taylorHom E ψ φ ha hφ) s

theorem Manifold.isNoetherianRing_stalk_of_chart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : IsNoetherianRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

Rückert's basis theorem for the stalk [BM97, (3.8)(3)]: 𝒪_{M,a} is Noetherian, being isomorphic to the ring Conv 𝕜 n of convergent power series.

theorem Manifold.ringKrullDim_stalk_of_chart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : ringKrullDim ↑((structureSheaf 𝕜 E M).presheaf.stalk a) = ↑n

ringKrullDim 𝒪_{M,a} = n: the completion 𝒪̂_{M,a} ≅ 𝕜[[X_1, …, X_n]] has the same dimension as 𝒪_{M,a}, and dim 𝕜[[X]] = n.

theorem Manifold.spanFinrank_maximalIdeal_stalk_le {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : Submodule.spanFinrank (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) ≤ n

The maximal ideal of the stalk is generated by the n centred coordinates, so its minimal number of generators is at most n.

theorem Manifold.isRegularLocalRing_stalk_of_chart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : IsRegularLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The stalk 𝒪_{M,a} is a regular local ring ("smooth if … 𝒪_{X,x} is a regular local ring" [BM97, §3]; Hironaka's simple points [Hir64, p. 121]): 𝔪_a has n generators and ringKrullDim 𝒪_{M,a} = n (Mathlib's IsRegularLocalRing.of_spanFinrank_maximalIdeal_le).

theorem Manifold.spanFinrank_maximalIdeal_stalk_of_chart {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) : Submodule.spanFinrank (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) = n

The embedding dimension dim_𝕜 𝔪_a/𝔪_a² (the minimal number of generators of 𝔪_a) is n.

instance Manifold.isNoetherianRing_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : IsNoetherianRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The analytic stalks are Noetherian [BM97, (3.8)(3)].

theorem Manifold.ringKrullDim_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : ringKrullDim ↑((structureSheaf 𝕜 E M).presheaf.stalk a) = ↑(Module.finrank 𝕜 E)

ringKrullDim 𝒪_{M,a} = n, the dimension of the manifold.

instance Manifold.isRegularLocalRing_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : IsRegularLocalRing ↑((structureSheaf 𝕜 E M).presheaf.stalk a)

The analytic stalks are regular local rings ([BM97, §3]; [Hir64, p. 121]).

theorem Manifold.spanFinrank_maximalIdeal_stalk {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] [FiniteDimensional 𝕜 E] (a : M) : Submodule.spanFinrank (IsLocalRing.maximalIdeal ↑((structureSheaf 𝕜 E M).presheaf.stalk a)) = Module.finrank 𝕜 E

The embedding dimension of the stalk is n.